awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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 : ∀ᶠ (x : F) in 𝓝[≠] f x, x ∉ t
⊢ ∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ∉ t

Tactic:
eventually_map.mp (ht.filter_mono (h.tendsto_nhdsWithin_nhdsNE hf'))

Premises used: Filter.Eventually.filter_mono, Filter.eventually_map, HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNE, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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 : ∀ᶠ (x : F) in 𝓝[≠] f x, x ∉ t
⊢ ∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ∉ t

Tactic:
exact eventually_map.mp (ht.filter_mono (h.tendsto_nhdsWithin_nhdsNE hf'))

Premises used: Filter.Eventually.filter_mono, Filter.eventually_map, HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNE, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
h : HasFDerivAt f f' x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
⊢ Tendsto f (𝓝[≠] x) (𝓝[≠] f x)

Tactic:
simpa only [compl_eq_univ_diff] using (hasFDerivWithinAt_univ.2 h).tendsto_nhdsWithin_nhdsNE hf'

Premises used: Iff.mpr, HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNE, Set.compl_eq_univ_diff, hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
c : F
h : HasFDerivAt f f' x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
⊢ ∀ᶠ (z : E) in 𝓝[≠] x, f z ≠ c

Tactic:
simpa only [compl_eq_univ_diff] using (hasFDerivWithinAt_univ.2 h).eventually_ne hf'

Premises used: Iff.mpr, HasFDerivWithinAt.eventually_ne, Set.compl_eq_univ_diff, hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
h : HasFDerivAt f f' 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 𝓝[≠] x, f z ∉ t

Tactic:
simpa only [compl_eq_univ_diff] using (hasFDerivWithinAt_univ.2 h).eventually_notMem hf' t ht

Premises used: Iff.mpr, HasFDerivWithinAt.eventually_notMem, Set.compl_eq_univ_diff, hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
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)
⊢ 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)

Tactic:
symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
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)
⊢ 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:
rw [tendsto_iff_norm_sub_tendsto_zero]

Premises used: tendsto_iff_norm_sub_tendsto_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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)

Tactic:
tendsto_congr fun x' => ?_

Premises used: Filter.tendsto_congr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
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)‖
⊢ 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:
refine tendsto_congr fun x' => ?_

