awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this_1 : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this : ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)
rwa : {f x}ᶜ ∈ map f (𝓝[s \ {x}] x)
rwa₁ : ∀ᶠ (x_1 : F) in map f (𝓝[s \ {x}] x), Membership.mem (γ := Set F) {f x}ᶜ x_1
⊢ map f (𝓝[s \ {x}] x) ≤ 𝓟 {f x}ᶜ
have rwa₂ : ∀ᶠ (a : E) in 𝓝[s \ {x}] x, Membership.mem (γ := Set F) {f x}ᶜ (f a)
Tactic: rwa [le_principal_iff, ← eventually_mem_set, eventually_map, diff_eq, nhdsWithin_inter',
    eventually_inf_principal]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this_1 : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this : ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)
rwa : {f x}ᶜ ∈ map f (𝓝[s \ {x}] x)
rwa₁ : ∀ᶠ (x_1 : F) in map f (𝓝[s \ {x}] x), Membership.mem (γ := Set F) {f x}ᶜ x_1
rwa₂ : ∀ᶠ (a : E) in 𝓝[s \ {x}] x, Membership.mem (γ := Set F) {f x}ᶜ (f a)
⊢ map f (𝓝[s \ {x}] x) ≤ 𝓟 {f x}ᶜ
have rwa₃ : ∀ᶠ (a : E) in 𝓝[s ∩ {x}ᶜ] x, Membership.mem (γ := Set F) {f x}ᶜ (f a)
Tactic: rwa [le_principal_iff, ← eventually_mem_set, eventually_map, diff_eq, nhdsWithin_inter',
    eventually_inf_principal]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this_1 : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this : ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)
rwa : {f x}ᶜ ∈ map f (𝓝[s \ {x}] x)
rwa₁ : ∀ᶠ (x_1 : F) in map f (𝓝[s \ {x}] x), Membership.mem (γ := Set F) {f x}ᶜ x_1
rwa₂ : ∀ᶠ (a : E) in 𝓝[s \ {x}] x, Membership.mem (γ := Set F) {f x}ᶜ (f a)
rwa₃ : ∀ᶠ (a : E) in 𝓝[s ∩ {x}ᶜ] x, Membership.mem (γ := Set F) {f x}ᶜ (f a)
⊢ map f (𝓝[s \ {x}] x) ≤ 𝓟 {f x}ᶜ
have rwa₄ : ∀ᶠ (a : E) in 𝓝[s] x ⊓ 𝓟 {x}ᶜ, Membership.mem (γ := Set F) {f x}ᶜ (f a)
Tactic: rwa [le_principal_iff, ← eventually_mem_set, eventually_map, diff_eq, nhdsWithin_inter',
    eventually_inf_principal]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
