awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : ¬y = a
⊢ ContinuousWithinAt f t y
have this : y ∈ s
Tactic: have : y ∈ s := sab ⟨hy.1, lt_of_le_of_ne hy.2 h⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
⊢ HasDerivWithinAt f e (Iic a) a
have t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
Tactic: have t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y := by
    rw [t_closure]
    intro y hy
    by_cases h : y = a
    · rw [h]; exact f_lim.mono ts
    · have : y ∈ s := sab ⟨hy.1, lt_of_le_of_ne hy.2 h⟩
      exact (f_diff.continuousOn y this).mono ts
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
⊢ Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
have simp : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ toSpanSingleton ℝ (deriv f x)) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
Tactic: simp only [toSpanSingleton_deriv.symm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
⊢ HasDerivWithinAt f e (Iic a) a
have t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
Tactic: have t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (1 : ℝ →L[ℝ] ℝ) e)) := by
    simp only [toSpanSingleton_deriv.symm]
    exact Tendsto.comp
      (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
      (tendsto_nhdsWithin_mono_left Ioo_subset_Iio_self f_lim')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
⊢ HasDerivWithinAt f e (Icc b a) a
have rw : HasFDerivWithinAt f (toSpanSingleton ℝ e) (closure t) a
Tactic: rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← t_closure]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
⊢ HasDerivWithinAt f e (Iic a) a
have this : HasDerivWithinAt f e (Icc b a) a
Tactic: have : HasDerivWithinAt f e (Icc b a) a := by
    rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← t_closure]
    exact hasFDerivWithinAt_closure_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ HasDerivWithinAt f (g x) (Ici x) x
have diff : DifferentiableOn ℝ f (Ioi x)
Tactic: have diff : DifferentiableOn ℝ f (Ioi x) := fun y hy =>
      (f_diff y (ne_of_gt hy)).differentiableAt.differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
⊢ HasDerivWithinAt f (g x) (Ici x) x
have hasDerivWithinAt_Ici_of_tendsto_deriv : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] x) (𝓝 (g x))
Tactic: apply
      hasDerivWithinAt_Ici_of_tendsto_deriv diff hf.continuousWithinAt
        self_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
⊢ Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] x) (𝓝 (g x))
have this : Tendsto g (𝓝[>] x) (𝓝 (g x))
Tactic: have : Tendsto g (𝓝[>] x) (𝓝 (g x)) := tendsto_inf_left hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[>] x) (𝓝 (g x))
⊢ Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] x) (𝓝 (g x))
have apply : g =ᶠ[𝓝[>] x] fun (x : ℝ) ↦ deriv f x
Tactic: apply this.congr' _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[>] x) (𝓝 (g x))
⊢ g =ᶠ[𝓝[>] x] fun (x : ℝ) ↦ deriv f x
have apply : ∀ (y : ℝ) (hy : y ∈ Ioi x), Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ g x = (fun (x : ℝ) ↦ deriv f x) x) x} y
Tactic: apply mem_of_superset self_mem_nhdsWithin fun y hy => _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ HasDerivAt f (g x) x
have A : HasDerivWithinAt f (g x) (Ici x) x
Tactic: have A : HasDerivWithinAt f (g x) (Ici x) x := by
    have diff : DifferentiableOn ℝ f (Ioi x) := fun y hy =>
      (f_diff y (ne_of_gt hy)).differentiableAt.differentiableWithinAt
    -- next line is the nontrivial bit of this proof, appealing to differentiability
    -- extension results.
    apply
      hasDerivWithinAt_Ici_of_tendsto_deriv diff hf.continuousWithinAt
        self_mem_nhdsWithin
    have : Tendsto g (𝓝[>] x) (𝓝 (g x)) := tendsto_inf_left hg
    apply this.congr' _
    apply mem_of_superset self_mem_nhdsWithin fun y hy => _
    intro y hy
    exact (f_diff y (ne_of_gt hy)).deriv.symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
⊢ HasDerivWithinAt f (g x) (Iic x) x
have diff : DifferentiableOn ℝ f (Iio x)
Tactic: have diff : DifferentiableOn ℝ f (Iio x) := fun y hy =>
      (f_diff y (ne_of_lt hy)).differentiableAt.differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
⊢ HasDerivWithinAt f (g x) (Iic x) x
have hasDerivWithinAt_Iic_of_tendsto_deriv : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] x) (𝓝 (g x))
Tactic: apply
      hasDerivWithinAt_Iic_of_tendsto_deriv diff hf.continuousWithinAt
        self_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
⊢ Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] x) (𝓝 (g x))
have this : Tendsto g (𝓝[<] x) (𝓝 (g x))
Tactic: have : Tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[<] x) (𝓝 (g x))
⊢ Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] x) (𝓝 (g x))
have apply : g =ᶠ[𝓝[<] x] fun (x : ℝ) ↦ deriv f x
Tactic: apply this.congr' _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[<] x) (𝓝 (g x))
⊢ g =ᶠ[𝓝[<] x] fun (x : ℝ) ↦ deriv f x
have apply : ∀ (y : ℝ) (hy : y ∈ Iio x), Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ g x = (fun (x : ℝ) ↦ deriv f x) x) x} y
Tactic: apply mem_of_superset self_mem_nhdsWithin fun y hy => _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
⊢ HasDerivAt f (g x) x
have B : HasDerivWithinAt f (g x) (Iic x) x
Tactic: have B : HasDerivWithinAt f (g x) (Iic x) x := by
    have diff : DifferentiableOn ℝ f (Iio x) := fun y hy =>
      (f_diff y (ne_of_lt hy)).differentiableAt.differentiableWithinAt
    -- next line is the nontrivial bit of this proof, appealing to differentiability
    -- extension results.
    apply
      hasDerivWithinAt_Iic_of_tendsto_deriv diff hf.continuousWithinAt
        self_mem_nhdsWithin
    have : Tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg
    apply this.congr' _
    apply mem_of_superset self_mem_nhdsWithin fun y hy => _
    intro y hy
    exact (f_diff y (ne_of_lt hy)).deriv.symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