Premises used: Filter.tendsto_congr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
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:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
apply : Tendsto (β := ℝ) (fun (n : ℝ) ↦ ‖n‖) atTop atTop
⊢ Tendsto.{0, u_2} (β := F) (fun (c : ℝ) ↦ c • (f (x + c⁻¹ • v) - f x)) atTop (𝓝 ((f' : (a : E) → F) v) : Filter F)

Tactic:
apply hf.lim v

Premises used: HasFDerivAt.lim
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
rw : ∀ (b : ℝ), ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → b ≤ ‖a‖
⊢ Tendsto (β := ℝ) (fun (n : ℝ) ↦ ‖n‖) atTop atTop

Tactic:
rw [tendsto_atTop_atTop]

Premises used: Filter.tendsto_atTop_atTop
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
⊢ ∀ (b : ℝ), ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → b ≤ ‖a‖

Tactic:
fun b => ⟨b, fun a ha => le_trans ha (le_abs_self _)⟩

Premises used: le_abs_self, Exists.intro, le_trans
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
⊢ ∀ (b : ℝ), ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → b ≤ ‖a‖

Tactic:
exact fun b => ⟨b, fun a ha => le_trans ha (le_abs_self _)⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
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)
⊢ 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⟩

Premises used: exists_fun_of_mem_tangentConeAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
hcd₁ : Tendsto (β := F) (fun (n : ι) ↦ c n • (f (x + d n) - f x)) l (𝓝 ((f' : (a : E) → F) y) : Filter F)
⊢ Membership.mem (α := F) (tangentConeAt 𝕜 (f '' s) (f x)) ((f' : (a : E) → F) y : F)

Tactic:
apply mem_tangentConeAt_of_seq l c (fun n ↦ f (x + d n) - f x)

Premises used: HSub.hSub, HAdd.hAdd, mem_tangentConeAt_of_seq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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 (fun (n : ι) ↦ f (x + d n)) l (𝓝 (f x))
⊢ Tendsto (β := F) (fun (n : ι) ↦ f (x + d n) - f x) l (𝓝 0)

Tactic:
rw [tendsto_sub_nhds_zero_iff]

Premises used: tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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))

Tactic:
h.continuousWithinAt.tendsto.comp <| tendsto_nhdsWithin_iff.mpr ⟨?_, hds⟩

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, And.intro, HasFDerivWithinAt.continuousWithinAt, Filter.Tendsto.comp, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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 (fun (n : ι) ↦ x + d n) l (𝓝 x)
⊢ Tendsto (fun (n : ι) ↦ f (x + d n)) l (𝓝 (f x))

Tactic:
refine h.continuousWithinAt.tendsto.comp <| tendsto_nhdsWithin_iff.mpr ⟨?_, hds⟩

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, And.intro, HasFDerivWithinAt.continuousWithinAt, Filter.Tendsto.comp, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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 : ι) ↦ x + d n) l (𝓝 x)

Tactic:
simpa using tendsto_const_nhds.add hd₀

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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)
n : ι
hn : x + d n ∈ s
⊢ f (x + d n) = f x + (f (x + d n) - f x)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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)
⊢ ∀ᶠ (n : ι) in l, f x + (f (x + d n) - f x) ∈ f '' s

Tactic:
exact hds.mono fun n hn ↦ ⟨x + d n, hn, by simp⟩

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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 : ι) ↦ c n • (f (x + d n) - f x)) l (𝓝 ((f' : (a : E) → F) y) : Filter F)

Tactic:
h.lim hd₀ hds hcd

Premises used: HasFDerivWithinAt.lim
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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 : ι) ↦ c n • (f (x + d n) - f x)) l (𝓝 ((f' : (a : E) → F) y) : Filter F)

Tactic:
exact h.lim hd₀ hds hcd

Premises used: HasFDerivWithinAt.lim
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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)

Tactic:
⟨h'.dense_of_mapsTo f'.continuous hs.1 ?_, h.continuousWithinAt.mem_closure_image hs.2⟩

Premises used: DenseRange.dense_of_mapsTo, ContinuousWithinAt.mem_closure_image, UniqueDiffWithinAt.dense_tangentConeAt, ContinuousLinearMap.continuous, UniqueDiffWithinAt.mem_closure, UniqueDiffWithinAt.mk, HasFDerivWithinAt.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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)
refine :
  MapsTo (⇑f' : (a : E) → F) (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E)
    (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x))) : Set F)
⊢ UniqueDiffWithinAt 𝕜 (f '' s) (f x)

Tactic:
refine ⟨h'.dense_of_mapsTo f'.continuous hs.1 ?_, h.continuousWithinAt.mem_closure_image hs.2⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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)))
⊢ MapsTo (⇑f' : (a : E) → F) (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E)
    (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x))) : Set F)

Tactic:
change
    Submodule.span 𝕜 (tangentConeAt 𝕜 s x) ≤
      (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x))).comap f'.toLinearMap

