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
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
g : (a : ℝ) → E := (⇑(AffineMap.lineMap x y) : (a : ℝ) → E)
segm : MapsTo g (Icc 0 1) s
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖
have hD : ∀ (t : ℝ),
  Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → G) (y - x)) (Icc 0 1) t
Tactic: have hD : ∀ t ∈ Icc (0 : ℝ) 1,
      HasDerivWithinAt (f ∘ g) (f' (g t) (y - x)) (Icc 0 1) t := fun t ht => by
    simpa using ((hf (g t) (segm ht)).restrictScalars ℝ).comp_hasDerivWithinAt _
      AffineMap.hasDerivWithinAt_lineMap segm
-- 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
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
g : (a : ℝ) → E := (⇑(AffineMap.lineMap x y) : (a : ℝ) → E)
segm : MapsTo g (Icc 0 1) s
hD :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → G) (y - x)) (Icc 0 1) t
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖
have bound₁ : ∀ (t : ℝ),
  Membership.mem (γ := Set ℝ) (Ico 0 1) t → norm.{u_4} (E := G) ((f' (g t) : (a : E) → G) (y - x) : G) ≤ C * ‖y - x‖
Tactic: have bound : ∀ t ∈ Ico (0 : ℝ) 1, ‖f' (g t) (y - x)‖ ≤ C * ‖y - x‖ := fun t ht =>
    le_of_opNorm_le _ (bound _ <| segm <| Ico_subset_Icc_self 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
f' : E → E →L[𝕜] G
C : ℝ≥0
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
hs : Convex ℝ s
⊢ LipschitzOnWith C f s
have rw : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ (↑C : ℝ) * ‖x - y‖
Tactic: rw [lipschitzOnWith_iff_norm_sub_le]
-- 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
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have obtain : ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ball x ε ∩ s ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}),
  ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
Tactic: obtain ⟨ε, ε0, hε⟩ : ∃ ε > 0,
      ball x ε ∩ s ⊆ { y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K } :=
    mem_nhdsWithin_iff.1 (hder.and <| hcont.nnnorm.eventually (gt_mem_nhds hK))
-- 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
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
ε : ℝ
ε0 : ε > 0
hε : ball x ε ∩ s ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have hε₁ : s ∩ ball x ε ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
Tactic: rw [inter_comm] at hε
Cleared hypotheses: 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
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
ε : ℝ
ε0 : ε > 0
hε : s ∩ ball x ε ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have refine : LipschitzOnWith K f (s ∩ ball x ε)
Tactic: refine ⟨s ∩ ball x ε, inter_mem_nhdsWithin _ (ball_mem_nhds _ ε0), ?_⟩
-- 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 : E → G
C : ℝ≥0
hf : Differentiable 𝕜 f
bound : ∀ (x : E), nnnorm (E := E →L[𝕜] G) (fderiv 𝕜 f x) ≤ C
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ LipschitzWith C f
have rw : LipschitzOnWith C f univ
Tactic: rw [← lipschitzOnWith_univ]
-- 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
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
⊢ ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ ≤ C * ‖y - x‖
have hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
Tactic: have hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x := fun x xs =>
    (hf x xs).sub φ.hasFDerivWithinAt
-- 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
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
⊢ ‖f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G)‖ =
    ‖HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G) - HSub.hSub (β := G) (f x) ((φ : (a : E) → G) x : G)‖
have e_a : f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G) =
  HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G) - HSub.hSub (β := G) (f x) ((φ : (a : E) → G) x : G)
Tactic: congr 1
-- 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
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
⊢ ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ ≤ C * ‖y - x‖
have y₁ : ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ =
  ‖f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G)‖
Tactic: calc
    ‖f y - f x - φ (y - x)‖ = ‖f y - f x - (φ y - φ x)‖ := by simp
    _ = ‖f y - φ y - (f x - φ x)‖ := by congr 1; abel
    _ = ‖g y - g x‖ := by simp [g]
    _ ≤ C * ‖y - x‖ := Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le hg bound hs xs ys
-- 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
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
y₁ :
  ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ =
    ‖f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G)‖
⊢ ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ ≤ C * ‖y - x‖
have y₂ : ‖f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G)‖ =
  ‖HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G) - HSub.hSub (β := G) (f x) ((φ : (a : E) → G) x : G)‖
Tactic: calc
    ‖f y - f x - φ (y - x)‖ = ‖f y - f x - (φ y - φ x)‖ := by simp
    _ = ‖f y - φ y - (f x - φ x)‖ := by congr 1; abel
    _ = ‖g y - g x‖ := by simp [g]
    _ ≤ C * ‖y - x‖ := Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le hg bound hs xs ys
-- 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
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
y₁ :
  ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ =
    ‖f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G)‖
y₂ :
  ‖f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G)‖ =
    ‖HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G) - HSub.hSub (β := G) (f x) ((φ : (a : E) → G) x : G)‖
⊢ ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ ≤ C * ‖y - x‖
have y₃ : ‖HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G) - HSub.hSub (β := G) (f x) ((φ : (a : E) → G) x : G)‖ = ‖g y - g x‖
Tactic: calc
    ‖f y - f x - φ (y - x)‖ = ‖f y - f x - (φ y - φ x)‖ := by simp
    _ = ‖f y - φ y - (f x - φ x)‖ := by congr 1; abel
    _ = ‖g y - g x‖ := by simp [g]
    _ ≤ C * ‖y - x‖ := Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le hg bound hs xs ys
