awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
⊢ f '' t ∈ 𝓝 (f x)

Tactic:
IsOpen.mem_nhds ((hf.mono_set hts).open_image f'symm ht hc) (mem_image_of_mem _ xt)

Premises used: ApproximatesLinearOn.mono_set, ApproximatesLinearOn.open_image, Set.mem_image_of_mem, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
⊢ f '' t ∈ 𝓝 (f x)

Tactic:
exact IsOpen.mem_nhds ((hf.mono_set hts).open_image f'symm ht hc) (mem_image_of_mem _ xt)

Premises used: ApproximatesLinearOn.mono_set, ApproximatesLinearOn.open_image, Set.mem_image_of_mem, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
⊢ map f (𝓝 x) = 𝓝 (f x)

Tactic:
le_antisymm ((hf.continuousOn x (mem_of_mem_nhds hs)).continuousAt hs) (le_map fun t ht => ?_)

Premises used: mem_of_mem_nhds, le_antisymm, ApproximatesLinearOn.continuousOn, Filter.le_map, ContinuousWithinAt.continuousAt
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
le_antisymm : ∀ (t : Set E) (ht : t ∈ 𝓝 x), f '' t ∈ 𝓝 (f x)
⊢ map f (𝓝 x) = 𝓝 (f x)

Tactic:
refine
    le_antisymm ((hf.continuousOn x (mem_of_mem_nhds hs)).continuousAt hs) (le_map fun t ht => ?_)

Premises used: mem_of_mem_nhds, le_antisymm, ApproximatesLinearOn.continuousOn, Filter.le_map, ContinuousWithinAt.continuousAt
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
ht : t ∈ 𝓝 x
⊢ f '' (s ∩ t) ∈ 𝓝 (f x)

Tactic:
have : f '' (s ∩ t) ∈ 𝓝 (f x) :=
    (hf.mono_set inter_subset_left).image_mem_nhds f'symm (inter_mem hs ht) hc
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
ht : t ∈ 𝓝 x
this : f '' (s ∩ t) ∈ 𝓝 (f x)
⊢ f '' t ∈ 𝓝 (f x)

Tactic:
mem_of_superset this (image_mono inter_subset_right)

Premises used: Set.image_mono, Set.inter_subset_right, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
ht : t ∈ 𝓝 x
this : f '' (s ∩ t) ∈ 𝓝 (f x)
⊢ f '' t ∈ 𝓝 (f x)

Tactic:
exact mem_of_superset this (image_mono inter_subset_right)

Premises used: Set.image_mono, Set.inter_subset_right, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
inl :
  ∀ (hE : Subsingleton E), AntilipschitzWith (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ (s.restrict (π := fun (a : E) ↦ F) f)
inr :
  ∀ (hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹),
    AntilipschitzWith (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ (s.restrict (π := fun (a : E) ↦ F) f)
⊢ AntilipschitzWith (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ (s.restrict (π := fun (a : E) ↦ F) f)

Tactic:
rcases hc with hE | hc
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hE : Subsingleton E
⊢ AntilipschitzWith (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ (s.restrict (π := fun (a : E) ↦ F) f)

Tactic:
AntilipschitzWith.of_subsingleton

Premises used: AntilipschitzWith.of_subsingleton
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hE : Subsingleton E
⊢ AntilipschitzWith (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ (s.restrict (π := fun (a : E) ↦ F) f)

Tactic:
exact AntilipschitzWith.of_subsingleton

Premises used: AntilipschitzWith.of_subsingleton
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ AntilipschitzWith.{u_2, u_3} (β := F) (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ fun (x : (↑s : Type u_2)) ↦
    HAdd.hAdd (α := F) (s.restrict (π := fun (a : E) ↦ F) (⇑f' : (a : E) → F) x : F)
      (HSub.hSub (β := F) (f (↑x : E)) (((↑f' : E →L[𝕜] F) : (a : E) → F) (↑x : E) : F))

Tactic:
(f'.antilipschitz.restrict s).add_lipschitzWith hf.lipschitz_sub hc

Premises used: ContinuousLinearEquiv.antilipschitz, ApproximatesLinearOn.lipschitz_sub, AntilipschitzWith.restrict, AntilipschitzWith.add_lipschitzWith
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
h :
  ∀ (x : (↑s : Type u_2)),
    s.restrict (π := fun (a : E) ↦ F) f x =
      HAdd.hAdd (α := F) (s.restrict (π := fun (a : E) ↦ F) (⇑f' : (a : E) → F) x : F)
        (HSub.hSub (β := F) (f (↑x : E)) (((↑f' : E →L[𝕜] F) : (a : E) → F) (↑x : E) : F))
⊢ AntilipschitzWith (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ (s.restrict (π := fun (a : E) ↦ F) f)

Tactic:
convert! (f'.antilipschitz.restrict s).add_lipschitzWith hf.lipschitz_sub hc

Premises used: ContinuousLinearEquiv.antilipschitz, ApproximatesLinearOn.lipschitz_sub, AntilipschitzWith.restrict, AntilipschitzWith.add_lipschitzWith
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
x : (↑s : Type u_2)
⊢ s.restrict (π := fun (a : E) ↦ F) f x =
    HAdd.hAdd (α := F) (s.restrict (π := fun (a : E) ↦ F) (⇑f' : (a : E) → F) x : F)
      (HSub.hSub (β := F) (f (↑x : E)) (((↑f' : E →L[𝕜] F) : (a : E) → F) (↑x : E) : F))

Tactic:
simp [restrict]

Premises used: Set.restrict
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ Injective (s.restrict (π := fun (a : E) ↦ F) f)

Tactic:
(hf.antilipschitz hc).injective

Premises used: AntilipschitzWith.injective, ApproximatesLinearOn.antilipschitz
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ InjOn f s

Tactic:
injOn_iff_injective.2 <| hf.injective hc

Premises used: Iff.mpr, Set.injOn_iff_injective, ApproximatesLinearOn.injective
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
inl : ∀ (hE : Subsingleton E), Surjective f
inr : ∀ (hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹), Surjective f
⊢ Surjective f

Tactic:
rcases hc with hE | hc
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hE : Subsingleton E
⊢ Subsingleton F

Tactic:
haveI : Subsingleton F := (Equiv.subsingleton_congr f'.toEquiv).1 hE
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hE : Subsingleton E
this : Subsingleton F
⊢ Surjective f

Tactic:
surjective_to_subsingleton _

Premises used: Function.surjective_to_subsingleton
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hE : Subsingleton E
this : Subsingleton F
⊢ Surjective f

Tactic:
exact surjective_to_subsingleton _

Premises used: Function.surjective_to_subsingleton
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
apply : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun (y : F) ↦ ∃ (a : E), f a = y) y
⊢ Surjective f

Tactic:
apply forall_of_forall_mem_closedBall (fun y : F => ∃ a, f a = y) (f 0) _

Premises used: Exists, OfNat.ofNat, Metric.forall_of_forall_mem_closedBall, Eq
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
rw : (↑c : ℝ) < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ)
⊢ 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)

Tactic:
rw [sub_pos]

Premises used: sub_pos
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ (↑c : ℝ) < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ)

Tactic:
hc

Premises used: NNReal.toReal
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ (↑c : ℝ) < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ)

Tactic:
exact hc
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)

Tactic:
have hc' : (0 : ℝ) < N⁻¹ - c := by rw [sub_pos]; exact hc
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
⊢ ∀ᶠ (r : ℝ) in atTop, 0 ≤ r

Tactic:
have hr : ∀ᶠ r : ℝ in atTop, 0 ≤ r := eventually_ge_atTop 0
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
hr : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
⊢ ∀ᶠ (r : ℝ) in atTop, p (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r)

Tactic:
hr.mono fun r hr => Subset.trans ?_ (image_subset_range f (closedBall 0 r))

Premises used: Set.Subset.trans, Set.image_subset_range, Filter.Eventually.mono, Metric.closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
hr : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
refine :
  ∀ (r : ℝ) (hr : 0 ≤ r), closedBall (f 0) (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r) ⊆ f '' closedBall 0 r
⊢ ∀ᶠ (r : ℝ) in atTop, p (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r)

Tactic:
refine hr.mono fun r hr => Subset.trans ?_ (image_subset_range f (closedBall 0 r))

Premises used: Set.Subset.trans, Set.image_subset_range, Filter.Eventually.mono, Metric.closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
hr_1 : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ closedBall (f 0) (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r) ⊆ f '' closedBall 0 r

Tactic:
hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse hr ?_

Premises used: ContinuousLinearEquiv.toNonlinearRightInverse, ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse, Set.SurjOn, NNReal.toReal
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
hr_1 : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
refine : Subset.{u_2} (α := Set E) (closedBall 0 r) univ
⊢ closedBall (f 0) (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r) ⊆ f '' closedBall 0 r

Tactic:
refine hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse hr ?_

Premises used: ContinuousLinearEquiv.toNonlinearRightInverse, ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
hr_1 : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ Subset.{u_2} (α := Set E) (closedBall 0 r) univ

Tactic:
subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
hr_1 : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ Subset.{u_2} (α := Set E) (closedBall 0 r) univ

Tactic:
exact subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
⊢ ∀ᶠ (r : ℝ) in atTop, p (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r)

Tactic:
have hp : ∀ᶠ r : ℝ in atTop, p ((N⁻¹ - c) * r) := by
      have hr : ∀ᶠ r : ℝ in atTop, 0 ≤ r := eventually_ge_atTop 0
      refine hr.mono fun r hr => Subset.trans ?_ (image_subset_range f (closedBall 0 r))
      refine hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse hr ?_
      exact subset_univ _
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
hp : ∀ᶠ (r : ℝ) in atTop, p (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r)
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun (y : F) ↦ ∃ (a : E), f a = y) y

Tactic:
((tendsto_id.const_mul_atTop hc').frequently hp.frequently).mono ?_

Premises used: Filter.Tendsto.const_mul_atTop, Filter.tendsto_id, Filter.Tendsto.frequently, Filter.Frequently.mono, Filter.Eventually.frequently
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
hp : ∀ᶠ (r : ℝ) in atTop, p (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r)
refine : ∀ (x : ℝ), p x → ∀ y ∈ closedBall (f 0) x, (fun (y : F) ↦ ∃ (a : E), f a = y) y
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun (y : F) ↦ ∃ (a : E), f a = y) y

Tactic:
refine ((tendsto_id.const_mul_atTop hc').frequently hp.frequently).mono ?_

Premises used: Filter.Tendsto.const_mul_atTop, Filter.tendsto_id, Filter.Tendsto.frequently, Filter.Frequently.mono, Filter.Eventually.frequently