awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
⊢ f x = f y
have h₂ : Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (f ∘ Subtype.val (p := Membership.mem s))
Tactic: have h₂ := hf.continuousOn.comp_continuous continuous_subtype_val (fun x ↦ x.2)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
⊢ f x = f y
have inr : ∀ (h₃ : ¬f x = f y), False
Tactic: by_contra h₃
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x = f y
⊢ False
have inr : ∀ (t : Set E) (ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
  (ht' :
    Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
      (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {f y})ᶜ),
  False
Tactic: obtain ⟨t, ht, ht'⟩ := (isClosed_singleton (x := f y)).preimage h₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' :
  Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
    (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {f y})ᶜ
⊢ False
have ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y
Tactic: have ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y := by simpa [Set.ext_iff] using ht'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' :
  Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
    (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {f y})ᶜ
ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y
⊢ False
have inr : ∀ (z : E) (H₁ : z ∈ s) (H₂ : z ∈ s ∩ f ⁻¹' {f y}) (H₃ : z ∈ t), False
Tactic: obtain ⟨z, H₁, H₂, H₃⟩ := hs' _ _ h₁ ht (fun x h ↦ by simp [h, ht'', eq_or_ne]) ⟨y, by simpa⟩
      ⟨x, by simp [ht'' _ hx, hx, h₃]⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y
have obtain : ∀ (a : G) (ha : ∀ x ∈ s, f x = a), f x = f y
Tactic: obtain ⟨a, ha⟩ := hs.exists_is_const_of_fderiv_eq_zero hs' hf hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
x y : E
hx : x ∈ s
hy : y ∈ s
a : G
ha : ∀ x ∈ s, f x = a
⊢ f x = f y
have rw : a = f y
Tactic: rw [ha x hx, ha y hy]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
x y : E
hx : x ∈ s
hy : y ∈ s
a : G
ha : ∀ x ∈ s, f x = a
rw : a = f y
⊢ f x = f y
have rw₁ : a = a
Tactic: rw [ha x hx, ha y hy]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) (fderiv 𝕜 g) s
⊢ ∃ (a : G), EqOn f (fun (x : E) ↦ g x + a) s
have simp_rw : ∃ (a : G), ∀ ⦃x : E⦄, x ∈ s → f x - g x = a
Tactic: simp_rw [Set.EqOn, ← sub_eq_iff_eq_add']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) (fderiv 𝕜 g) s
⊢ ∃ (a : G), ∀ ⦃x : E⦄, x ∈ s → f x - g x = a
have refine : ∀ (x : E) (hx : x ∈ s), Eq (α := E →L[𝕜] G) (fderiv 𝕜 (fun (x : E) ↦ f x - g x) x) (0 x)
Tactic: refine hs.exists_is_const_of_fderiv_eq_zero hs' (hf.sub hg) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) (fderiv 𝕜 g) s
x : E
hx : x ∈ s
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 (fun (x : E) ↦ f x - g x) x) (0 x)
have rw : HSub.hSub (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x) = 0 x
Tactic: rw [fderiv_fun_sub (hf.differentiableAt (hs.mem_nhds hx)) (hg.differentiableAt (hs.mem_nhds hx)),
    hf' hx, sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) (fderiv 𝕜 g) s
x : E
hx : x ∈ s
rw : HSub.hSub (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x) = 0 x
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 (fun (x : E) ↦ f x - g x) x) (0 x)
have rw₁ : HSub.hSub (α := E →L[𝕜] G) (fderiv 𝕜 g x) (fderiv 𝕜 g x) = 0 x
Tactic: rw [fderiv_fun_sub (hf.differentiableAt (hs.mem_nhds hx)) (hg.differentiableAt (hs.mem_nhds hx)),
    hf' hx, sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) (fderiv 𝕜 g) s
x : E
hx : x ∈ s
rw : HSub.hSub (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x) = 0 x
rw₁ : HSub.hSub (α := E →L[𝕜] G) (fderiv 𝕜 g x) (fderiv 𝕜 g x) = 0 x
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 (fun (x : E) ↦ f x - g x) x) (0 x)
have rw₂ : Eq (α := E →L[𝕜] G) 0 (0 x)
Tactic: rw [fderiv_fun_sub (hf.differentiableAt (hs.mem_nhds hx)) (hg.differentiableAt (hs.mem_nhds hx)),
    hf' hx, sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) (fderiv 𝕜 g) s
x : E
hx : x ∈ s
rw : HSub.hSub (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x) = 0 x
rw₁ : HSub.hSub (α := E →L[𝕜] G) (fderiv 𝕜 g x) (fderiv 𝕜 g x) = 0 x
rw₂ : Eq (α := E →L[𝕜] G) 0 (0 x)
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 (fun (x : E) ↦ f x - g x) x) (0 x)
have rw₃ : Eq (α := E →L[𝕜] G) 0 0
Tactic: rw [fderiv_fun_sub (hf.differentiableAt (hs.mem_nhds hx)) (hg.differentiableAt (hs.mem_nhds hx)),
    hf' hx, sub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
x : E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : ∀ x ∈ s, Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x)
hx : x ∈ s
hfgx : f x = g x
⊢ EqOn f g s
have obtain : ∀ (a : G) (ha : EqOn f (fun (x : E) ↦ g x + a) s), EqOn f g s
Tactic: obtain ⟨a, ha⟩ := hs.exists_eq_add_of_fderiv_eq hs' hf hg hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
x : E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : ∀ x ∈ s, Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x)
hx : x ∈ s
hfgx : f x = g x
a : G
ha : EqOn f (fun (x : E) ↦ g x + a) s
⊢ EqOn f g s
have ha₁ : EqOn f (fun (x : E) ↦ g x + 0) s
Tactic: obtain rfl := left_eq_add.mp (hfgx.symm.trans (ha hx))
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
𝕜 : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace 𝕜 G
E : Type u_5
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
f g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x)
x : E
hfgx : f x = g x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ f = g
have suffices : EqOn f g univ
Tactic: suffices Set.univ.EqOn f g from funext fun x => this <| mem_univ x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf' : IsLittleO (F := ℝ) (𝓝[s] x₀) f' fun (x : E) ↦ ‖x - x₀‖ ^ n
⊢ IsLittleO.{u_1, u_4, 0} (E := G) (F := ℝ) (𝓝[s] x₀) (fun (x : E) ↦ f x - f x₀) fun (x : E) ↦ ‖x - x₀‖ ^ (n + 1)
have rw : ∀ (hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖) ⦃c : ℝ⦄,
  0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖ ^ (n + 1)‖