⊢ HasDerivAt f (g y) y
have inl : ∀ (f_diff : ∀ (y_1 : ℝ), y_1 ≠ y → HasDerivAt f (g y_1) y_1) (hf : ContinuousAt f y) (hg : ContinuousAt g y),
  HasDerivAt f (g y) y
Tactic: rcases eq_or_ne y x with (rfl | hne)
Cleared hypotheses: x, f_diff, hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
inl :
  ∀ (f_diff : ∀ (y_1 : ℝ), y_1 ≠ y → HasDerivAt f (g y_1) y_1) (hf : ContinuousAt f y) (hg : ContinuousAt g y),
    HasDerivAt f (g y) y
⊢ HasDerivAt f (g y) y
have inr : ∀ (hne : y ≠ x), HasDerivAt f (g y) y
Tactic: rcases eq_or_ne y x with (rfl | hne)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Linear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
x : E
s : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑f : (a : E) → F) s x = f
have rw : fderiv 𝕜 (⇑f : (a : E) → F) x = f
Tactic: rw [DifferentiableAt.fderivWithin f.differentiableAt hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Linear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : IsBoundedLinearMap 𝕜 f
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 f s x = toContinuousLinearMap f h
have rw : fderiv 𝕜 f x = toContinuousLinearMap f h
Tactic: rw [DifferentiableAt.fderivWithin h.differentiableAt hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (A f L r ε)
have rw : ∀ x ∈ A f L r ε, ∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
Tactic: rw [Metric.isOpen_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
⊢ ∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
have obtain : ∀ (s : ℝ) (s_gt : r / 2 < s) (s_lt : s < r'), ∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
Tactic: obtain ⟨s, s_gt, s_lt⟩ : ∃ s : ℝ, r / 2 < s ∧ s < r' := exists_between r'_mem.1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
⊢ ∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
have this : s ∈ Ioc (r / 2) r
Tactic: have : s ∈ Ioc (r / 2) r := ⟨s_gt, le_of_lt (s_lt.trans_le r'_mem.2)⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
⊢ r' - s > 0
have linarith : r' - s ≤ 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
linarith : r' - s ≤ 0 → 2 / 2 = 1
⊢ r' - s > 0
have linarith₁ : r' - s ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
linarith : r' - s ≤ 0 → 2 / 2 = 1
linarith₁ : r' - s ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ r' - s > 0
have linarith₂ : r' - s ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
linarith : r' - s ≤ 0 → 2 / 2 = 1
linarith₁ : r' - s ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : r' - s ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ r' - s > 0
have linarith₃ : r' - s ≤ 0 → s - r' + (r' - s - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
⊢ ∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
have refine : ∀ (x' : E) (hx' : x' ∈ ball x (r' - s)),
  ∀ y ∈ ball x' s, ∀ z ∈ ball x' s, ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
Tactic: refine ⟨r' - s, by linarith, fun x' hx' => ⟨s, this, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
⊢ ∀ y ∈ ball x' s, ∀ z ∈ ball x' s, ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
have B : ball x' s ⊆ ball x r'
Tactic: have B : ball x' s ⊆ ball x r' := ball_subset (le_of_lt hx')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
⊢ x ∈ A f L r δ
have refine : ∀ (y : E) (hy : y ∈ ball x r') (z : E) (hz : z ∈ ball x r'), 0 ≤ r
Tactic: refine ⟨r', r'r, fun y hy z hz => (hr' y hy z hz).trans_le (mul_le_mul_of_nonneg_right h ?_)⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
y : E
hy : y ∈ ball x r'
z : E
hz : z ∈ ball x r'
⊢ 0 ≤ r
have linarith : r < 0 → r - 0 + (dist y x - r') + (r' - r) + (0 - dist y x) = 0
Tactic: linarith [mem_ball.1 hy, r'r.2, @dist_nonneg _ _ y x]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
r ε : ℝ
L : E →L[𝕜] F
x : E
hx : x ∈ A f L r ε
y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
⊢ ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ ≤ ε * r
have rcases : ∀ (r' : ℝ) (r'mem : r' ∈ Ioc (r / 2) r)
  (hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r),
  ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ ≤ ε * r
Tactic: rcases hx with ⟨r', r'mem, hr'⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
r ε : ℝ
L : E →L[𝕜] F
x y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
⊢ ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ ≤ ε * r
have hab : ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
Tactic: apply le_of_lt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ε
have obtain : ∀ (R : ℝ) (R_pos : R > 0)
  (hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖),
  ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ε
Tactic: obtain ⟨R, R_pos, hR⟩ :
      ∃ R > 0, ∀ y ∈ ball x R, ‖f y - f x - fderiv 𝕜 f x (y - x)‖ ≤ δ * ‖y - x‖ :=
    eventually_nhds_iff_ball.1 <| hx.hasFDerivAt.isLittleO.bound <| by positivity