awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
⊢ Tendsto.{u_4, u_3} (β := F) (fun (n : α) ↦ c n • (f (x + d n) - f x)) l (𝓝 ((f' : (a : E) → F) v) : Filter F)
have tendsto_arg : Tendsto (fun (n : α) ↦ x + d n) l (𝓝[s] x)
Tactic: have tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x) := by
    rw [tendsto_nhdsWithin_iff]
    exact ⟨by simpa using tendsto_const_nhds.add dlim, dtop⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
tendsto_arg : Tendsto (fun (n : α) ↦ x + d n) l (𝓝[s] x)
⊢ Tendsto.{u_4, u_3} (β := F) (fun (n : α) ↦ c n • (f (x + d n) - f x)) l (𝓝 ((f' : (a : E) → F) v) : Filter F)
have this : IsLittleOTVS.{u_1, u_4, u_3, u_1} 𝕜 (E := F) (F := 𝕜) l
  (fun (n : α) ↦ HSub.hSub (β := F) (c n • (f (x + d n) - f x)) ((f' : (a : E) → F) (c n • d n) : F)) 1
Tactic: have := calc
    (fun n ↦ c n • (f (x + d n) - f x) - f' (c n • d n)) =o[𝕜; l] fun n ↦ c n • d n := by
      simpa [smul_sub] using h.isLittleOTVS.comp_tendsto tendsto_arg |>.smul_left c
    _ =O[𝕜; l] (1 : α → 𝕜) := cdlim.isBigOTVS_one _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
tendsto_arg : Tendsto (fun (n : α) ↦ x + d n) l (𝓝[s] x)
this :
  IsLittleOTVS.{u_1, u_4, u_3, u_1} 𝕜 (E := F) (F := 𝕜) l
    (fun (n : α) ↦ HSub.hSub (β := F) (c n • (f (x + d n) - f x)) ((f' : (a : E) → F) (c n • d n) : F)) 1
⊢ Tendsto.{u_4, u_3} (β := F) (fun (n : α) ↦ c n • (f (x + d n) - f x)) l (𝓝 ((f' : (a : E) → F) v) : Filter F)
have this₁ : Tendsto.{u_4, u_3} (β := F)
  (fun (n : α) ↦ HSub.hSub (β := F) (c n • (f (x + d n) - f x)) ((f' : (a : E) → F) (c n • d n) : F)) l (𝓝 0)
Tactic: rw [isLittleOTVS_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
s : Set E
inst_11 : T2Space F
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt f f₁' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
⊢ Eq.{u_3 + 1} (α := F) ((f' : (a : E) → F) y : F) ((f₁' : (a : E) → F) y : F)
have rcases : ∀ (ι : Type (max u_1 u_2)) (l : Filter ι) (hl : l.NeBot) (c : ι → 𝕜) (d : ι → E) (hd₀ : Tendsto d l (𝓝 0))
  (hds : ∀ᶠ (n : ι) in l, x + d n ∈ s) (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)),
  Eq.{u_3 + 1} (α := F) ((f' : (a : E) → F) y : F) ((f₁' : (a : E) → F) y : F)
Tactic: rcases exists_fun_of_mem_tangentConeAt hy with ⟨ι, l, hl, c, d, hd₀, hds, hcd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
inst_11 : T2Space F
h₀ : HasFDerivAt f f' x
h₁ : HasFDerivAt f f₁' x
⊢ f' = f₁'
have h₂ : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝[univ] x) (pure x))
Tactic: rw [HasFDerivAt, ← nhdsWithin_univ] at *
Cleared hypotheses: h₀, h₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
inst_11 : T2Space F
h₀ : HasFDerivAt f f' x
h₁ : HasFDerivAt f f₁' x
h₂ : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝[univ] x) (pure x))
⊢ f' = f₁'
have h₃ : HasFDerivAtFilter f f₁' (SProd.sprod (β := Filter E) (𝓝[univ] x) (pure x))
Tactic: rw [HasFDerivAt, ← nhdsWithin_univ] at *
Cleared hypotheses: h₀, h₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
x : E
h : ¬DifferentiableAt 𝕜 f x
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x) 0
have rw : ¬DifferentiableWithinAt 𝕜 f univ x
Tactic: rw [fderiv, fderivWithin_zero_of_not_differentiableWithinAt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x
have rw : HasFDerivWithinAt f f' s x ↔ HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝 x) (pure x))
Tactic: rw [HasFDerivAt, HasFDerivWithinAt, nhdsWithin_eq_nhds.mpr h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
h : s ∈ 𝓝 x
rw : HasFDerivWithinAt f f' s x ↔ HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝 x) (pure x))
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x
have rw₁ : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝[s] x) (pure x)) ↔
  HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝 x) (pure x))
Tactic: rw [HasFDerivAt, HasFDerivWithinAt, nhdsWithin_eq_nhds.mpr h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
h : s ∈ 𝓝 x
rw : HasFDerivWithinAt f f' s x ↔ HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝 x) (pure x))
rw₁ :
  HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝[s] x) (pure x)) ↔
    HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝 x) (pure x))
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x
have rw₂ : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝 x) (pure x)) ↔
  HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝 x) (pure x))
Tactic: rw [HasFDerivAt, HasFDerivWithinAt, nhdsWithin_eq_nhds.mpr h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
⊢ HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x
have simp_rw : (IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[insert x s] x)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x) ↔
  IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[s] x)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x
Tactic: simp_rw [hasFDerivWithinAt_iff_isLittleOTVS]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
⊢ (IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[insert x s] x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x) ↔
    IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[s] x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x
have h : HSub.hSub (β := F) (f x - f x) ((f' : (a : E) → F) (x - x) : F) = 0
Tactic: apply isLittleOTVS_insert
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
⊢ HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
have inl : HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x
Tactic: rcases eq_or_ne x y with (rfl | h)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
inl : HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
have inr : ∀ (h : x ≠ y), HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
Tactic: rcases eq_or_ne x y with (rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
h : x ≠ y
⊢ HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
have inr : ∀ (hf : HasFDerivWithinAt f f' s x), s ∈ 𝓝[insert y s] x
Tactic: refine ⟨.of_insert, fun hf => hf.mono_of_mem_nhdsWithin ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
h : x ≠ y
hf : HasFDerivWithinAt f f' s x
⊢ s ∈ 𝓝[insert y s] x
have inr : s ∈ 𝓝[s] x
Tactic: simp_rw [nhdsWithin_insert_of_ne h, self_mem_nhdsWithin]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
⊢ HasFDerivWithinAt f f' (s \ {x}) x ↔ HasFDerivWithinAt f f' s x
have rw : HasFDerivWithinAt f f' (insert x (s \ {x})) x ↔ HasFDerivWithinAt f f' s x
Tactic: rw [← hasFDerivWithinAt_insert_self, insert_diff_singleton, hasFDerivWithinAt_insert_self]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
rw : HasFDerivWithinAt f f' (insert x (s \ {x})) x ↔ HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f f' (s \ {x}) x ↔ HasFDerivWithinAt f f' s x
have rw₁ : HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x
Tactic: rw [← hasFDerivWithinAt_insert_self, insert_diff_singleton, hasFDerivWithinAt_insert_self]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
rw : HasFDerivWithinAt f f' (insert x (s \ {x})) x ↔ HasFDerivWithinAt f f' s x
rw₁ : HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f f' (s \ {x}) x ↔ HasFDerivWithinAt f f' s x
have rw₂ : HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' s x
Tactic: rw [← hasFDerivWithinAt_insert_self, insert_diff_singleton, hasFDerivWithinAt_insert_self]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
⊢ HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x
have rw : HasFDerivWithinAt f f' (insert y (s \ {y})) x ↔ HasFDerivWithinAt f f' s x
Tactic: rw [← hasFDerivWithinAt_insert, insert_diff_singleton, hasFDerivWithinAt_insert]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
rw : HasFDerivWithinAt f f' (insert y (s \ {y})) x ↔ HasFDerivWithinAt f f' s x
rw₁ : E
⊢ HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x
have rw₂ : HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
Tactic: rw [← hasFDerivWithinAt_insert, insert_diff_singleton, hasFDerivWithinAt_insert]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
rw : HasFDerivWithinAt f f' (insert y (s \ {y})) x ↔ HasFDerivWithinAt f f' s x
rw₁ : E
rw₂ : HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x
have rw₃ : HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' s x
Tactic: rw [← hasFDerivWithinAt_insert, insert_diff_singleton, hasFDerivWithinAt_insert]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
h : s.Finite
⊢ HasFDerivWithinAt f f' s x
have empty : HasFDerivWithinAt f f' ∅ x
Tactic: induction s, h using Set.Finite.induction_on with
  | empty => exact .empty
  | insert _ _ ih => exact ih.insert'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
h : s.Finite
empty : HasFDerivWithinAt f f' ∅ x
⊢ HasFDerivWithinAt f f' s x
have insert : ∀ {a : E} {s : Set E}, a ∉ s → s.Finite → ∀ (ih : HasFDerivWithinAt f f' s x), HasFDerivWithinAt f f' (insert a s) x
Tactic: induction s, h using Set.Finite.induction_on with
  | empty => exact .empty
  | insert _ _ ih => exact ih.insert'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
⊢ Tendsto.{u_4, u_3} (β := F) (fun (n : α) ↦ c n • (f (x + (c n)⁻¹ • v) - f x)) l (𝓝 ((f' : (a : E) → F) v) : Filter F)
have refine_1 : Tendsto.{u_4, u_2} (β := E) (fun (n : α) ↦ (c n)⁻¹ • v) l (𝓝 0)
Tactic: refine (hasFDerivWithinAt_univ.2 hf).lim ?_ (.of_forall fun _ ↦ mem_univ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
refine_1 : Tendsto.{u_4, u_2} (β := E) (fun (n : α) ↦ (c n)⁻¹ • v) l (𝓝 0)
⊢ Tendsto.{u_4, u_3} (β := F) (fun (n : α) ↦ c n • (f (x + (c n)⁻¹ • v) - f x)) l (𝓝 ((f' : (a : E) → F) v) : Filter F)
have refine_2 : Tendsto (fun (n : α) ↦ c n • (c n)⁻¹ • v) l (𝓝 v)
Tactic: refine (hasFDerivWithinAt_univ.2 hf).lim ?_ (.of_forall fun _ ↦ mem_univ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
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 → F
f' : E →L[𝕜] F
x : E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
⊢ Tendsto.{u_4, u_2} (β := E) (fun (n : α) ↦ (c n)⁻¹ • v) l (𝓝 0)
have hc₁ : Tendsto c l (Bornology.cobounded 𝕜)
Tactic: rw [tendsto_norm_atTop_iff_cobounded] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
⊢ Tendsto (fun (n : α) ↦ c n • (c n)⁻¹ • v) l (𝓝 v)
have refine_2 : ∀ᶠ (x' : α) in l, c x' • (c x')⁻¹ • v = v
Tactic: refine tendsto_nhds_of_eventually_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
⊢ ∀ᶠ (x' : α) in l, c x' • (c x')⁻¹ • v = v
have refine_2 : ∀ (y : α) (hy : c y ≠ 0), c y • (c y)⁻¹ • v = v
Tactic: refine (eventually_ne_of_tendsto_norm_atTop hc (0 : 𝕜)).mono fun y hy => ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s t : Set E
hs : HasFDerivWithinAt f f' s x
ht : HasFDerivWithinAt f f' t x
⊢ HasFDerivWithinAt f f' (s ∪ t) x
have simp : ∀
  (hs :
    IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[s] x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x)
  (ht :
    IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[t] x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x),
  IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[s] x ⊔ 𝓝[t] x)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x
Tactic: simp only [hasFDerivWithinAt_iff_isLittleOTVS, nhdsWithin_union] at *
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hs : s ∈ 𝓝 x
⊢ HasFDerivAt f f' x
have rwa : ∀ (h : HasFDerivWithinAt f f' (univ ∩ s) x) (hs : s ∈ 𝓝 x), HasFDerivAt f f' x
Tactic: rwa [← univ_inter s, hasFDerivWithinAt_inter hs, hasFDerivWithinAt_univ] at h
Cleared hypotheses: h, hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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 → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hs : s ∈ 𝓝 x
rwa : ∀ (h : HasFDerivWithinAt f f' (univ ∩ s) x) (hs : s ∈ 𝓝 x), HasFDerivAt f f' x
⊢ HasFDerivAt f f' x
have rwa₁ : ∀ (h : HasFDerivWithinAt f f' univ x) (hs : s ∈ 𝓝 x), HasFDerivAt f f' x
Tactic: rwa [← univ_inter s, hasFDerivWithinAt_inter hs, hasFDerivWithinAt_univ] at h
Cleared hypotheses: h, hs