awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
c : F
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
x_1 x_2 : 𝕜
⊢ ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)
have field_simp : ‖x_1 - x_2‖ ≤ ‖x_1 - x_2‖
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
x_1 x_2 : 𝕜
⊢ dist x_1 x_2 ≤
    (↑‖f'‖₊⁻¹ : ℝ) *
      dist.{v} (α := F) ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_1 : F)
        ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_2 : F)
have simp : ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)
Tactic: simp [dist_eq_norm_sub, ← sub_smul, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
x_1 x_2 : 𝕜
⊢ ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)
have field_simp : ‖x_1 - x_2‖ ≤ ‖x_1 - x_2‖
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y = c
⊢ derivWithin f s x = 0
have pos : ∀ (hf : DifferentiableWithinAt 𝕜 f s x), derivWithin f s x = 0
Tactic: by_cases hf : DifferentiableWithinAt 𝕜 f s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y = c
pos : ∀ (hf : DifferentiableWithinAt 𝕜 f s x), derivWithin f s x = 0
⊢ derivWithin f s x = 0
have neg : ∀ (hf : ¬DifferentiableWithinAt 𝕜 f s x), derivWithin f s x = 0
Tactic: by_cases hf : DifferentiableWithinAt 𝕜 f s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y = c
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0
have pos : ∀ (h : derivWithin f s x ≠ 0), ∀ᶠ (x : 𝕜) in 𝓝[s \ {x}] x, f x ≠ c
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
⊢ derivWithin f s x = 0
have pos : ∀ (hf : DifferentiableWithinAt 𝕜 f s x), derivWithin f s x = 0
Tactic: by_cases hf : DifferentiableWithinAt 𝕜 f s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
pos : ∀ (hf : DifferentiableWithinAt 𝕜 f s x), derivWithin f s x = 0
⊢ derivWithin f s x = 0
have neg : ∀ (hf : ¬DifferentiableWithinAt 𝕜 f s x), derivWithin f s x = 0
Tactic: by_cases hf : DifferentiableWithinAt 𝕜 f s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0
have pos : ∀ (h : derivWithin f s x ≠ 0), ∀ᶠ (x : 𝕜) in 𝓝[s \ {x}] x, f x ∉ t
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[≠] x, f y = c
⊢ deriv f x = 0
have rw : ∃ᶠ (y : 𝕜) in 𝓝[univ \ {x}] x, f y = c
Tactic: rw [← derivWithin_univ, derivWithin_zero_of_frequently_const]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[≠] x, f y ∈ t
⊢ deriv f x = 0
have rw : ∃ᶠ (y : 𝕜) in 𝓝[univ \ {x}] x, f y ∈ t
Tactic: rw [← derivWithin_univ, derivWithin_zero_of_frequently_mem t ht]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
hg : DifferentiableWithinAt 𝕜 g s a
⊢ False
have this : HasDerivWithinAt id (0 * derivWithin g s a) s a
Tactic: have := (hf.comp a hg.hasDerivWithinAt hst).congr_of_eventuallyEq_of_mem hfg.symm ha
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
hf : HasDerivAt f 0 (g a)
hfg : f ∘ g =ᶠ[𝓝 a] id
hg : DifferentiableAt 𝕜 g a
⊢ False
have this : HasDerivAt id (0 * deriv g a) a
Tactic: have := (hf.comp a hg.hasDerivAt).congr_of_eventuallyEq hfg.symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
have hI : h a = h b
Tactic: have hI : h a = h b := by simp only [h]; ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
hI : h a = h b
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f' x - (f b - f a) * g' x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
Tactic: have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := fun x hx =>
    ((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
hI : h a = h b
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
have hhc : ContinuousOn h (Icc a b)
Tactic: have hhc : ContinuousOn h (Icc a b) :=
    (continuousOn_const.mul hfc).sub (continuousOn_const.mul hgc)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
hI : h a = h b
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
hhc : ContinuousOn h (Icc a b)
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
have rcases : ∀ (c : ℝ) (cmem : c ∈ Ioo a b) (hc : h' c = 0), ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic: rcases exists_hasDerivAt_eq_zero hab hhc hI hhh' with ⟨c, cmem, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
⊢ Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
have this : Tendsto h (𝓝[>] a) (𝓝 ((lgb - lga) * lfa - (lfb - lfa) * lga))
Tactic: have : Tendsto h (𝓝[>] a) (𝓝 <| (lgb - lga) * lfa - (lfb - lfa) * lga) :=
      (tendsto_const_nhds.mul hfa).sub (tendsto_const_nhds.mul hga)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
this : Tendsto h (𝓝[>] a) (𝓝 ((lgb - lga) * lfa - (lfb - lfa) * lga))
⊢ Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
have h₁ : lgb * lfa - lfb * lga = (lgb - lga) * lfa - (lfb - lfa) * lga
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
⊢ ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
have hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
Tactic: have hha : Tendsto h (𝓝[>] a) (𝓝 <| lgb * lfa - lfb * lga) := by
    have : Tendsto h (𝓝[>] a) (𝓝 <| (lgb - lga) * lfa - (lfb - lfa) * lga) :=
      (tendsto_const_nhds.mul hfa).sub (tendsto_const_nhds.mul hga)
    convert! this using 2
    ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
⊢ Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
have this : Tendsto h (𝓝[<] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))
Tactic: have : Tendsto h (𝓝[<] b) (𝓝 <| (lgb - lga) * lfb - (lfb - lfa) * lgb) :=
      (tendsto_const_nhds.mul hfb).sub (tendsto_const_nhds.mul hgb)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
this : Tendsto h (𝓝[<] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))
⊢ Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
have h₁ : lgb * lfa - lfb * lga = (lgb - lga) * lfb - (lfb - lfa) * lgb
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
⊢ ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
have hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
Tactic: have hhb : Tendsto h (𝓝[<] b) (𝓝 <| lgb * lfa - lfb * lga) := by
    have : Tendsto h (𝓝[<] b) (𝓝 <| (lgb - lga) * lfb - (lfb - lfa) * lgb) :=
      (tendsto_const_nhds.mul hfb).sub (tendsto_const_nhds.mul hgb)
    convert! this using 2
    ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
⊢ ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
Tactic: have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := by
    intro x hx
    exact ((hff' x hx).const_mul _).sub ((hgg' x hx).const_mul _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
⊢ ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
have rcases : ∀ (c : ℝ) (cmem : c ∈ Ioo a b) (hc : h' c = 0), ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
Tactic: rcases exists_hasDerivAt_eq_zero' hab hha hhb hhh' with ⟨c, cmem, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
have obtain : ∀ (c : ℝ) (cmem : c ∈ Ioo a b) (hc : (b - a) * f' c = (f b - f a) * 1), ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
Tactic: obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Ioo a b, (b - a) * f' c = (f b - f a) * 1 :=
    exists_ratio_hasDerivAt_eq_ratio_slope f f' hab hfc hff' id 1 continuousOn_id
      fun x _ => hasDerivAt_id x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
have right : f' c = (f b - f a) / (b - a)
Tactic: use c, cmem
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
⊢ f' c = (f b - f a) / (b - a)
have right : ∀ (hc : (b - a) * f' c = f b - f a), f' c = (f b - f a) / (b - a)
Tactic: rwa [mul_one, mul_comm, ← eq_div_iff (sub_ne_zero.2 hab.ne')] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
right : ∀ (hc : (b - a) * f' c = f b - f a), f' c = (f b - f a) / (b - a)
⊢ f' c = (f b - f a) / (b - a)
have right₁ : ∀ (hc : f' c * (b - a) = f b - f a), f' c = (f b - f a) / (b - a)
Tactic: rwa [mul_one, mul_comm, ← eq_div_iff (sub_ne_zero.2 hab.ne')] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
right : ∀ (hc : (b - a) * f' c = f b - f a), f' c = (f b - f a) / (b - a)
right₁ : ∀ (hc : f' c * (b - a) = f b - f a), f' c = (f b - f a) / (b - a)
⊢ f' c = (f b - f a) / (b - a)
have right₂ : ∀ (hc : f' c = (f b - f a) / (b - a)), f' c = (f b - f a) / (b - a)
Tactic: rwa [mul_one, mul_comm, ← eq_div_iff (sub_ne_zero.2 hab.ne')] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
⊢ ∃ c ∈ Ioo a b, deriv f c = slope f a b
have rw : ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a)
Tactic: rw [slope_def_field]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
⊢ Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
have refine : deriv f =ᶠ[𝓝[>] a] derivWithin f (Ioi a)
Tactic: refine hf.congr' ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
⊢ deriv f =ᶠ[𝓝[>] a] derivWithin f (Ioi a)
have h : ∀ (x : ℝ) (hx : x ∈ Ioi a), deriv f x = derivWithin f (Ioi a) x
Tactic: filter_upwards [eventually_mem_nhdsWithin] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
x : ℝ
hx : x ∈ Ioi a
⊢ deriv f x = derivWithin f (Ioi a) x
have this : Ioi a ∈ 𝓝 x
Tactic: have : Ioi a ∈ 𝓝 x := by simp [← mem_interior_iff_mem_nhds, hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
⊢ ¬DifferentiableWithinAt ℝ f (Ioi a) a
have hf₁ : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
Tactic: replace hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop := by
    refine hf.congr' ?_
    filter_upwards [eventually_mem_nhdsWithin] with x hx
    have : Ioi a ∈ 𝓝 x := by simp [← mem_interior_iff_mem_nhds, hx]
    exact (derivWithin_of_mem_nhds this).symm
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
⊢ ¬DifferentiableWithinAt ℝ f (Ioi a) a
have by_cases : ∀ (hcont_at_a : ContinuousWithinAt f (Ici a) a), ¬DifferentiableWithinAt ℝ f (Ioi a) a
Tactic: by_cases hcont_at_a : ContinuousWithinAt f (Ici a) a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
by_cases : ∀ (hcont_at_a : ContinuousWithinAt f (Ici a) a), ¬DifferentiableWithinAt ℝ f (Ioi a) a
⊢ ¬DifferentiableWithinAt ℝ f (Ioi a) a
have by_cases₁ : ∀ (hcont_at_a : ¬ContinuousWithinAt f (Ici a) a), ¬DifferentiableWithinAt ℝ f (Ioi a) a
Tactic: by_cases hcont_at_a : ContinuousWithinAt f (Ici a) a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ¬ContinuousWithinAt f (Ici a) a
hcontra : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ False
have this : ContinuousWithinAt f (Ioi a) a
Tactic: have := hcontra.continuousWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ¬ContinuousWithinAt f (Ici a) a
hcontra : DifferentiableWithinAt ℝ f (Ioi a) a
this : ContinuousWithinAt f (Ioi a) a
⊢ False
have hcont_at_a₁ : ¬ContinuousWithinAt f (Ici a \ Ioi a) a
Tactic: rw [← ContinuousWithinAt.diff_iff this] at hcont_at_a
Cleared hypotheses: hcont_at_a, hcontra, this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ False
have hdiff₁ : HasDerivWithinAt f (derivWithin f (Ioi a) a) (Ioi a) a
Tactic: replace hdiff := hdiff.hasDerivWithinAt
Cleared hypotheses: hdiff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : HasDerivWithinAt f (derivWithin f (Ioi a) a) (Ioi a) a
⊢ False
have hdiff₁ : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
Tactic: rw [hasDerivWithinAt_iff_tendsto_slope, Set.diff_singleton_eq_self self_notMem_Ioi] at hdiff
Cleared hypotheses: hdiff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
have rw : ∃ (i : ℝ),
  a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1
Tactic: rw [(nhdsGT_basis a).eventually_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
⊢ ∃ (i : ℝ),
    a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1
have hf₁ : ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
Tactic: rw [(nhdsGT_basis a).tendsto_left_iff] at hf
Cleared hypotheses: hf, hcont_at_a, hdiff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf :
  ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
⊢ ∃ (i : ℝ),
    a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1
have obtain : ∀ (b : ℝ) (hab : a < b) (hb : MapsTo (derivWithin f (Ioi a)) (Ioo a b) (Ioi (max (derivWithin f (Ioi a) a + 1) 0))),
  ∃ (i : ℝ),
    a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1
Tactic: obtain ⟨b, hab, hb⟩ := hf (Ioi (max (derivWithin f (Ioi a) a + 1) 0)) (Ioi_mem_atTop _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf :
  ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
b : ℝ
hab : a < b
hb : MapsTo (derivWithin f (Ioi a)) (Ioo a b) (Ioi (max (derivWithin f (Ioi a) a + 1) 0))
⊢ ∃ (i : ℝ),
    a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1
have refine : ∀ (x : ℝ) (hx : x ∈ Ioo a b) (z : ℝ) (hz : z ∈ Ioc a x), max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) z
Tactic: refine ⟨b, hab, fun x hx z hz => ?_⟩