awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rwa₁ : ∀ (h : HasFDerivWithinAt f f' univ x) (hs : s ∈ 𝓝 x), HasFDerivAt f f' x
⊢ HasFDerivAt f f' x
have rwa₂ : ∀ (h : HasFDerivAt f f' 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 (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
s : Set E
h : ¬AccPt x (𝓟 s)
⊢ HasFDerivWithinAt f f' s x
have h₁ : 𝓝[s \ {x}] x = ⊥
Tactic: rw [accPt_principal_iff_nhdsWithin, not_neBot] at h
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
h : 𝓝[s \ {x}] x = ⊥
⊢ HasFDerivWithinAt f f' s x
have rw : IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) ⊥
  (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x
Tactic: rw [← hasFDerivWithinAt_diff_singleton_self, hasFDerivWithinAt_iff_isLittleOTVS, 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
s : Set E
h : ¬AccPt x (𝓟 s)
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) 0
have rw : Eq (α := E →L[𝕜] F)
  (if HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x then 0
  else
    if h : DifferentiableWithinAt 𝕜 f s x then
      Classical.choose (p := fun (x_1 : E →L[𝕜] F) ↦ HasFDerivWithinAt f x_1 s x) h
    else 0)
  0
Tactic: rw [fderivWithin, if_pos (.of_not_accPt 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
s : Set E
h : ¬AccPt x (𝓟 s)
rw :
  Eq (α := E →L[𝕜] F)
    (if HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x then 0
    else
      if h : DifferentiableWithinAt 𝕜 f s x then
        Classical.choose (p := fun (x_1 : E →L[𝕜] F) ↦ HasFDerivWithinAt f x_1 s x) h
      else 0)
    0
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) 0
have rw₁ : Eq (α := E →L[𝕜] F) 0 0
Tactic: rw [fderivWithin, if_pos (.of_not_accPt 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
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x
have simp : HasFDerivWithinAt f
  (if HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x then 0
  else Classical.choose (p := fun (x_1 : E →L[𝕜] F) ↦ HasFDerivWithinAt f x_1 s x) h)
  s x
Tactic: simp only [fderivWithin, dif_pos 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
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
⊢ HasFDerivWithinAt f
    (if HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x then 0
    else Classical.choose (p := fun (x_1 : E →L[𝕜] F) ↦ HasFDerivWithinAt f x_1 s x) h)
    s x
have pos : ∀ (h₀ : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x), HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x
Tactic: split_ifs with 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
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
pos : ∀ (h₀ : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x), HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x
⊢ HasFDerivWithinAt f
    (if HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x then 0
    else Classical.choose (p := fun (x_1 : E →L[𝕜] F) ↦ HasFDerivWithinAt f x_1 s x) h)
    s x
have neg : ∀ (h₀ : ¬HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x),
  HasFDerivWithinAt f (Classical.choose (p := fun (x_1 : E →L[𝕜] F) ↦ HasFDerivWithinAt f x_1 s x) h) s x
Tactic: split_ifs with 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
⊢ HasFDerivAt f (fderiv 𝕜 f x) x
have rw : HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ x
Tactic: rw [fderiv, ← hasFDerivWithinAt_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
x : E
h : DifferentiableAt 𝕜 f x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ x
have h₁ : DifferentiableWithinAt 𝕜 f univ x
Tactic: rw [← differentiableWithinAt_univ] at h
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
inst_11 : T2Space F
h : HasFDerivAt f f' x
⊢ fderiv 𝕜 f x = f'
have rw : Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x) (fderiv 𝕜 f x)
Tactic: rw [h.unique h.differentiableAt.hasFDerivAt]
-- 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
s t : Set E
h : DifferentiableWithinAt 𝕜 f t x
st : s ⊆ t
⊢ DifferentiableWithinAt 𝕜 f s x
have rcases : ∀ (f' : E →L[𝕜] F) (hf' : HasFDerivWithinAt f f' t x), DifferentiableWithinAt 𝕜 f s x
Tactic: rcases h with ⟨f', hf'⟩
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
s : Set E
h : ∀ x ∈ s, ∃ (u : Set E), IsOpen[inst_3] u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
⊢ DifferentiableWithinAt 𝕜 f s x
have rcases : ∀ (t : Set E) (t_open : IsOpen[inst_3] t) (xt : x ∈ t) (ht : DifferentiableOn 𝕜 f (s ∩ t)),
  DifferentiableWithinAt 𝕜 f s x
Tactic: rcases h x xs with ⟨t, t_open, xt, 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
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderiv 𝕜 f x)
have rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f univ x)
Tactic: rw [← fderivWithin_univ, ← univ_inter s, fderivWithin_inter 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
s : Set E
h : s ∈ 𝓝 x
rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f univ x)
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderiv 𝕜 f x)
have rw₁ : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f (univ ∩ s) x) (fderivWithin 𝕜 f univ x)
Tactic: rw [← fderivWithin_univ, ← univ_inter s, fderivWithin_inter 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
s : Set E
h : s ∈ 𝓝 x
rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f univ x)
rw₁ : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f (univ ∩ s) x) (fderivWithin 𝕜 f univ x)
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderiv 𝕜 f x)
have rw₂ : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f univ x) (fderivWithin 𝕜 f univ x)
Tactic: rw [← fderivWithin_univ, ← univ_inter s, fderivWithin_inter 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
s : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableAt 𝕜 f x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderiv 𝕜 f x)
have rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f univ x)
Tactic: rw [← fderivWithin_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
s : Set (E →L[𝕜] F)
x : E
⊢ fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
have pos : ∀ (hx : DifferentiableAt 𝕜 f x),
  fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
Tactic: by_cases hx : DifferentiableAt 𝕜 f x
-- 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
s : Set (E →L[𝕜] F)
x : E
pos :
  ∀ (hx : DifferentiableAt 𝕜 f x),
    fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
⊢ fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
have neg : ∀ (hx : ¬DifferentiableAt 𝕜 f x),
  fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
Tactic: by_cases hx : DifferentiableAt 𝕜 f x
-- 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
t : Set E
s : Set (E →L[𝕜] F)
x : E
⊢ fderivWithin 𝕜 f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
have pos : ∀ (hx : DifferentiableWithinAt 𝕜 f t x),
  fderivWithin 𝕜 f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
Tactic: by_cases hx : DifferentiableWithinAt 𝕜 f t x
-- 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
t : Set E
s : Set (E →L[𝕜] F)
x : E
pos :
  ∀ (hx : DifferentiableWithinAt 𝕜 f t x),
    fderivWithin 𝕜 f t x ∈ s ↔
      DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
⊢ fderivWithin 𝕜 f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
have neg : ∀ (hx : ¬DifferentiableWithinAt 𝕜 f t x),
  fderivWithin 𝕜 f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
Tactic: by_cases hx : DifferentiableWithinAt 𝕜 f t x
-- 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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
x : E
hx : x ∈ s ∪ t
⊢ DifferentiableWithinAt 𝕜 f (s ∪ t) x
have inl : ∀ (hx : x ∈ s), DifferentiableWithinAt 𝕜 f (s ∪ t) x
Tactic: obtain (hx | hx) := hx
Cleared hypotheses: hx
-- 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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
x : E
hx : x ∈ s ∪ t
inl : ∀ (hx : x ∈ s), DifferentiableWithinAt 𝕜 f (s ∪ t) x
⊢ DifferentiableWithinAt 𝕜 f (s ∪ t) x
have inr : ∀ (hx : x ∈ t), DifferentiableWithinAt 𝕜 f (s ∪ t) x
Tactic: obtain (hx | hx) := hx
Cleared hypotheses: hx
-- 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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hst : s ∪ t = univ
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
⊢ Differentiable 𝕜 f
have rw : DifferentiableOn 𝕜 f (s ∪ t)
Tactic: rw [← differentiableOn_univ, ← hst]
-- 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
ι : Type u_4
s : ι → Set E
hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
hs : ∀ (i : ι), IsOpen[inst_3] (s i)
hs' : Eq.{u_2 + 1} (α := Set E) (⋃ (i : ι), s i) univ
⊢ Differentiable 𝕜 f
have rw : DifferentiableOn 𝕜 f (⋃ (i : ι), s i)
Tactic: rw [← differentiableOn_univ, ← 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
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L (pure x))
⊢ IsLittleOTVS.{u_1, u_2, u_3, u_1} 𝕜 (E := F) (F := 𝕜) L (fun (x_1 : E) ↦ f x_1 - f x) 1
have refine : IsLittleOTVS 𝕜 (E := E) (F := 𝕜) L ((fun (p : E × E) ↦ p.1 - p.2) ∘ fun (a : E) ↦ (a, x)) 1
Tactic: refine h.isBigOTVS_sub |>.comp_tendsto prod_pure.ge |>.trans_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
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L (pure x))
⊢ IsLittleOTVS 𝕜 (E := E) (F := 𝕜) L ((fun (p : E × E) ↦ p.1 - p.2) ∘ fun (a : E) ↦ (a, x)) 1
have rw : Tendsto (β := E) ((fun (p : E × E) ↦ p.1 - p.2) ∘ fun (a : E) ↦ (a, x)) L (𝓝 0)
Tactic: rw [isLittleOTVS_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
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
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L (pure x))
⊢ Tendsto f L (𝓝 (f x))
have this : IsLittleOTVS.{u_1, u_2, u_3, u_1} 𝕜 (E := F) (F := 𝕜) L (fun (x_1 : E) ↦ f x_1 - f x) 1
Tactic: have : (f · - f x) =o[𝕜; L] (1 : E → 𝕜) := by
    refine h.isBigOTVS_sub |>.comp_tendsto prod_pure.ge |>.trans_isLittleOTVS ?_
    rw [isLittleOTVS_one]
    simpa [sub_eq_add_neg] using (tendsto_id'.mpr hL).add_const (-x)
-- 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
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L (pure x))
this : IsLittleOTVS.{u_1, u_2, u_3, u_1} 𝕜 (E := F) (F := 𝕜) L (fun (x_1 : E) ↦ f x_1 - f x) 1
⊢ Tendsto f L (𝓝 (f x))
have this₁ : Tendsto.{u_2, u_3} (β := F) (fun (x_1 : E) ↦ f x_1 - f x) 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
x : E
s : Set E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 id s x) (ContinuousLinearMap.id 𝕜 E)
have rw : Eq (α := E →L[𝕜] E) (fderiv 𝕜 id x) (ContinuousLinearMap.id 𝕜 E)
Tactic: rw [DifferentiableAt.fderivWithin differentiableAt_id hxs]
-- 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 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsEquivalent.{u_2, u_3} (E' := F) L (fun (p : E × E) ↦ f p.1 - f p.2) fun (p : E × E) ↦ (f' : (a : E) → F) (p.1 - p.2)
have rw : IsLittleOTVS 𝕜 (F := F) L
  (HSub.hSub (α := E × E → F) (fun (p : E × E) ↦ f p.1 - f p.2) fun (p : E × E) ↦ (f' : (a : E) → F) (p.1 - p.2))
  fun (p : E × E) ↦ (f' : (a : E) → F) (p.1 - p.2)
Tactic: rw [IsEquivalent, ← isLittleOTVS_iff_isLittleO (𝕜 := 𝕜)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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
f' : E →L[𝕜] F
L : Filter (E × E)
⊢ HasFDerivAtFilter f f' L ↔
    Tendsto (β := ℝ)
      (fun (p : E × E) ↦ ‖p.1 - p.2‖⁻¹ * ‖HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)‖) L
      (𝓝 0)
have rw : Tendsto (β := ℝ)
    (fun (x : E × E) ↦ ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ / ‖x.1 - x.2‖) L
    (𝓝 0) ↔
  Tendsto (β := ℝ)
    (fun (p : E × E) ↦ ‖p.1 - p.2‖⁻¹ * ‖HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)‖) L
    (𝓝 0)
Tactic: rw [hasFDerivAtFilter_iff_isLittleO, ← isLittleO_norm_left, ← isLittleO_norm_right,
    isLittleO_iff_tendsto]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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
f' : E →L[𝕜] F
L : Filter (E × E)
rw :
  Tendsto (β := ℝ)
      (fun (x : E × E) ↦ ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ / ‖x.1 - x.2‖) L
      (𝓝 0) ↔
    Tendsto (β := ℝ)
      (fun (p : E × E) ↦ ‖p.1 - p.2‖⁻¹ * ‖HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)‖) L
      (𝓝 0)
⊢ HasFDerivAtFilter f f' L ↔
    Tendsto (β := ℝ)
      (fun (p : E × E) ↦ ‖p.1 - p.2‖⁻¹ * ‖HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)‖) L
      (𝓝 0)
have rw₁ : ∀ (x : E × E), ‖x.1 - x.2‖ = 0 → ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ = 0
Tactic: rw [hasFDerivAtFilter_iff_isLittleO, ← isLittleO_norm_left, ← isLittleO_norm_right,
    isLittleO_iff_tendsto]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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
f' : E →L[𝕜] F
x : E
⊢ HasFDerivAt f f' x ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝 x) (𝓝 0)
have rw : HasFDerivWithinAt f f' univ x ↔
  Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
    (𝓝 x) (𝓝 0)
Tactic: rw [← hasFDerivWithinAt_univ, hasFDerivWithinAt_iff_tendsto, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (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
f' : E →L[𝕜] F
x : E
rw :
  HasFDerivWithinAt f f' univ x ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝 x) (𝓝 0)
⊢ HasFDerivAt f f' x ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝 x) (𝓝 0)
have rw₁ : Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
    (𝓝[univ] x) (𝓝 0) ↔
  Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
    (𝓝 x) (𝓝 0)
Tactic: rw [← hasFDerivWithinAt_univ, hasFDerivWithinAt_iff_tendsto, nhdsWithin_univ]