-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
theorem surjective [CompleteSpace E] (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) univ c)
    (hc : Subsingleton E ∨ c < N⁻¹) : Surjective f

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
hc' : 0 < ↑‖↑f'.symm‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hr✝ : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ closedBall (f 0) ((↑‖↑f'.symm‖₊⁻¹ - ↑c) * r) ⊆ f '' closedBall 0 r

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

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
hc' : 0 < ↑‖↑f'.symm‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hr✝ : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ closedBall 0 r ⊆ univ

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
hc' : 0 < ↑‖↑f'.symm‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hr : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
⊢ ∀ᶠ (r : ℝ) in atTop, p ((↑‖↑f'.symm‖₊⁻¹ - ↑c) * r)

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

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
hc' : 0 < ↑‖↑f'.symm‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hr✝ : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ closedBall (f 0) ((↑‖↑f'.symm‖₊⁻¹ - ↑c) * r) ⊆ f '' closedBall 0 r

Proof state:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
⊢ Surjective f

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

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun y => ∃ a, f a = y) y

Proof state:
case inl
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hE : Subsingleton E
⊢ Surjective f

Tactic:
haveI : Subsingleton F := (Equiv.subsingleton_congr f'.toEquiv).1 hE

Result:
case inl
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hE : Subsingleton E
this : Subsingleton F
⊢ Surjective f

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun y => ∃ a, f a = y) y

Tactic:
have hc' : (0 : ℝ) < N⁻¹ - c := by rw [sub_pos]; exact hc

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
hc' : 0 < ↑‖↑f'.symm‖₊⁻¹ - ↑c
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun y => ∃ a, f a = y) y

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
hc' : 0 < ↑‖↑f'.symm‖₊⁻¹ - ↑c
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun y => ∃ a, f a = y) y

Tactic:
let p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ Set.range f

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
hc' : 0 < ↑‖↑f'.symm‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun y => ∃ a, f a = y) y