[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
[PROOFSTEP]
have A : ⋃ n : ℕ, closure (f '' ball 0 n) = Set.univ :=
  by
  refine' Subset.antisymm (subset_univ _) fun y _ => _
  rcases surj y with ⟨x, hx⟩
  rcases exists_nat_gt ‖x‖ with ⟨n, hn⟩
  refine' mem_iUnion.2 ⟨n, subset_closure _⟩
  refine' (mem_image _ _ _).2 ⟨x, ⟨_, hx⟩⟩
  rwa [mem_ball, dist_eq_norm, sub_zero]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
⊢ ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
[PROOFSTEP]
refine' Subset.antisymm (subset_univ _) fun y _ => _
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
⊢ y ∈ ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)
[PROOFSTEP]
rcases surj y with ⟨x, hx⟩
[GOAL]
case intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
⊢ y ∈ ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)
[PROOFSTEP]
rcases exists_nat_gt ‖x‖ with ⟨n, hn⟩
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
n : ℕ
hn : ‖x‖ < ↑n
⊢ y ∈ ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)
[PROOFSTEP]
refine' mem_iUnion.2 ⟨n, subset_closure _⟩
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
n : ℕ
hn : ‖x‖ < ↑n
⊢ y ∈ ↑f '' ball 0 ↑n
[PROOFSTEP]
refine' (mem_image _ _ _).2 ⟨x, ⟨_, hx⟩⟩
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
n : ℕ
hn : ‖x‖ < ↑n
⊢ x ∈ ball 0 ↑n
[PROOFSTEP]
rwa [mem_ball, dist_eq_norm, sub_zero]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
[PROOFSTEP]
have : ∃ (n : ℕ) (x : _), x ∈ interior (closure (f '' ball 0 n)) :=
  nonempty_interior_of_iUnion_of_closed (fun n => isClosed_closure) A
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
this : ∃ n x, x ∈ interior (closure (↑f '' ball 0 ↑n))
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
[PROOFSTEP]
simp only [mem_interior_iff_mem_nhds, Metric.mem_nhds_iff] at this 
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
this : ∃ n x ε, ε > 0 ∧ ball x ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
[PROOFSTEP]
rcases this with ⟨n, a, ε, ⟨εpos, H⟩⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
[PROOFSTEP]
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
[PROOFSTEP]
refine' ⟨(ε / 2)⁻¹ * ‖c‖ * 2 * n, _, fun y => _⟩
[GOAL]
case intro.intro.intro.intro.intro.refine'_1
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n ≥ 0
[PROOFSTEP]
refine' mul_nonneg (mul_nonneg (mul_nonneg _ (norm_nonneg _)) (by norm_num)) _
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro.intro.intro.intro.refine'_1.refine'_1
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 ≤ (ε / 2)⁻¹
case intro.intro.intro.intro.intro.refine'_1.refine'_2
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 ≤ ↑n
[PROOFSTEP]
exacts [inv_nonneg.2 (div_nonneg (le_of_lt εpos) (by norm_num)), n.cast_nonneg]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro.intro.intro.intro.refine'_2
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y = 0
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
use 0
[GOAL]
case h
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y = 0
⊢ dist (↑f 0) y ≤ 1 / 2 * ‖y‖ ∧ ‖0‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
simp [hy]
[GOAL]
case neg
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
rcases rescale_to_shell hc (half_pos εpos) hy with ⟨d, hd, ydlt, -, dinv⟩
[GOAL]
case neg.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
let δ := ‖d‖ * ‖y‖ / 4
[GOAL]
case neg.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
have δpos : 0 < δ := div_pos (mul_pos (norm_pos_iff.2 hd) (norm_pos_iff.2 hy)) (by norm_num)
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
⊢ 0 < 4
[PROOFSTEP]
norm_num
[GOAL]
case neg.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
have : a + d • y ∈ ball a ε := by simp [dist_eq_norm, lt_of_le_of_lt ydlt.le (half_lt_self εpos)]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
⊢ a + d • y ∈ ball a ε
[PROOFSTEP]
simp [dist_eq_norm, lt_of_le_of_lt ydlt.le (half_lt_self εpos)]
[GOAL]
case neg.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
rcases Metric.mem_closure_iff.1 (H this) _ δpos with ⟨z₁, z₁im, h₁⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₁ : dist (a + d • y) z₁ < δ
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
rcases(mem_image _ _ _).1 z₁im with ⟨x₁, hx₁, xz₁⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₁ : dist (a + d • y) z₁ < δ
x₁ : E
hx₁ : x₁ ∈ ball 0 ↑n
xz₁ : ↑f x₁ = z₁
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
rw [← xz₁] at h₁ 
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : x₁ ∈ ball 0 ↑n
xz₁ : ↑f x₁ = z₁
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
rw [mem_ball, dist_eq_norm, sub_zero] at hx₁ 
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
have : a ∈ ball a ε := by
  simp
  exact εpos
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
⊢ a ∈ ball a ε
[PROOFSTEP]
simp
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
⊢ 0 < ε
[PROOFSTEP]
exact εpos
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
rcases Metric.mem_closure_iff.1 (H this) _ δpos with ⟨z₂, z₂im, h₂⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₂ : dist a z₂ < δ
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
rcases(mem_image _ _ _).1 z₂im with ⟨x₂, hx₂, xz₂⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₂ : dist a z₂ < δ
x₂ : E
hx₂ : x₂ ∈ ball 0 ↑n
xz₂ : ↑f x₂ = z₂
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
rw [← xz₂] at h₂ 
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : x₂ ∈ ball 0 ↑n
xz₂ : ↑f x₂ = z₂
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
rw [mem_ball, dist_eq_norm, sub_zero] at hx₂ 
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
let x := x₁ - x₂
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
have I : ‖f x - d • y‖ ≤ 2 * δ :=
  calc
    ‖f x - d • y‖ = ‖f x₁ - (a + d • y) - (f x₂ - a)‖ := by
      congr 1
      simp only [f.map_sub]
      abel
    _ ≤ ‖f x₁ - (a + d • y)‖ + ‖f x₂ - a‖ := (norm_sub_le _ _)
    _ ≤ δ + δ := by
      apply add_le_add
      · rw [← dist_eq_norm, dist_comm]
        exact le_of_lt h₁
      · rw [← dist_eq_norm, dist_comm]
        exact le_of_lt h₂
    _ = 2 * δ := (two_mul _).symm
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖↑f x - d • y‖ = ‖↑f x₁ - (a + d • y) - (↑f x₂ - a)‖
[PROOFSTEP]
congr 1
[GOAL]
case e_a
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ↑f x - d • y = ↑f x₁ - (a + d • y) - (↑f x₂ - a)
[PROOFSTEP]
simp only [f.map_sub]
[GOAL]
case e_a
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ↑f x₁ - ↑f x₂ - d • y = ↑f x₁ - (a + d • y) - (↑f x₂ - a)
[PROOFSTEP]
abel
[GOAL]
case e_a
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ↑f x₁ - ↑f x₂ - d • y = ↑f x₁ - (a + d • y) - (↑f x₂ - a)
[PROOFSTEP]
abel
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖↑f x₁ - (a + d • y)‖ + ‖↑f x₂ - a‖ ≤ δ + δ
[PROOFSTEP]
apply add_le_add
[GOAL]
case h₁
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖↑f x₁ - (a + d • y)‖ ≤ δ
[PROOFSTEP]
rw [← dist_eq_norm, dist_comm]
[GOAL]
case h₁
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ dist (a + d • y) (↑f x₁) ≤ δ
[PROOFSTEP]
exact le_of_lt h₁
[GOAL]
case h₂
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖↑f x₂ - a‖ ≤ δ
[PROOFSTEP]
rw [← dist_eq_norm, dist_comm]
[GOAL]
case h₂
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ dist a (↑f x₂) ≤ δ
[PROOFSTEP]
exact le_of_lt h₂
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
have J : ‖f (d⁻¹ • x) - y‖ ≤ 1 / 2 * ‖y‖ :=
  calc
    ‖f (d⁻¹ • x) - y‖ = ‖d⁻¹ • f x - (d⁻¹ * d) • y‖ := by rwa [f.map_smul _, inv_mul_cancel, one_smul]
    _ = ‖d⁻¹ • (f x - d • y)‖ := by rw [mul_smul, smul_sub]
    _ = ‖d‖⁻¹ * ‖f x - d • y‖ := by rw [norm_smul, norm_inv]
    _ ≤ ‖d‖⁻¹ * (2 * δ) := by
      apply mul_le_mul_of_nonneg_left I
      rw [inv_nonneg]
      exact norm_nonneg _
    _ = ‖d‖⁻¹ * ‖d‖ * ‖y‖ / 2 := by
      simp only
      ring
    _ = ‖y‖ / 2 := by
      rw [inv_mul_cancel, one_mul]
      simp [norm_eq_zero, hd]
    _ = 1 / 2 * ‖y‖ := by ring
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖↑f (d⁻¹ • x) - y‖ = ‖d⁻¹ • ↑f x - (d⁻¹ * d) • y‖
[PROOFSTEP]
rwa [f.map_smul _, inv_mul_cancel, one_smul]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d⁻¹ • ↑f x - (d⁻¹ * d) • y‖ = ‖d⁻¹ • (↑f x - d • y)‖
[PROOFSTEP]
rw [mul_smul, smul_sub]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d⁻¹ • (↑f x - d • y)‖ = ‖d‖⁻¹ * ‖↑f x - d • y‖
[PROOFSTEP]
rw [norm_smul, norm_inv]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖⁻¹ * ‖↑f x - d • y‖ ≤ ‖d‖⁻¹ * (2 * δ)
[PROOFSTEP]
apply mul_le_mul_of_nonneg_left I
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ 0 ≤ ‖d‖⁻¹
[PROOFSTEP]
rw [inv_nonneg]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ 0 ≤ ‖d‖
[PROOFSTEP]
exact norm_nonneg _
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖⁻¹ * (2 * δ) = ‖d‖⁻¹ * ‖d‖ * ‖y‖ / 2
[PROOFSTEP]
simp only
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖⁻¹ * (2 * (‖d‖ * ‖y‖ / 4)) = ‖d‖⁻¹ * ‖d‖ * ‖y‖ / 2
[PROOFSTEP]
ring
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖⁻¹ * ‖d‖ * ‖y‖ / 2 = ‖y‖ / 2
[PROOFSTEP]
rw [inv_mul_cancel, one_mul]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖ ≠ 0
[PROOFSTEP]
simp [norm_eq_zero, hd]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖y‖ / 2 = 1 / 2 * ‖y‖
[PROOFSTEP]
ring
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : ‖↑f (d⁻¹ • x) - y‖ ≤ 1 / 2 * ‖y‖
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
rw [← dist_eq_norm] at J 
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
have K : ‖d⁻¹ • x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖ :=
  calc
    ‖d⁻¹ • x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖ := by rw [norm_smul, norm_inv]
    _ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖ * (n + n) :=
      by
      refine' mul_le_mul dinv _ (norm_nonneg _) _
      · exact le_trans (norm_sub_le _ _) (add_le_add (le_of_lt hx₁) (le_of_lt hx₂))
      · apply mul_nonneg (mul_nonneg _ (norm_nonneg _)) (norm_nonneg _)
        exact inv_nonneg.2 (le_of_lt (half_pos εpos))
    _ = (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖ := by ring
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖d⁻¹ • x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖
[PROOFSTEP]
rw [norm_smul, norm_inv]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖d‖⁻¹ * ‖x₁ - x₂‖ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖ * (↑n + ↑n)
[PROOFSTEP]
refine' mul_le_mul dinv _ (norm_nonneg _) _
[GOAL]
case refine'_1
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖x₁ - x₂‖ ≤ ↑n + ↑n
[PROOFSTEP]
exact le_trans (norm_sub_le _ _) (add_le_add (le_of_lt hx₁) (le_of_lt hx₂))
[GOAL]
case refine'_2
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ 0 ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
[PROOFSTEP]
apply mul_nonneg (mul_nonneg _ (norm_nonneg _)) (norm_nonneg _)
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ 0 ≤ (ε / 2)⁻¹
[PROOFSTEP]
exact inv_nonneg.2 (le_of_lt (half_pos εpos))
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ (ε / 2)⁻¹ * ‖c‖ * ‖y‖ * (↑n + ↑n) = (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
ring
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
K : ‖d⁻¹ • x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
[PROOFSTEP]
exact ⟨d⁻¹ • x, J, K⟩
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
⊢ ∃ C, C > 0 ∧ ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
[PROOFSTEP]
obtain ⟨C, C0, hC⟩ := exists_approx_preimage_norm_le f surj
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
hC : ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
⊢ ∃ C, C > 0 ∧ ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
[PROOFSTEP]
choose g hg using hC
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
⊢ ∃ C, C > 0 ∧ ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
[PROOFSTEP]
let h y := y - f (g y)
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
⊢ ∃ C, C > 0 ∧ ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
[PROOFSTEP]
have hle : ∀ y, ‖h y‖ ≤ 1 / 2 * ‖y‖ := by
  intro y
  rw [← dist_eq_norm, dist_comm]
  exact (hg y).1
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
⊢ ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
[PROOFSTEP]
intro y
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
y : F
⊢ ‖h y‖ ≤ 1 / 2 * ‖y‖
[PROOFSTEP]
rw [← dist_eq_norm, dist_comm]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
y : F
⊢ dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖
[PROOFSTEP]
exact (hg y).1
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
⊢ ∃ C, C > 0 ∧ ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
[PROOFSTEP]
refine' ⟨2 * C + 1, by linarith, fun y => _⟩
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
⊢ 2 * C + 1 > 0
[PROOFSTEP]
linarith
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
have hnle : ∀ n : ℕ, ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖ := by
  intro n
  induction' n with n IH
  · simp only [one_div, Nat.zero_eq, one_mul, iterate_zero_apply, pow_zero, le_rfl]
  · rw [iterate_succ']
    apply le_trans (hle _) _
    rw [pow_succ, mul_assoc]
    apply mul_le_mul_of_nonneg_left IH
    norm_num
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
⊢ ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
[PROOFSTEP]
intro n
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
n : ℕ
⊢ ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
⊢ ‖h^[Nat.zero] y‖ ≤ (1 / 2) ^ Nat.zero * ‖y‖
[PROOFSTEP]
simp only [one_div, Nat.zero_eq, one_mul, iterate_zero_apply, pow_zero, le_rfl]
[GOAL]
case succ
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
n : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ ‖h^[Nat.succ n] y‖ ≤ (1 / 2) ^ Nat.succ n * ‖y‖
[PROOFSTEP]
rw [iterate_succ']
[GOAL]
case succ
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
n : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ ‖(h ∘ h^[n]) y‖ ≤ (1 / 2) ^ Nat.succ n * ‖y‖
[PROOFSTEP]
apply le_trans (hle _) _
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
n : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ 1 / 2 * ‖h^[n] y‖ ≤ (1 / 2) ^ Nat.succ n * ‖y‖
[PROOFSTEP]
rw [pow_succ, mul_assoc]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
n : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ 1 / 2 * ‖h^[n] y‖ ≤ 1 / 2 * ((1 / 2) ^ n * ‖y‖)
[PROOFSTEP]
apply mul_le_mul_of_nonneg_left IH
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
n : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ 0 ≤ 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
let u n := g (h^[n] y)
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
have ule : ∀ n, ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖) := by
  intro n
  apply le_trans (hg _).2 _
  calc
    C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖) := mul_le_mul_of_nonneg_left (hnle n) C0
    _ = (1 / 2) ^ n * (C * ‖y‖) := by ring
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
⊢ ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
[PROOFSTEP]
intro n
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
n : ℕ
⊢ ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
[PROOFSTEP]
apply le_trans (hg _).2 _
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
n : ℕ
⊢ C * ‖h^[n] y‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
[PROOFSTEP]
calc
  C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖) := mul_le_mul_of_nonneg_left (hnle n) C0
  _ = (1 / 2) ^ n * (C * ‖y‖) := by ring
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
n : ℕ
⊢ C * ((1 / 2) ^ n * ‖y‖) = (1 / 2) ^ n * (C * ‖y‖)
[PROOFSTEP]
ring
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
have sNu : Summable fun n => ‖u n‖ :=
  by
  refine' summable_of_nonneg_of_le (fun n => norm_nonneg _) ule _
  exact Summable.mul_right _ (summable_geometric_of_lt_1 (by norm_num) (by norm_num))
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
⊢ Summable fun n => ‖u n‖
[PROOFSTEP]
refine' summable_of_nonneg_of_le (fun n => norm_nonneg _) ule _
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
⊢ Summable fun b => (1 / 2) ^ b * (C * ‖y‖)
[PROOFSTEP]
exact Summable.mul_right _ (summable_geometric_of_lt_1 (by norm_num) (by norm_num))
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
⊢ 0 ≤ 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
⊢ 1 / 2 < 1
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
have su : Summable u := summable_of_summable_norm sNu
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
let x := tsum u
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
have x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖ :=
  calc
    ‖x‖ ≤ ∑' n, ‖u n‖ := norm_tsum_le_tsum_norm sNu
    _ ≤ ∑' n, (1 / 2) ^ n * (C * ‖y‖) := (tsum_le_tsum ule sNu (Summable.mul_right _ summable_geometric_two))
    _ = (∑' n, (1 / 2) ^ n) * (C * ‖y‖) := tsum_mul_right
    _ = 2 * C * ‖y‖ := by rw [tsum_geometric_two, mul_assoc]
    _ ≤ 2 * C * ‖y‖ + ‖y‖ := (le_add_of_nonneg_right (norm_nonneg y))
    _ = (2 * C + 1) * ‖y‖ := by ring
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
⊢ (∑' (n : ℕ), (1 / 2) ^ n) * (C * ‖y‖) = 2 * C * ‖y‖
[PROOFSTEP]
rw [tsum_geometric_two, mul_assoc]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
⊢ 2 * C * ‖y‖ + ‖y‖ = (2 * C + 1) * ‖y‖
[PROOFSTEP]
ring
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
have fsumeq : ∀ n : ℕ, f (∑ i in Finset.range n, u i) = y - h^[n] y :=
  by
  intro n
  induction' n with n IH
  · simp [f.map_zero]
  · rw [sum_range_succ, f.map_add, IH, iterate_succ_apply', sub_add]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
⊢ ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
[PROOFSTEP]
intro n
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
n : ℕ
⊢ ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
⊢ ↑f (∑ i in Finset.range Nat.zero, u i) = y - h^[Nat.zero] y
[PROOFSTEP]
simp [f.map_zero]
[GOAL]
case succ
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
n : ℕ
IH : ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
⊢ ↑f (∑ i in Finset.range (Nat.succ n), u i) = y - h^[Nat.succ n] y
[PROOFSTEP]
rw [sum_range_succ, f.map_add, IH, iterate_succ_apply', sub_add]
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
have : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x) := su.hasSum.tendsto_sum_nat
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
have L₁ : Tendsto (fun n => f (∑ i in Finset.range n, u i)) atTop (𝓝 (f x)) := (f.continuous.tendsto _).comp this
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => ↑f (∑ i in Finset.range n, u i)) atTop (𝓝 (↑f x))
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
simp only [fsumeq] at L₁ 
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
have L₂ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (y - 0)) :=
  by
  refine' tendsto_const_nhds.sub _
  rw [tendsto_iff_norm_tendsto_zero]
  simp only [sub_zero]
  refine' squeeze_zero (fun _ => norm_nonneg _) hnle _
  rw [← zero_mul ‖y‖]
  refine' (_root_.tendsto_pow_atTop_nhds_0_of_lt_1 _ _).mul tendsto_const_nhds <;> norm_num
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
⊢ Tendsto (fun n => y - h^[n] y) atTop (𝓝 (y - 0))
[PROOFSTEP]
refine' tendsto_const_nhds.sub _
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
⊢ Tendsto (fun n => h^[n] y) atTop (𝓝 0)
[PROOFSTEP]
rw [tendsto_iff_norm_tendsto_zero]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
⊢ Tendsto (fun e => ‖h^[e] y - 0‖) atTop (𝓝 0)
[PROOFSTEP]
simp only [sub_zero]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
⊢ Tendsto (fun e => ‖(fun y => y - ↑f (g y))^[e] y‖) atTop (𝓝 0)
[PROOFSTEP]
refine' squeeze_zero (fun _ => norm_nonneg _) hnle _
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
⊢ Tendsto (fun t => (1 / 2) ^ t * ‖y‖) atTop (𝓝 0)
[PROOFSTEP]
rw [← zero_mul ‖y‖]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
⊢ Tendsto (fun t => (1 / 2) ^ t * ‖y‖) atTop (𝓝 (0 * ‖y‖))
[PROOFSTEP]
refine' (_root_.tendsto_pow_atTop_nhds_0_of_lt_1 _ _).mul tendsto_const_nhds
[GOAL]
case refine'_1
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
⊢ 0 ≤ 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
⊢ 1 / 2 < 1
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
L₂ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (y - 0))
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
have feq : f x = y - 0 := tendsto_nhds_unique L₁ L₂
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
L₂ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (y - 0))
feq : ↑f x = y - 0
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
rw [sub_zero] at feq 
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (↑f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y => y - ↑f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n => g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n => ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), ↑f (∑ i in Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n => y - (fun y => y - ↑f (g y))^[n] y) atTop (𝓝 (↑f (∑' (n : ℕ), g ((fun y => y - ↑f (g y))^[n] y))))
L₂ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (y - 0))
feq : ↑f x = y
⊢ ∃ x, ↑f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
[PROOFSTEP]
exact ⟨x, feq, x_ineq⟩
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
⊢ IsOpenMap ↑f
[PROOFSTEP]
intro s hs
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
⊢ IsOpen (↑f '' s)
[PROOFSTEP]
rcases exists_preimage_norm_le f surj with ⟨C, Cpos, hC⟩
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
⊢ IsOpen (↑f '' s)
[PROOFSTEP]
refine' isOpen_iff.2 fun y yfs => _
[GOAL]
case intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
⊢ ∃ ε, ε > 0 ∧ ball y ε ⊆ ↑f '' s
[PROOFSTEP]
rcases mem_image_iff_bex.1 yfs with ⟨x, xs, fxy⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
⊢ ∃ ε, ε > 0 ∧ ball y ε ⊆ ↑f '' s
[PROOFSTEP]
rcases isOpen_iff.1 hs x xs with ⟨ε, εpos, hε⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
⊢ ∃ ε, ε > 0 ∧ ball y ε ⊆ ↑f '' s
[PROOFSTEP]
refine' ⟨ε / C, div_pos εpos Cpos, fun z hz => _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
⊢ z ∈ ↑f '' s
[PROOFSTEP]
rcases hC (z - y) with ⟨w, wim, wnorm⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
⊢ z ∈ ↑f '' s
[PROOFSTEP]
have : f (x + w) = z := by rw [f.map_add, wim, fxy, add_sub_cancel'_right]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
⊢ ↑f (x + w) = z
[PROOFSTEP]
rw [f.map_add, wim, fxy, add_sub_cancel'_right]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ z ∈ ↑f '' s
[PROOFSTEP]
rw [← this]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ ↑f (x + w) ∈ ↑f '' s
[PROOFSTEP]
have : x + w ∈ ball x ε :=
  calc
    dist (x + w) x = ‖w‖ := by
      rw [dist_eq_norm]
      simp
    _ ≤ C * ‖z - y‖ := wnorm
    _ < C * (ε / C) := by
      apply mul_lt_mul_of_pos_left _ Cpos
      rwa [mem_ball, dist_eq_norm] at hz 
    _ = ε := mul_div_cancel' _ (ne_of_gt Cpos)
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ dist (x + w) x = ‖w‖
[PROOFSTEP]
rw [dist_eq_norm]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ ‖x + w - x‖ = ‖w‖
[PROOFSTEP]
simp
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ C * ‖z - y‖ < C * (ε / C)
[PROOFSTEP]
apply mul_lt_mul_of_pos_left _ Cpos
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ ‖z - y‖ < ε / C
[PROOFSTEP]
rwa [mem_ball, dist_eq_norm] at hz 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this✝ : ↑f (x + w) = z
this : x + w ∈ ball x ε
⊢ ↑f (x + w) ∈ ↑f '' s
[PROOFSTEP]
exact Set.mem_image_of_mem _ (hε this)
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
hsurj : LinearMap.range f = ⊤
⊢ ∃ fsymm, 0 < fsymm.nnnorm
[PROOFSTEP]
choose C hC fsymm h using exists_preimage_norm_le _ (LinearMap.range_eq_top.mp hsurj)
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
hsurj : LinearMap.range f = ⊤
C : ℝ
hC : C > 0
fsymm : F → E
h : ∀ (y : F), ↑f (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖
⊢ ∃ fsymm, 0 < fsymm.nnnorm
[PROOFSTEP]
use{
    toFun := fsymm
    nnnorm := ⟨C, hC.lt.le⟩
    bound' := fun y => (h y).2
    right_inv' := fun y => (h y).1 }
[GOAL]
case h
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
hsurj : LinearMap.range f = ⊤
C : ℝ
hC : C > 0
fsymm : F → E
h : ∀ (y : F), ↑f (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖
⊢ 0 <
    { toFun := fsymm, nnnorm := { val := C, property := (_ : 0 ≤ C) }, bound' := (_ : ∀ (y : F), ‖fsymm y‖ ≤ C * ‖y‖),
        right_inv' := (_ : ∀ (y : F), ↑f (fsymm y) = y) }.nnnorm
[PROOFSTEP]
exact hC
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
hsurj : LinearMap.range f = ⊤
⊢ 0 < (nonlinearRightInverseOfSurjective f hsurj).nnnorm
[PROOFSTEP]
rw [nonlinearRightInverseOfSurjective]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
hsurj : LinearMap.range f = ⊤
⊢ 0 < (Classical.choose (_ : ∃ fsymm, 0 < fsymm.nnnorm)).nnnorm
[PROOFSTEP]
exact Classical.choose_spec (exists_nonlinearRightInverse_of_surjective f hsurj)
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑e
⊢ Continuous ↑(symm e)
[PROOFSTEP]
rw [continuous_def]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑e
⊢ ∀ (s : Set E), IsOpen s → IsOpen (↑(symm e) ⁻¹' s)
[PROOFSTEP]
intro s hs
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑e
s : Set E
hs : IsOpen s
⊢ IsOpen (↑(symm e) ⁻¹' s)
[PROOFSTEP]
rw [← e.image_eq_preimage]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑e
s : Set E
hs : IsOpen s
⊢ IsOpen (↑e '' s)
[PROOFSTEP]
rw [← e.coe_coe] at h ⊢
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑↑e
s : Set E
hs : IsOpen s
⊢ IsOpen (↑↑e '' s)
[PROOFSTEP]
exact ContinuousLinearMap.isOpenMap (𝕜 := 𝕜) ⟨↑e, h⟩ e.surjective s hs
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
hinj : ker f = ⊥
hsurj : LinearMap.range f = ⊤
⊢ Continuous ↑(LinearEquiv.ofBijective ↑f (_ : Injective ↑↑f ∧ Surjective ↑↑f))
[PROOFSTEP]
convert f.continuous
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
hinj : ker f = ⊥
hsurj : LinearMap.range f = ⊤
⊢ ↑(ofBijective f hinj hsurj) = f
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
hinj : ker f = ⊥
hsurj : LinearMap.range f = ⊤
x✝ : E
⊢ ↑↑(ofBijective f hinj hsurj) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
inst✝ : CompleteSpace { x // x ∈ G }
hker : ker f = ⊥
⊢ ker (coprod f (Submodule.subtypeL G)) = ⊥
[PROOFSTEP]
rw [ker_coprod_of_disjoint_range]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
inst✝ : CompleteSpace { x // x ∈ G }
hker : ker f = ⊥
⊢ Submodule.prod (ker f) (ker (Submodule.subtypeL G)) = ⊥
[PROOFSTEP]
rw [hker, Submodule.ker_subtypeL, Submodule.prod_bot]
[GOAL]
case hd
𝕜 : 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 →L[𝕜] F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
inst✝ : CompleteSpace { x // x ∈ G }
hker : ker f = ⊥
⊢ Disjoint (LinearMap.range f) (LinearMap.range (Submodule.subtypeL G))
[PROOFSTEP]
rw [Submodule.range_subtypeL]
[GOAL]
case hd
𝕜 : 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 →L[𝕜] F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
inst✝ : CompleteSpace { x // x ∈ G }
hker : ker f = ⊥
⊢ Disjoint (LinearMap.range f) G
[PROOFSTEP]
exact h.disjoint
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
inst✝ : CompleteSpace { x // x ∈ G }
hker : ker f = ⊥
⊢ LinearMap.range (coprod f (Submodule.subtypeL G)) = ⊤
[PROOFSTEP]
rw [range_coprod, Submodule.range_subtypeL, h.sup_eq_top]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
inst✝ : CompleteSpace { x // x ∈ G }
hker : ker f = ⊥
⊢ LinearMap.range f = Submodule.map (↑↑(coprodSubtypeLEquivOfIsCompl f h hker)) (Submodule.prod ⊤ ⊥)
[PROOFSTEP]
rw [coprodSubtypeLEquivOfIsCompl, ContinuousLinearEquiv.coe_ofBijective, coe_coprod, LinearMap.coprod_map_prod,
  Submodule.map_bot, sup_bot_eq, Submodule.map_top]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
inst✝ : CompleteSpace { x // x ∈ G }
hker : ker f = ⊥
⊢ LinearMap.range f = LinearMap.range ↑f
[PROOFSTEP]
rfl
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
⊢ IsClosed ↑(LinearMap.range f)
[PROOFSTEP]
haveI : CompleteSpace G := hG.completeSpace_coe
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
⊢ IsClosed ↑(LinearMap.range f)
[PROOFSTEP]
let g := coprodSubtypeLEquivOfIsCompl f h hker
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
g : (E × { x // x ∈ G }) ≃L[𝕜] F := coprodSubtypeLEquivOfIsCompl f h hker
⊢ IsClosed ↑(LinearMap.range f)
[PROOFSTEP]
rw [range_eq_map_coprodSubtypeLEquivOfIsCompl f h hker]
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
g : (E × { x // x ∈ G }) ≃L[𝕜] F := coprodSubtypeLEquivOfIsCompl f h hker
⊢ IsClosed ↑(Submodule.map (↑↑(coprodSubtypeLEquivOfIsCompl f h hker)) (Submodule.prod ⊤ ⊥))
[PROOFSTEP]
apply g.toHomeomorph.isClosed_image.2
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
g : (E × { x // x ∈ G }) ≃L[𝕜] F := coprodSubtypeLEquivOfIsCompl f h hker
⊢ IsClosed ↑(Submodule.prod ⊤ ⊥)
[PROOFSTEP]
exact isClosed_univ.prod isClosed_singleton
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : IsClosed ↑(graph g)
⊢ Continuous ↑g
[PROOFSTEP]
letI : CompleteSpace g.graph := completeSpace_coe_iff_isComplete.mpr hg.isComplete
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : IsClosed ↑(graph g)
this : CompleteSpace { x // x ∈ graph g } := Iff.mpr completeSpace_coe_iff_isComplete (IsClosed.isComplete hg)
⊢ Continuous ↑g
[PROOFSTEP]
let φ₀ : E →ₗ[𝕜] E × F := LinearMap.id.prod g
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : IsClosed ↑(graph g)
this : CompleteSpace { x // x ∈ graph g } := Iff.mpr completeSpace_coe_iff_isComplete (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := prod id g
⊢ Continuous ↑g
[PROOFSTEP]
have : Function.LeftInverse Prod.fst φ₀ := fun x => rfl
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : IsClosed ↑(graph g)
this✝ : CompleteSpace { x // x ∈ graph g } := Iff.mpr completeSpace_coe_iff_isComplete (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := prod id g
this : LeftInverse Prod.fst ↑φ₀
⊢ Continuous ↑g
[PROOFSTEP]
let φ : E ≃ₗ[𝕜] g.graph := (LinearEquiv.ofLeftInverse this).trans (LinearEquiv.ofEq _ _ g.graph_eq_range_prod.symm)
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : IsClosed ↑(graph g)
this✝ : CompleteSpace { x // x ∈ graph g } := Iff.mpr completeSpace_coe_iff_isComplete (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := prod id g
this : LeftInverse Prod.fst ↑φ₀
φ : E ≃ₗ[𝕜] { x // x ∈ graph g } :=
  LinearEquiv.trans (LinearEquiv.ofLeftInverse this)
    (LinearEquiv.ofEq (range φ₀) (graph g) (_ : range (prod id g) = graph g))
⊢ Continuous ↑g
[PROOFSTEP]
let ψ : g.graph ≃L[𝕜] E := φ.symm.toContinuousLinearEquivOfContinuous continuous_subtype_val.fst
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : IsClosed ↑(graph g)
this✝ : CompleteSpace { x // x ∈ graph g } := Iff.mpr completeSpace_coe_iff_isComplete (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := prod id g
this : LeftInverse Prod.fst ↑φ₀
φ : E ≃ₗ[𝕜] { x // x ∈ graph g } :=
  LinearEquiv.trans (LinearEquiv.ofLeftInverse this)
    (LinearEquiv.ofEq (range φ₀) (graph g) (_ : range (prod id g) = graph g))
ψ : { x // x ∈ graph g } ≃L[𝕜] E :=
  LinearEquiv.toContinuousLinearEquivOfContinuous (LinearEquiv.symm φ) (_ : Continuous fun a => (↑a).fst)
⊢ Continuous ↑g
[PROOFSTEP]
exact (continuous_subtype_val.comp ψ.symm.continuous).snd
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
⊢ Continuous ↑g
[PROOFSTEP]
refine' g.continuous_of_isClosed_graph (IsSeqClosed.isClosed _)
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
⊢ IsSeqClosed ↑(graph g)
[PROOFSTEP]
rintro φ ⟨x, y⟩ hφg hφ
[GOAL]
case mk
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
⊢ (x, y) ∈ ↑(graph g)
[PROOFSTEP]
refine' hg (Prod.fst ∘ φ) x y ((continuous_fst.tendsto _).comp hφ) _
[GOAL]
case mk
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
⊢ Tendsto (↑g ∘ Prod.fst ∘ φ) atTop (𝓝 y)
[PROOFSTEP]
have : g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ := by
  ext n
  exact (hφg n).symm
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
⊢ ↑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
[PROOFSTEP]
ext n
[GOAL]
case h
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
n : ℕ
⊢ (↑g ∘ Prod.fst ∘ φ) n = (Prod.snd ∘ φ) n
[PROOFSTEP]
exact (hφg n).symm
[GOAL]
case mk
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
this : ↑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
⊢ Tendsto (↑g ∘ Prod.fst ∘ φ) atTop (𝓝 y)
[PROOFSTEP]
rw [this]
[GOAL]
case mk
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
this : ↑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
⊢ Tendsto (Prod.snd ∘ φ) atTop (𝓝 y)
[PROOFSTEP]
exact (continuous_snd.tendsto _).comp hφ
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : IsClosed ↑(LinearMap.graph g)
⊢ ↑(ofIsClosedGraph hg) = g
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : IsClosed ↑(LinearMap.graph g)
x✝ : E
⊢ ↑↑(ofIsClosedGraph hg) x✝ = ↑g x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
⊢ ↑(ofSeqClosedGraph hg) = g
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : 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 →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
x✝ : E
⊢ ↑↑(ofSeqClosedGraph hg) x✝ = ↑g x✝
[PROOFSTEP]
rfl