Premises used: ContinuousLinearMap.toLinearMap, Submodule.comap, Submodule.span, tangentConeAt, Set.image
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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)
rw :
  tangentConeAt 𝕜 s x ⊆
    (↑(Submodule.comap (↑f' : E →ₗ[𝕜] F) (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x)))) : Set E)
⊢ Submodule.span 𝕜 (tangentConeAt 𝕜 s x) ≤
    Submodule.comap (↑f' : E →ₗ[𝕜] F) (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x)))

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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)
⊢ tangentConeAt 𝕜 s x ⊆
    (↑(Submodule.comap (↑f' : E →ₗ[𝕜] F) (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x)))) : Set E)

Tactic:
h.mapsTo_tangent_cone.mono Subset.rfl Submodule.subset_span

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.MapsTo.mono, HasFDerivWithinAt.mapsTo_tangent_cone, Set.Subset, Set.Subset.rfl, Set.preimage, Set.MapsTo, Submodule.subset_span
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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)
⊢ tangentConeAt 𝕜 s x ⊆
    (↑(Submodule.comap (↑f' : E →ₗ[𝕜] F) (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x)))) : Set E)

Tactic:
exact h.mapsTo_tangent_cone.mono Subset.rfl Submodule.subset_span

Premises used: Set.MapsTo.mono, HasFDerivWithinAt.mapsTo_tangent_cone, Set.Subset.rfl, Submodule.subset_span
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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 → E →L[𝕜] F
hs : UniqueDiffOn 𝕜 s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hd : ∀ x ∈ s, DenseRange.{u_3, u_2} (X := F) (α := E) (⇑(f' x) : (a : E) → F)
⊢ UniqueDiffOn 𝕜 (f '' s)

Tactic:
forall_mem_image.2 fun x hx => (hf' x hx).uniqueDiffWithinAt (hs x hx) (hd x hx)

Premises used: Iff.mpr, UniqueDiffOn, HasFDerivWithinAt.uniqueDiffWithinAt, Set.forall_mem_image
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
x : E
e' : E ≃L[𝕜] F
h : HasFDerivWithinAt f (↑e' : E →L[𝕜] F) s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ UniqueDiffWithinAt 𝕜 (f '' s) (f x)

Tactic:
h.uniqueDiffWithinAt hs e'.surjective.denseRange

Premises used: Function.Surjective.denseRange, HasFDerivWithinAt.uniqueDiffWithinAt, ContinuousLinearEquiv.surjective
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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 : E ≃L[𝕜] F
h : UniqueDiffOn 𝕜 s
⊢ UniqueDiffOn.{u_1, u_3} 𝕜 (E := F) ((⇑e : (a : E) → F) '' s)

Tactic:
h.image (fun _ _ => e.hasFDerivWithinAt) fun _ _ => e.surjective.denseRange

Premises used: Function.Surjective.denseRange, UniqueDiffOn.image, ContinuousLinearEquiv.hasFDerivWithinAt, ContinuousLinearEquiv.surjective
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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 : E ≃L[𝕜] F
⊢ UniqueDiffOn.{u_1, u_3} 𝕜 (E := F) ((⇑e : (a : E) → F) '' s) ↔ UniqueDiffOn 𝕜 s

Tactic:
⟨fun h => e.symm_image_image s ▸ e.symm.uniqueDiffOn_image h, e.uniqueDiffOn_image⟩

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.uniqueDiffOn_image, Eq.rec, ContinuousLinearEquiv.symm_image_image, Iff.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
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
rw₁ rw₂ : UniqueDiffOn 𝕜 s ↔ UniqueDiffOn 𝕜 s
⊢ UniqueDiffOn.{u_1, u_3} 𝕜 (E := F) ((⇑e : (a : F) → E) ⁻¹' s) ↔ UniqueDiffOn 𝕜 s

Tactic:
rw [← e.image_symm_eq_preimage, e.symm.uniqueDiffOn_image_iff]

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.image_symm_eq_preimage, ContinuousLinearEquiv.uniqueDiffOn_image_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
h : UniqueDiffWithinAt 𝕜 s x
G : Type u_4
inst_3 : GroupWithZero G
inst_4 : DistribMulAction G E
inst_5 : ContinuousConstSMul G E
inst_6 : SMulCommClass G 𝕜 E
c : G
hc : c ≠ 0
⊢ UniqueDiffWithinAt 𝕜 (c • s) (c • x)

Tactic:
(ContinuousLinearEquiv.smulLeft <| Units.mk0 c hc).hasFDerivWithinAt
    |>.uniqueDiffWithinAt_of_continuousLinearEquiv _ h

Premises used: ContinuousLinearEquiv.hasFDerivWithinAt, Units.mk0, DFunLike.coe, ContinuousLinearEquiv.smulLeft, HasFDerivWithinAt.uniqueDiffWithinAt_of_continuousLinearEquiv