⊢ ∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ≠ c
have rw : ∀ᶠ (b : F) in map f (𝓝[s \ {x}] x), b ≠ c
Tactic: rw [← eventually_map (m := f) (P := fun z ↦ z ≠ c)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
⊢ ∀ᶠ (b : F) in map f (𝓝[s \ {x}] x), b ≠ c
have apply : ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c
Tactic: apply Eventually.filter_mono (h.tendsto_nhdsWithin_nhdsNE hf')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
⊢ ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c
have inl : ∀ᶠ (x_1 : F) in 𝓝[≠] f x, x_1 ≠ f x
Tactic: rcases eq_or_ne (f x) c with rfl | hc
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
inl : ∀ᶠ (x_1 : F) in 𝓝[≠] f x, x_1 ≠ f x
⊢ ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c
have inr : ∀ (hc : f x ≠ c), ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c
Tactic: rcases eq_or_ne (f x) c with rfl | hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
⊢ ∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ∉ t
have ht₁ : ∀ᶠ (x : F) in 𝓝[≠] f x, x ∉ t
Tactic: rw [accPt_iff_frequently_nhdsNE, not_frequently] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖) L
      (𝓝 0) ↔
    Tendsto.{u_1, u_2} (β := F)
      (fun (x' : E) ↦ ‖x' - x‖⁻¹ • HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) L (𝓝 0)
have symm : Tendsto.{u_1, u_2} (β := F)
    (fun (x' : E) ↦ ‖x' - x‖⁻¹ • HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) L (𝓝 0) ↔
  Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖) L
    (𝓝 0)
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto.{u_1, u_2} (β := F)
      (fun (x' : E) ↦ ‖x' - x‖⁻¹ • HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) L (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖) L
      (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (e : E) ↦ ‖‖e - x‖⁻¹ • HSub.hSub (β := F) (f e - f x) ((f' : (a : E) → F) (e - x) : F) - 0‖) L
    (𝓝 0) ↔
  Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖) L
    (𝓝 0)
Tactic: rw [tendsto_iff_norm_sub_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (β := ℝ) (fun (e : E) ↦ ‖‖e - x‖⁻¹ • HSub.hSub (β := F) (f e - f x) ((f' : (a : E) → F) (e - x) : F) - 0‖) L
      (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖) L
      (𝓝 0)
have refine : ∀ (x' : E),
  ‖‖x' - x‖⁻¹ • HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F) - 0‖ =
    ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖
Tactic: refine tendsto_congr fun x' => ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
hf : HasFDerivAt f f' x
v : E
⊢ Tendsto.{0, u_2} (β := F) (fun (c : ℝ) ↦ c • (f (x + c⁻¹ • v) - f x)) atTop (𝓝 ((f' : (a : E) → F) v) : Filter F)
have apply : Tendsto (β := ℝ) (fun (n : ℝ) ↦ ‖n‖) atTop atTop
Tactic: apply hf.lim v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
hf : HasFDerivAt f f' x
v : E
⊢ Tendsto (β := ℝ) (fun (n : ℝ) ↦ ‖n‖) atTop atTop
have rw : ∀ (b : ℝ), ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → b ≤ ‖a‖
Tactic: rw [tendsto_atTop_atTop]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
⊢ Membership.mem (α := F) (tangentConeAt 𝕜 (f '' s) (f x)) ((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)),
  Membership.mem (α := F) (tangentConeAt 𝕜 (f '' s) (f x)) ((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.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : 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)
⊢ Membership.mem (α := F) (tangentConeAt 𝕜 (f '' s) (f x)) ((f' : (a : E) → F) y : F)
have hd₁ : Tendsto (β := F) (fun (n : ι) ↦ f (x + d n) - f x) l (𝓝 0)
Tactic: apply mem_tangentConeAt_of_seq l c (fun n ↦ f (x + d n) - f x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : 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)
hd₁ : Tendsto (β := F) (fun (n : ι) ↦ f (x + d n) - f x) l (𝓝 0)
⊢ Membership.mem (α := F) (tangentConeAt 𝕜 (f '' s) (f x)) ((f' : (a : E) → F) y : F)
have hds₁ : ∀ᶠ (n : ι) in l, f x + (f (x + d n) - f x) ∈ f '' s
Tactic: apply mem_tangentConeAt_of_seq l c (fun n ↦ f (x + d n) - f x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : 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)
hd₁ : Tendsto (β := F) (fun (n : ι) ↦ f (x + d n) - f x) l (𝓝 0)
hds₁ : ∀ᶠ (n : ι) in l, f x + (f (x + d n) - f x) ∈ f '' s
⊢ Membership.mem (α := F) (tangentConeAt 𝕜 (f '' s) (f x)) ((f' : (a : E) → F) y : F)
have hcd₁ : Tendsto (β := F) (fun (n : ι) ↦ c n • (f (x + d n) - f x)) l (𝓝 ((f' : (a : E) → F) y) : Filter F)
Tactic: apply mem_tangentConeAt_of_seq l c (fun n ↦ f (x + d n) - f x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : 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)
⊢ Tendsto (β := F) (fun (n : ι) ↦ f (x + d n) - f x) l (𝓝 0)
have hd₁ : Tendsto (fun (n : ι) ↦ f (x + d n)) l (𝓝 (f x))
Tactic: rw [tendsto_sub_nhds_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : 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)
⊢ Tendsto (fun (n : ι) ↦ f (x + d n)) l (𝓝 (f x))
have hd₁ : Tendsto (fun (n : ι) ↦ x + d n) l (𝓝 x)
Tactic: refine h.continuousWithinAt.tendsto.comp <| tendsto_nhdsWithin_iff.mpr ⟨?_, hds⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
hs : UniqueDiffWithinAt 𝕜 s x
h' : DenseRange.{u_3, u_2} (X := F) (α := E) (⇑f' : (a : E) → F)
⊢ UniqueDiffWithinAt 𝕜 (f '' s) (f x)
have refine : MapsTo (⇑f' : (a : E) → F) (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E)
  (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x))) : Set F)
Tactic: refine ⟨h'.dense_of_mapsTo f'.continuous hs.1 ?_, h.continuousWithinAt.mem_closure_image hs.2⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
hs : UniqueDiffWithinAt 𝕜 s x
h' : DenseRange.{u_3, u_2} (X := F) (α := E) (⇑f' : (a : E) → F)
⊢ MapsTo (⇑f' : (a : E) → F) (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E)
    (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x))) : Set F)
have 𝕜₁ : Submodule.span 𝕜 (tangentConeAt 𝕜 s x) ≤
  Submodule.comap (↑f' : E →ₗ[𝕜] F) (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x)))
Tactic: change
    Submodule.span 𝕜 (tangentConeAt 𝕜 s x) ≤
      (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x))).comap f'.toLinearMap
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
hs : UniqueDiffWithinAt 𝕜 s x
h' : DenseRange.{u_3, u_2} (X := F) (α := E) (⇑f' : (a : E) → F)
⊢ Submodule.span 𝕜 (tangentConeAt 𝕜 s x) ≤
    Submodule.comap (↑f' : E →ₗ[𝕜] F) (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x)))
have rw : tangentConeAt 𝕜 s x ⊆ (↑(Submodule.comap (↑f' : E →ₗ[𝕜] F) (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x)))) : Set E)
Tactic: rw [Submodule.span_le]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
e : F ≃L[𝕜] E
⊢ UniqueDiffOn.{u_1, u_3} 𝕜 (E := F) ((⇑e : (a : F) → E) ⁻¹' s) ↔ UniqueDiffOn 𝕜 s
have rw : UniqueDiffOn.{u_1, u_3} 𝕜 (E := F) ((⇑e.symm : (a : E) → F) '' s) ↔ UniqueDiffOn 𝕜 s
Tactic: rw [← e.image_symm_eq_preimage, e.symm.uniqueDiffOn_image_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
e : F ≃L[𝕜] E
rw : UniqueDiffOn.{u_1, u_3} 𝕜 (E := F) ((⇑e.symm : (a : E) → F) '' s) ↔ UniqueDiffOn 𝕜 s
⊢ UniqueDiffOn.{u_1, u_3} 𝕜 (E := F) ((⇑e : (a : F) → E) ⁻¹' s) ↔ UniqueDiffOn 𝕜 s
have rw₁ : UniqueDiffOn 𝕜 s ↔ UniqueDiffOn 𝕜 s
Tactic: rw [← e.image_symm_eq_preimage, e.symm.uniqueDiffOn_image_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)
have inl : HasFDerivWithinAt (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) (HSMul.hSMul (α := 𝕜) 0 f') s x ↔
  HasFDerivWithinAt f f' (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)
Tactic: rcases eq_or_ne c 0 with rfl | hc
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
inl :
  HasFDerivWithinAt (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) (HSMul.hSMul (α := 𝕜) 0 f') s x ↔
    HasFDerivWithinAt f f' (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)
have inr : ∀ (hc : c ≠ 0), HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)
Tactic: rcases eq_or_ne c 0 with rfl | hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
hc : c ≠ 0
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)
have inr : ∀ (c : 𝕜ˣ) (hc : (↑c : 𝕜) ≠ 0),
  HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x ↔
    HasFDerivWithinAt f f' ((↑c : 𝕜) • s) ((↑c : 𝕜) • x)
Tactic: lift c to 𝕜ˣ using IsUnit.mk0 c hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : (↑c : 𝕜) ≠ 0
⊢ f' ∘SL (↑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c) : E →L[𝕜] E) = c • f'
have h : ∀ (x : E),
  Eq.{u_3 + 1} (α := F)
    ((f' ∘SL (↑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c) : E →L[𝕜] E) : (a : E) → F) x : F)
    ((c • f' : (a : E) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : (↑c : 𝕜) ≠ 0
⊢ HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x ↔
    HasFDerivWithinAt f f' ((↑c : 𝕜) • s) ((↑c : 𝕜) • x)
have A : f' ∘SL (↑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c) : E →L[𝕜] E) = c • f'
Tactic: have A : f'.comp ((ContinuousLinearEquiv.smulLeft c : E ≃L[𝕜] E) : E →L[𝕜] E) = c • f' := by
      ext; simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : (↑c : 𝕜) ≠ 0
A : f' ∘SL (↑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c) : E →L[𝕜] E) = c • f'
⊢ HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x ↔
    HasFDerivWithinAt f f' ((↑c : 𝕜) • s) ((↑c : 𝕜) • x)
have inr : HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x ↔
  HasFDerivWithinAt (f ∘ (⇑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c : E ≃L[𝕜] E) : (a : E) → E))
    (c • f')
    ((⇑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c : E ≃L[𝕜] E) : (a : E) → E) ⁻¹' ((↑c : 𝕜) • s)) x
Tactic: rw [← Units.smul_def c x, ← ContinuousLinearEquiv.smulLeft_apply_apply (R₁ := 𝕜),
      ← ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, A]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
hc : c ≠ 0
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) f' s x ↔ HasFDerivWithinAt (c • f) f' (c • s) (c • x)
have simp : HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) f' s x ↔ HasFDerivWithinAt (fun (x : E) ↦ c • f (c • x)) (c • f') s x
Tactic: simp only [← hasFDerivWithinAt_comp_smul_smul_iff, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
hc : c ≠ 0
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) f' s x ↔ HasFDerivWithinAt (fun (x : E) ↦ c • f (c • x)) (c • f') s x
have lift : ∀ (c : 𝕜ˣ) (hc : (↑c : 𝕜) ≠ 0),
  HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) f' s x ↔
    HasFDerivWithinAt (fun (x : E) ↦ (↑c : 𝕜) • f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x
Tactic: lift c to 𝕜ˣ using IsUnit.mk0 c hc
Cleared hypotheses: c, hc