awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
f : E → F
x : E
s : Set E
g' : G → G'
g : F → G
t : Set F
u : Set G
y : F
y' : G
hg' : DifferentiableWithinAt 𝕜 g' u y'
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h2g : MapsTo g t u
h2f : MapsTo f s t
h3g : g y = y'
h3f : f x = y
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] G') (fderivWithin 𝕜 (g' ∘ g ∘ f) s x)
    (fderivWithin 𝕜 g' u y' ∘SL fderivWithin 𝕜 g t y ∘SL fderivWithin 𝕜 f s x)
have substs : ∀ (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hg' : DifferentiableWithinAt 𝕜 g' u (g (f x))),
  Eq (α := E →L[𝕜] G') (fderivWithin 𝕜 (g' ∘ g ∘ f) s x)
    (fderivWithin 𝕜 g' u (g (f x)) ∘SL fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)
Tactic: substs h3g h3f
Cleared hypotheses: y, y', hg', hg, h3g, h3f
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
⊢ HasFDerivAtFilter f^[n + 1] (f' ^ (n + 1)) L
have succ : HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') L
Tactic: rw [Function.iterate_succ, pow_succ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
⊢ HasFDerivAtFilter f^[n] (f' ^ n) L
have zero : HasFDerivAtFilter f^[0] (HPow.hPow (β := ℕ) f' 0) L
Tactic: induction n with
  | zero => exact hasFDerivAtFilter_id L
  | succ n ihn =>
    rw [Function.iterate_succ, pow_succ]
    exact ihn.comp hf hL
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
zero : HasFDerivAtFilter f^[0] (HPow.hPow (β := ℕ) f' 0) L
⊢ HasFDerivAtFilter f^[n] (f' ^ n) L
have succ : ∀ (n : ℕ) (ihn : HasFDerivAtFilter f^[n] (f' ^ n) L), HasFDerivAtFilter f^[n + 1] (f' ^ (n + 1)) L
Tactic: induction n with
  | zero => exact hasFDerivAtFilter_id L
  | succ n ihn =>
    rw [Function.iterate_succ, pow_succ]
    exact ihn.comp hf hL
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ HasFDerivAt f^[n] (f' ^ n) x
have refine : Tendsto (Prod.map f f) (SProd.sprod (β := Filter E) (𝓝 x) (pure x)) (SProd.sprod (β := Filter E) (𝓝 x) (pure x))
Tactic: refine HasFDerivAtFilter.iterate hf ?_ n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ HasFDerivWithinAt f^[n] (f' ^ n) s x
have refine : Tendsto (Prod.map f f) (SProd.sprod (β := Filter E) (𝓝[s] x) (pure x)) (SProd.sprod (β := Filter E) (𝓝[s] x) (pure x))
Tactic: refine HasFDerivAtFilter.iterate hf ?_ n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasStrictFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ HasStrictFDerivAt f^[n] (f' ^ n) x
have refine : Tendsto (Prod.map f f) (𝓝 (x, x)) (𝓝 (x, x))
Tactic: refine HasFDerivAtFilter.iterate hf ?_ n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.CompCLM (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Finite ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : (i : ι) → M i
m : E
⊢ Eq.{u_7 + 1} (α := H) ((fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) s x : (a : E) → H) m : H)
    ((((fderivWithin 𝕜 c s x : (a : E) → ContinuousMultilinearMap 𝕜 M H) m : ContinuousMultilinearMap 𝕜 M H) :
          (a : (i : ι) → M i) → H)
        u :
      H)
have have : ∀ (this : Fintype ι),
  Eq.{u_7 + 1} (α := H) ((fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) s x : (a : E) → H) m : H)
    ((((fderivWithin 𝕜 c s x : (a : E) → ContinuousMultilinearMap 𝕜 M H) m : ContinuousMultilinearMap 𝕜 M H) :
          (a : (i : ι) → M i) → H)
        u :
      H)
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.CompCLM (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Finite ι
hc : DifferentiableAt 𝕜 c x
u : (i : ι) → M i
m : E
⊢ Eq.{u_7 + 1} (α := H) ((fderiv 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) x : (a : E) → H) m : H)
    ((((fderiv 𝕜 c x : (a : E) → ContinuousMultilinearMap 𝕜 M H) m : ContinuousMultilinearMap 𝕜 M H) :
          (a : (i : ι) → M i) → H)
        u :
      H)
have have : ∀ (this : Fintype ι),
  Eq.{u_7 + 1} (α := H) ((fderiv 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) x : (a : E) → H) m : H)
    ((((fderiv 𝕜 c x : (a : E) → ContinuousMultilinearMap 𝕜 M H) m : ContinuousMultilinearMap 𝕜 M H) :
          (a : (i : ι) → M i) → H)
        u :
      H)
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.CompCLM (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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Finite ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : ι → F
m : E
⊢ Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) s x : (a : E) → G) m : G)
    ((((fderivWithin 𝕜 c s x : (a : E) → F [⋀^ι]→L[𝕜] G) m : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) u : G)
have have : ∀ (this : Fintype ι),
  Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) s x : (a : E) → G) m : G)
    ((((fderivWithin 𝕜 c s x : (a : E) → F [⋀^ι]→L[𝕜] G) m : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) u : G)
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.CompCLM (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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Finite ι
hc : DifferentiableAt 𝕜 c x
u : ι → F
m : E
⊢ Eq.{u_4 + 1} (α := G) ((fderiv 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) x : (a : E) → G) m : G)
    ((((fderiv 𝕜 c x : (a : E) → F [⋀^ι]→L[𝕜] G) m : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) u : G)
have have : ∀ (this : Fintype ι),
  Eq.{u_4 + 1} (α := G) ((fderiv 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) x : (a : E) → G) m : G)
    ((((fderiv 𝕜 c x : (a : E) → F [⋀^ι]→L[𝕜] G) m : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) u : G)
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Congr (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
h : s =ᶠ[𝓝[≠] x] t
⊢ HasFDerivWithinAt f f' (s \ {x}) x ↔ HasFDerivWithinAt f f' (t \ {x}) x
have suffices : 𝓝[s \ {x}] x = 𝓝[t \ {x}] x
Tactic: suffices 𝓝[s \ {x}] x = 𝓝[t \ {x}] x by simp only [HasFDerivWithinAt, this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Congr (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
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
have inl : ∀ (h : s =ᶠ[𝓝[≠] x] t), HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
Tactic: rcases eq_or_ne x y with rfl | hne
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Congr (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
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
inl : ∀ (h : s =ᶠ[𝓝[≠] x] t), HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
have inr : ∀ (hne : x ≠ y), HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
Tactic: rcases eq_or_ne x y with rfl | hne
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Congr (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 t : Set E
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hne : x ≠ y
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
have h₁ : s =ᶠ[𝓝 x] t
Tactic: rw [hne.nhdsWithin_compl_singleton] at h
Cleared hypotheses: h, hne
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Congr (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₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
L : Filter (E × E)
h₀ : Prod.map f₀ f₀ =ᶠ[L] Prod.map f₁ f₁
h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f₀' : (a : E) → F) x : F) ((f₁' : (a : E) → F) x : F)
⊢ HasFDerivAtFilter f₀ f₀' L ↔ HasFDerivAtFilter f₁ f₁' L
have simp : (IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) L
    (fun (p : E × E) ↦ HSub.hSub (β := F) (f₀ p.1 - f₀ p.2) ((f₀' : (a : E) → F) (p.1 - p.2) : F)) fun (p : E × E) ↦
    p.1 - p.2) ↔
  IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) L
    (fun (p : E × E) ↦ HSub.hSub (β := F) (f₁ p.1 - f₁ p.2) ((f₁' : (a : E) → F) (p.1 - p.2) : F)) fun (p : E × E) ↦
    p.1 - p.2
Tactic: simp only [hasFDerivAtFilter_iff_isLittleOTVS]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Congr (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 f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[insert x s] x] f
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ s x) (fderivWithin 𝕜 f s x)
have apply : f₁ x = f x
Tactic: apply Filter.EventuallyEq.fderivWithin_eq (nhdsWithin_mono _ (subset_insert x s) hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Congr (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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f₁ x) (fderiv 𝕜 f x)
have rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ univ x) (fderiv 𝕜 f x)
Tactic: rw [← fderivWithin_univ, ← fderivWithin_univ, h.fderivWithin_eq_of_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Congr (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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ univ x) (fderiv 𝕜 f x)
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f₁ x) (fderiv 𝕜 f x)
have rw₁ : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ univ x) (fderivWithin 𝕜 f univ x)
Tactic: rw [← fderivWithin_univ, ← fderivWithin_univ, h.fderivWithin_eq_of_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Congr (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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ univ x) (fderiv 𝕜 f x)
rw₁ : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ univ x) (fderivWithin 𝕜 f univ x)
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f₁ x) (fderiv 𝕜 f x)
have rw₂ : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f univ x) (fderivWithin 𝕜 f univ x)
Tactic: rw [← fderivWithin_univ, ← fderivWithin_univ, h.fderivWithin_eq_of_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
x : E
s : Set E
c : F
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ c) s x) 0
have hc : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ c) 0 s x
Tactic: rw [fderivWithin, if_pos]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
s : Set E
c : F
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ c) s) 0
have h : ∀ (x x_1 : E),
  Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 (fun (x : E) ↦ c) s x : (a : E) → F) x_1 : F) ((0 x : (a : E) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
s : Set E
c : F
x x_1 : E
⊢ Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 (fun (x : E) ↦ c) s x : (a : E) → F) x_1 : F) ((0 x : (a : E) → F) x_1 : F)
have h : Eq.{u_3 + 1} (α := F) ((0 : (a : E) → F) x_1 : F) ((0 x : (a : E) → F) x_1 : F)
Tactic: rw [fderivWithin_const_apply, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
s : Set E
c : F
x x_1 : E
h : Eq.{u_3 + 1} (α := F) ((0 : (a : E) → F) x_1 : F) ((0 x : (a : E) → F) x_1 : F)
⊢ Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 (fun (x : E) ↦ c) s x : (a : E) → F) x_1 : F) ((0 x : (a : E) → F) x_1 : F)
have h₁ : Eq.{u_3 + 1} (α := F) ((0 : (a : E) → F) x_1 : F) ((0 : (a : E) → F) x_1 : F)
Tactic: rw [fderivWithin_const_apply, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
x : E
c : F
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (x : E) ↦ c) x) 0
have rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ c) univ x) 0
Tactic: rw [fderiv, fderivWithin_const_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
x : E
c : F
rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ c) univ x) 0
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (x : E) ↦ c) x) 0
have rw₁ : Eq (α := E →L[𝕜] F) 0 0
Tactic: rw [fderiv, fderivWithin_const_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
c : F
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderiv 𝕜 fun (x : E) ↦ c) 0
have rw : Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ c) univ) 0
Tactic: rw [← fderivWithin_univ, fderivWithin_fun_const]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
c : F
rw : Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ c) univ) 0
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderiv 𝕜 fun (x : E) ↦ c) 0
have rw₁ : Eq (α := (x : E) → E →L[𝕜] F) 0 0
Tactic: rw [← fderivWithin_univ, fderivWithin_fun_const]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 {x} x
have refine : ¬AccPt x (𝓟 {x})
Tactic: refine .of_not_accPt ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
⊢ ¬AccPt x (𝓟 {x})
have rw : ¬ClusterPt x (𝓟 ({x}ᶜ ∩ {x}))
Tactic: rw [accPt_iff_clusterPt, inf_principal]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
h : Subsingleton E
f : E → F
s : Set E
x : E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x
have inl : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 ∅ x
Tactic: obtain rfl | ⟨a, rfl⟩ := s.eq_empty_or_singleton_of_subsingleton
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
h : Subsingleton E
f : E → F
s : Set E
x : E
inl : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 ∅ x
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x
have inr : ∀ (a : E), HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 {a} x
Tactic: obtain rfl | ⟨a, rfl⟩ := s.eq_empty_or_singleton_of_subsingleton
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x
have rw : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 {x} x
Tactic: rw [← hasFDerivWithinAt_univ, subsingleton_univ.eq_singleton_of_mem (mem_univ x)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
s : Set E
hf : Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f s x) : (a : E) → F)
⊢ DifferentiableWithinAt 𝕜 f s x
have a : Nontrivial E
Tactic: nontriviality E
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
hf : Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f s x) : (a : E) → F)
h : Nontrivial E
⊢ DifferentiableWithinAt 𝕜 f s x
have contrapose : ∀ (hf : ¬DifferentiableWithinAt 𝕜 f s x),
  ¬Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f s x) : (a : E) → F)
Tactic: contrapose hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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 : Nontrivial E
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f s x) : (a : E) → F)
have rw : ¬Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑0 : (a : E) → F)
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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
hf : Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderiv 𝕜 f x) : (a : E) → F)
⊢ DifferentiableAt 𝕜 f x
have simp : ∀ (hf : Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f univ x) : (a : E) → F)),
  DifferentiableWithinAt 𝕜 f univ x
Tactic: simp only [← differentiableWithinAt_univ, ← fderivWithin_univ] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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 : x ∉ tsupport f
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x
have h₁ : f =ᶠ[𝓝 x] 0
Tactic: rw [notMem_tsupport_iff_eventuallyEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (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 : x ∉ tsupport f
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x) 0
have h₁ : f =ᶠ[𝓝 x] 0
Tactic: rw [notMem_tsupport_iff_eventuallyEq] at h
Cleared hypotheses: h