Cauchy の平均値の定理を示す問題で apply が失敗する

[Seasawher]

@aconite-ac @haruhisa-enomoto

Lean 勉強会 Analysis / Lecture 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]
      -- apply HasDerivAt.const_mul
      sorry
 
  -- `h` は閉区間 `[a, b]` 上で連続
  have hhc : ContinuousOn h (Icc a b) :=
    (continuousOn_const.mul hfc).sub (continuousOn_const.mul hgc)
  
  -- `h` は端の値が等しい
  have hfI : h a = h b := by simp ; ring

  sorry

-- apply HasDerivAt.const_mul のところで，証明が通らなくなります．なぜでしょうか？

定理が適用できる形だと思ったのですが…

[aconite-ac]

一般的に、エラーメッセージを見て1ステップずつ考えるという方針が有効だと思います。

まず、HasDerivAtの第1引数について、
(fun x ↦ ?c * ?f x)と(fun x ↦ -1 * (f b - f a) * g x)を見比べると、
メタ変数?cには-1 * (f b - f a)が入ってほしいと分かります。
次に、HasDerivAtの第2引数について、
(?c * ?f') = (-1 * (f b - f a) * ?f')と(-((f b - f a) * g' x))を見比べると、
(-((f b - f a) * g' x))は(-1 * (f b - f a) * g' x)という形をとらなければならないと分かります。

あとは、(-((f b - f a) * g' x))を(-1 * (f b - f a) * g' x)にrwする方法を考えればOKです。
(ヒント: hnegとmul_assocに適切な引数を与えるだけです。)