-- 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
x y : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ x ∈ s, Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f s x) 0
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y
have bound : ∀ x ∈ s, norm (E := E →L[𝕜] G) (fderivWithin 𝕜 f s x) ≤ 0
Tactic: have bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖ ≤ 0 := fun x hx => by
    simp only [hf' x hx, norm_zero, le_rfl]
-- 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 : E → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : E), Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) 0
x_1 y : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f univ x) 0
have rw : Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) 0
Tactic: rw [fderivWithin_univ]
-- 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 : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (β := E →L[𝕜] G) (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
⊢ f y = g y
have suffices : f x - g x = f y - g y
Tactic: suffices f x - g x = f y - g y by rwa [hfgx, sub_self, eq_comm, sub_eq_zero] at this
-- 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 : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (β := E →L[𝕜] G) (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
⊢ f x - g x = f y - g y
have refine : ∀ (z : E) (hz : z ∈ s), Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f - g) s z) 0
Tactic: refine hs.is_const_of_fderivWithin_eq_zero (hf.sub hg) (fun z hz => ?_) hx 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
x : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (β := E →L[𝕜] G) (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f - g) s z) 0
have rw : HSub.hSub (α := E →L[𝕜] G) (fderivWithin 𝕜 f s z) (fderivWithin 𝕜 g s z) = 0
Tactic: rw [fderivWithin_sub (hs' _ hz) (hf _ hz) (hg _ hz), sub_eq_zero, hf' hz]
-- 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 : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (β := E →L[𝕜] G) (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
rw : HSub.hSub (α := E →L[𝕜] G) (fderivWithin 𝕜 f s z) (fderivWithin 𝕜 g s z) = 0
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f - g) s z) 0
have rw₁ : Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f s z) (fderivWithin 𝕜 g s z)
Tactic: rw [fderivWithin_sub (hs' _ hz) (hf _ hz) (hg _ hz), sub_eq_zero, hf' hz]
-- 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 : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (β := E →L[𝕜] G) (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
rw : HSub.hSub (α := E →L[𝕜] G) (fderivWithin 𝕜 f s z) (fderivWithin 𝕜 g s z) = 0
rw₁ : Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f s z) (fderivWithin 𝕜 g s z)
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f - g) s z) 0
have rw₂ : Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 g s z) (fderivWithin 𝕜 g s z)
Tactic: rw [fderivWithin_sub (hs' _ hz) (hf _ hz) (hg _ hz), sub_eq_zero, hf' hz]
-- 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
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' t)
have refine : ∀ y ∈ s ∩ f ⁻¹' t, ∀ (hy : y ∈ s) (hy' : y ∈ f ⁻¹' t), ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t
Tactic: refine Metric.isOpen_iff.mpr fun y ⟨hy, 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
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
y : E
h : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
⊢ ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t
have obtain : ∀ (r : ℝ) (hr : r > 0) (h : ball y r ⊆ s), ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t
Tactic: obtain ⟨r, hr, h⟩ := Metric.isOpen_iff.mp hs 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
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
y : E
h_1 : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
⊢ ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t
have refine : ∀ (x : E) (hx : x ∈ ball y r), x ∈ f ⁻¹' t
Tactic: refine ⟨r, hr, Set.subset_inter h 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 : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
y : E
h_1 : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
⊢ x ∈ f ⁻¹' t
have refine_2 : ∀ (this : f x = f y), x ∈ f ⁻¹' t
Tactic: have := (convex_ball y r).is_const_of_fderivWithin_eq_zero (hf.mono h) ?_ hx (mem_ball_self hr)
-- 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
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
y : E
h_1 : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
refine_2 : ∀ (this : f x = f y), x ∈ f ⁻¹' t
⊢ x ∈ f ⁻¹' t
have refine_1 : ∀ x ∈ ball y r, Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f (ball y r) x) 0
Tactic: have := (convex_ball y r).is_const_of_fderivWithin_eq_zero (hf.mono h) ?_ hx (mem_ball_self hr)
-- 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
⊢ ∃ (a : G), ∀ x ∈ s, f x = a
have inl : ∀ (hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hs' : IsPreconnected.{u_1} (α := E) ∅)
  (hf : DifferentiableOn 𝕜 f ∅) (hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 ∅),
  ∃ (a : G), ∀ (x : E), Membership.mem (γ := Set E) ∅ x → f x = a
Tactic: obtain (rfl | ⟨y, hy⟩) := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs, 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
inl :
  ∀ (hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hs' : IsPreconnected.{u_1} (α := E) ∅)
    (hf : DifferentiableOn 𝕜 f ∅) (hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 ∅),
    ∃ (a : G), ∀ (x : E), Membership.mem (γ := Set E) ∅ x → f x = a
⊢ ∃ (a : G), ∀ x ∈ s, f x = a
have inr : ∀ (y : E) (hy : y ∈ s), ∃ (a : G), ∀ x ∈ s, f x = a
Tactic: obtain (rfl | ⟨y, hy⟩) := s.eq_empty_or_nonempty
-- 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
⊢ ∃ (a : G), ∀ x ∈ s, f x = a
have inr : ∀ (x : E) (hx : x ∈ s), f x = f y
Tactic: refine ⟨f y, fun x hx ↦ ?_⟩
-- 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
⊢ f x = f y
have h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
Tactic: have h₁ := hs.isOpen_inter_preimage_of_fderiv_eq_zero hf hf' {f y}