Tactic: rw [Asymptotics.isLittleO_iff] at hf' ⊢
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖ ^ (n + 1)‖
have simp_rw : ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
Tactic: simp_rw [norm_pow, pow_succ, ← mul_assoc, norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
have hf'₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
Tactic: simp_rw [norm_pow, norm_norm] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
have h1 : ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s
Tactic: have h1 : ∀ᶠ x in 𝓝[s] x₀, x ∈ s := eventually_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
h1 : ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
have h : ∀ (x : E) (hxs : x ∈ s) (h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖y - x₀‖ ^ n),
  [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
Tactic: filter_upwards [h1, hs.eventually_nhdsWithin_segment hx₀s (hf' hc)] with x hxs h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
h1 : ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s
x : E
hxs : x ∈ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖y - x₀‖ ^ n
⊢ [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
have h₁ : ∀ (y : E) (hy : y ∈ [x₀ -[ℝ] x]), c * ‖y - x₀‖ ^ n ≤ c * ‖x - x₀‖ ^ n
Tactic: refine ⟨hs.segment_subset hx₀s hxs, fun y hy ↦ (h y hy).trans ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
h1 : ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s
x : E
hxs : x ∈ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖y - x₀‖ ^ n
y : E
hy : y ∈ [x₀ -[ℝ] x]
⊢ c * ‖y - x₀‖ ^ n ≤ c * ‖x - x₀‖ ^ n
have h₁ : ‖y - x₀‖ ≤ ‖x - x₀‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
have this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
Tactic: have : ∀ᶠ x in 𝓝[s] x₀, segment ℝ x₀ x ⊆ s ∧ ∀ y ∈ segment ℝ x₀ x, ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n := by
    have h1 : ∀ᶠ x in 𝓝[s] x₀, x ∈ s := eventually_mem_nhdsWithin
    filter_upwards [h1, hs.eventually_nhdsWithin_segment hx₀s (hf' hc)] with x hxs h
    refine ⟨hs.segment_subset hx₀s hxs, fun y hy ↦ (h y hy).trans ?_⟩
    gcongr
    exact norm_sub_le_of_mem_segment hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
⊢ ([x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n) → ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
have h : ∀ (h_segment : [x₀ -[ℝ] x] ⊆ s) (h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n),
  ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
Tactic: ⟨h_segment, h⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
have h : ∀ (x : E) (h_segment : [x₀ -[ℝ] x] ⊆ s) (h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n),
  ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
Tactic: filter_upwards [this] with x ⟨h_segment, h⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h_segment : [x₀ -[ℝ] x] ⊆ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
have h₁ : ‖f x - f x₀‖ = ‖f x - f x₀ - (f x₀ - f x₀)‖
Tactic: convert!
    (convex_segment x₀ x).norm_image_sub_le_of_norm_hasFDerivWithin_le (f := fun x ↦ f x - f x₀)
      (y := x) (x := x₀) (s := segment ℝ x₀ x) ?_ h
      (left_mem_segment ℝ x₀ x)
      (right_mem_segment ℝ x₀ x) using 1