Conv モードに一度入るだけで，複数ターゲットの書き換えをする

[Seasawher]

@aconite-ac

何度もすみません．Lean 勉強会 Analysis 2 の exists_ratio_hasDerivAt_eq_ratio_slope についてです．

この問題そのものは解くことができました．私のコードを以下に示します．

/-- Cauchyの平均値の定理 -/
theorem exists_ratio_hasDerivAt_eq_ratio_slope (hab : a < b) 
    (hfc : ContinuousOn f (Icc a b)) (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x)
      (hgc : ContinuousOn g (Icc a b)) (hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x) :
        ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c := by
  -- 関数 `h` を定義する
  let h x := (g b - g a) * f x - (f b - f a) * g x

  -- 関数 `h'` も定義する
  let h' x := (g b - g a) * f' x - (f b - f a) * g' x

  -- マイナス1を掛けることと，加法逆元をとることが同じ
  have hneg : ∀ a : ℝ , - a = (-1) * a := by exact fun a ↦ neg_eq_neg_one_mul a

  -- `h'` は `h` の導関数
  have hdv : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := by
    intros x hx
    dsimp
    apply HasDerivAt.add
    · apply HasDerivAt.const_mul
      exact hff' x hx
    · conv =>
        arg 1
        intro x
        rw [hneg]
        rw [← mul_assoc]
      conv =>
        arg 2
        rw [hneg, ←mul_assoc]
      apply HasDerivAt.const_mul
      exact hgg' x hx
 
  -- 以下省略
  sorry

ここで hdv の証明をする際に２回 conv を使用していますが，一回で済ませる書き方はありませんか？

[aconite-ac]

単純にconvを一度で済ませられればいいということなら、

conv =>
  arg 2
  rw [hneg, ←mul_assoc]

の代わりに

rw [hneg ((f b - f a) * g' x), ←mul_assoc]

とすればOKです。

しかし、rw [hneg]とrw [← mul_assoc]を一度で済ませる方法は自分はすぐには思いつきませんね…。
rw [hneg]の制御が難しいと感じています。

[Seasawher]

ありがとうございます

arg を実行したときに、constructor のように複数のターゲットに分割する、というのがやりたいことなのですが、それはleanにサポートされていなさそうということでしょうか？

[aconite-ac]

質問の意図を勘違いしていました。失礼しました。
それでしたら、convモード中にcongrを使う事で解決できます。
congrは(入れ子になっている場合は一番外側の)関数を分解し、引数の数だけターゲットを生成するコマンドです。

以下解答例です。個人的にも、こちらの方が簡潔かつ分かりやすい気がしますね。

    · conv =>
        congr
        · intro x
          rw [hneg, ← mul_assoc]
        · rw [hneg, ← mul_assoc]