awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
inl : ∀ (hxy' : x = y), C * (y - x) ≤ f y - f x
⊢ C * (y - x) ≤ f y - f x
have inr : ∀ (hxy' : x < y), C * (y - x) ≤ f y - f x
Tactic: rcases eq_or_lt_of_le hxy with hxy' | hxy'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x = y
⊢ C * (y - x) ≤ f y - f x
have inl : C * (y - y) ≤ f y - f y
Tactic: rw [hxy', sub_self, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x = y
inl : C * (y - y) ≤ f y - f y
⊢ C * (y - x) ≤ f y - f x
have inl₁ : C * 0 ≤ f y - f y
Tactic: rw [hxy', sub_self, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x = y
inl : C * (y - y) ≤ f y - f y
inl₁ : C * 0 ≤ f y - f y
⊢ C * (y - x) ≤ f y - f x
have inl₂ : C * 0 ≤ 0
Tactic: rw [hxy', sub_self, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x = y
inl : C * (y - y) ≤ f y - f y
inl₁ : C * 0 ≤ f y - f y
inl₂ : C * 0 ≤ 0
⊢ C * (y - x) ≤ f y - f x
have inl₃ : LE.le (α := ℝ) 0 0
Tactic: rw [hxy', sub_self, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
⊢ C * (y - x) ≤ f y - f x
have hxyD : Icc x y ⊆ D
Tactic: have hxyD : Icc x y ⊆ D := hD.ordConnected.out hx hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
⊢ C * (y - x) ≤ f y - f x
have hxyD' : Ioo x y ⊆ interior D
Tactic: have hxyD' : Ioo x y ⊆ interior D :=
    subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hxyD⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
⊢ C * (y - x) ≤ f y - f x
have inr : ∀ (a : ℝ) (a_mem : a ∈ Ioo x y) (ha : deriv f a = (f y - f x) / (y - x)), C * (y - x) ≤ f y - f x
Tactic: obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) :=
    exists_deriv_eq_slope f hxy' (hf.mono hxyD) (hf'.mono hxyD')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
⊢ C * (y - x) ≤ f y - f x
have this : C ≤ (f y - f x) / (y - x)
Tactic: have : C ≤ (f y - f x) / (y - x) := ha ▸ hf'_ge _ (hxyD' a_mem)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x_1 : ℝ
hx_1 : x_1 ∈ D
y : ℝ
hy : y ∈ D
hxy : x_1 < y
x : ℝ
hx : x ∈ interior D
⊢ -C < deriv (fun (y : ℝ) ↦ -f y) x
have rw : deriv f x < C
Tactic: rw [deriv.fun_neg, neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
⊢ f y - f x < C * (y - x)
have hf'_gt : ∀ x ∈ interior D, -C < deriv (fun (y : ℝ) ↦ -f y) x
Tactic: have hf'_gt : ∀ x ∈ interior D, -C < deriv (fun y => -f y) x := fun x hx => by
    rw [deriv.fun_neg, neg_lt_neg_iff]
    exact lt_hf' x hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
hf'_gt : ∀ x ∈ interior D, -C < deriv (fun (y : ℝ) ↦ -f y) x
⊢ f y - f x < C * (y - x)
have linarith : C * (y - x) ≤ f y - f x → C * (y - x) - (f y - f x) + (-C * (y - x) - (-f y - -f x)) = 0
Tactic: linarith [hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x hx y hy hxy]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x_1 : ℝ
hx_1 : x_1 ∈ D
y : ℝ
hy : y ∈ D
hxy : x_1 ≤ y
x : ℝ
hx : x ∈ interior D
⊢ -C ≤ deriv (fun (y : ℝ) ↦ -f y) x
have rw : deriv f x ≤ C
Tactic: rw [deriv.fun_neg, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
⊢ f y - f x ≤ C * (y - x)
have hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (fun (y : ℝ) ↦ -f y) x
Tactic: have hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (fun y => -f y) x := fun x hx => by
    rw [deriv.fun_neg, neg_le_neg_iff]
    exact le_hf' x hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (fun (y : ℝ) ↦ -f y) x
⊢ f y - f x ≤ C * (y - x)
have linarith : C * (y - x) < f y - f x → C * (y - x) - (f y - f x) + (-C * (y - x) - (-f y - -f x)) = 0
Tactic: linarith [hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x hx y hy hxy]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ x < y → f x < f y
have this : DifferentiableOn ℝ f (interior D)
Tactic: have : DifferentiableOn ℝ f (interior D) := fun z hz =>
    (differentiableAt_of_deriv_ne_zero (hf' z hz).ne').differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 < f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 < deriv f x
have rw : 0 < f' x
Tactic: rw [deriv_eqOn isOpen_interior hf' hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
⊢ 0 < deriv f x
have rw : 0 < f' x
Tactic: rw [(hf _).deriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ deriv f x
have rw : 0 ≤ f' x
Tactic: rw [deriv_eqOn isOpen_interior hf' hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
⊢ 0 ≤ deriv f x
have rw : 0 ≤ f' x
Tactic: rw [(hf _).deriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x < 0
x : ℝ
hx : x ∈ interior D
⊢ deriv f x < 0
have rw : f' x < 0
Tactic: rw [deriv_eqOn isOpen_interior hf' hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
⊢ deriv f x < 0
have rw : f' x < 0
Tactic: rw [(hf _).deriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x ≤ 0
x : ℝ
hx : x ∈ interior D
⊢ deriv f x ≤ 0
have rw : f' x ≤ 0
Tactic: rw [deriv_eqOn isOpen_interior hf' hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
⊢ deriv f x ≤ 0
have rw : f' x ≤ 0
Tactic: rw [(hf _).deriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z : (a : E) → ℝ) (y - x)
have hsub : Ioo 0 1 ⊆ I
Tactic: have hsub : Ioo (0 : ℝ) 1 ⊆ I := Ioo_subset_Icc_self
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z : (a : E) → ℝ) (y - x)
have hmaps : MapsTo g I s
Tactic: have hmaps : MapsTo g I s := hs.mapsTo_lineMap xs ys
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z : (a : E) → ℝ) (y - x)
have hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
Tactic: have hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) (f' (g t) (y - x)) I t := fun t ht =>
    (hf _ (hmaps ht)).comp_hasDerivWithinAt t AffineMap.hasDerivWithinAt_lineMap hmaps
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
⊢ ∃ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧
      (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0
have refine_1 : ContinuousOn (f ∘ g) (Icc 0 1)
Tactic: refine exists_hasDerivAt_eq_slope (f ∘ g) _ (by simp) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
refine_1 : ContinuousOn (f ∘ g) (Icc 0 1)
⊢ ∃ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧
      (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0
have refine_2 : ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) x_1 → HasDerivAt (f ∘ g) ((f' (g x_1) : (a : E) → ℝ) (y - x)) x_1
Tactic: refine exists_hasDerivAt_eq_slope (f ∘ g) _ (by simp) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z : (a : E) → ℝ) (y - x)
have hMVT : ∃ (t : ℝ),
  Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧
    (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0
Tactic: have hMVT : ∃ t ∈ Ioo (0 : ℝ) 1, f' (g t) (y - x) = (f (g 1) - f (g 0)) / (1 - 0) := by
    refine exists_hasDerivAt_eq_slope (f ∘ g) _ (by simp) ?_ ?_
    · exact fun t Ht => (hfg t Ht).continuousWithinAt
    · exact fun t Ht => (hfg t <| hsub Ht).hasDerivAt (Icc_mem_nhds Ht.1 Ht.2)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
hMVT :
  ∃ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧
      (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z : (a : E) → ℝ) (y - x)
have rcases : ∀ (t : ℝ) (Ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t)
  (hMVT' : (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0),
  ∃ z ∈ segment ℝ x y, f y - f x = (f' z : (a : E) → ℝ) (y - x)
Tactic: rcases hMVT with ⟨t, Ht, hMVT'⟩
Cleared hypotheses: hMVT
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
t : ℝ
Ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
hMVT' : (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z : (a : E) → ℝ) (y - x)
have rw : ∃ (x_1 : ℝ),
  Membership.mem (γ := Set ℝ) (Icc 0 1) x_1 ∧
    f y - f x = (f' ((AffineMap.lineMap x y : (a : ℝ) → E) x_1) : (a : E) → ℝ) (y - x)
Tactic: rw [segment_eq_image_lineMap, exists_mem_image]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
t : ℝ
Ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
hMVT' : (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0
⊢ ∃ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) x_1 ∧
      f y - f x = (f' ((AffineMap.lineMap x y : (a : ℝ) → E) x_1) : (a : E) → ℝ) (y - x)
have refine : f y - f x = (f' ((AffineMap.lineMap x y : (a : ℝ) → E) t) : (a : E) → ℝ) (y - x)
Tactic: refine ⟨t, hsub Ht, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
⊢ HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x
have pos : ∀ (hxu : x ∈ tsupport u),
  HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x
Tactic: by_cases hxu : x ∈ tsupport u
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
pos :
  ∀ (hxu : x ∈ tsupport u),
    HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
      (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
        ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
      x
⊢ HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x
have neg : ∀ (hxu : x ∉ tsupport u),
  HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x
Tactic: by_cases hxu : x ∈ tsupport u
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
⊢ HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x
have pos : ∀ (hxv : x ∈ tsupport v),
  HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x
Tactic: by_cases hxv : x ∈ tsupport v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
pos :
  ∀ (hxv : x ∈ tsupport v),
    HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
      (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
        ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
      x
⊢ HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x
have neg : ∀ (hxv : x ∉ tsupport v),
  HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x
Tactic: by_cases hxv : x ∈ tsupport v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∉ tsupport v
⊢ HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x
have hx : x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)
Tactic: have hx : x ∉ tsupport fun x ↦ B (u x) (v x) :=
        mt (closure_mono (fun x ↦ mt fun h ↦ by simp [h]) ·) hxv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∉ tsupport v
hx : x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)
⊢ HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x
have h : HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
    ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G) =
  0
Tactic: convert! HasDerivAt.of_notMem_tsupport hx