mvt.lean:11:2 unknown identifier 'hgf' mvt.lean:11:6 unexpec

Stream: lean4

[Lewis]

How to correct:

import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Data.Real.Basic

open Set

theorem mean_value_theorem {a b : ℝ} (hab : a < b) {f : ℝ → ℝ}
  (hfc : ContinuousOn f (Icc a b)) (hfd : DifferentiableOn ℝ f (Ioo a b)) :
  ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a) :=
let
  g := λ x ↦ f x - (f b - f a) / (b - a) * x;
  hgf := ContinuousOn.sub hfc (ContinuousOn.mul continuousOn_const continuousOn_id);
  hgd := DifferentiableOn.sub hfd (DifferentiableOn.mul (differentiableOn_const _) differentiableOn_id);
  hga := rfl;
  hgb := rfl;
  hgab := by rw [hga, hgb]; field_simp [ne_of_lt hab]; ring;
  ⟨c, hc, hgc⟩ := exists_deriv_eq_zero hgf hgd hgab hab
in ⟨c, hc, by
  have h : deriv g c = 0 := hgc;
  rw [deriv_sub, deriv_const_mul_field, deriv_id] at h;
  field_simp [ne_of_lt hab] at h;
  rw sub_eq_zero at h;
  exact h⟩

to fix the errors:

mvt.lean:11:2
unknown identifier 'hgf'
mvt.lean:11:6
unexpected token ':='; expected command

?

Thanks.

[Kim Morrison]

You need a separate let for each definition, I think??