case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
obtain ⟨C, C0, hC⟩ := exists_approx_preimage_norm_le f surj
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
choose g hg using hC
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
let h y := y - f (g y)
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
have hle : ∀ y, ‖h y‖ ≤ 1 / 2 * ‖y‖ := by
  intro y
  rw [← dist_eq_norm, dist_comm]
  exact (hg y).1
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
refine' ⟨2 * C + 1, by linarith, fun y => _⟩
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
let u n := g ((h^[n]) y)
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
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
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
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))
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
have su : Summable u := summable_of_summable_norm sNu
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
let x := tsum u
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
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
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
have : Tendsto (fun n => ∑ i in Finset.range n, u i) atTop (𝓝 x) := su.hasSum.tendsto_sum_nat
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
have L₁ : Tendsto (fun n => f (∑ i in Finset.range n, u i)) atTop (𝓝 (f x)) :=
  (f.continuous.tendsto _).comp this
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
simp only [fsumeq] at L₁
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
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 [← MulZeroClass.zero_mul ‖y‖]
  refine' (_root_.tendsto_pow_atTop_nhds_0_of_lt_1 _ _).mul tendsto_const_nhds <;> norm_num
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
have feq : f x = y - 0 := tendsto_nhds_unique L₁ L₂
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
rw [sub_zero] at feq
no goals
case intro.intro
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
exact ⟨x, feq, x_ineq⟩
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
intro y
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
rw [← dist_eq_norm, dist_comm]
no goals
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
exact (hg y).1
no goals
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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
linarith
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
intro n
case zero
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖

case succ
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
induction' n with n IH
no goals
case zero
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
simp only [one_div, Nat.zero_eq, one_mul, iterate_zero_apply, pow_zero, le_rfl]
case succ
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case succ
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
rw [iterate_succ']
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
case succ
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
apply le_trans (hle _) _
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖)
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
rw [pow_succ, mul_assoc]
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖)
apply mul_le_mul_of_nonneg_left IH
no goals
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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
norm_num
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖)
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖)
intro n
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖)
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖)
apply le_trans (hg _).2 _
no goals
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖)
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
no goals
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖)
ring
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖)
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
refine' summable_of_nonneg_of_le (fun n => norm_nonneg _) ule _
no goals
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖)
exact Summable.mul_right _ (summable_geometric_of_lt_1 (by norm_num) (by norm_num))
no goals
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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
norm_num
no goals
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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
norm_num
no goals
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
rw [tsum_geometric_two, mul_assoc]
no goals
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖
ring
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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
intro n
case zero
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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

case succ
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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
induction' n with n IH
no goals
case zero
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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
simp [f.map_zero]
no goals
case succ
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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
rw [sum_range_succ, f.map_add, IH, iterate_succ_apply', sub_add]
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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)
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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))
refine' tendsto_const_nhds.sub _
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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)
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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)
rw [tendsto_iff_norm_tendsto_zero]
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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)
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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)
simp only [sub_zero]
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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)
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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)
refine' squeeze_zero (fun _ => norm_nonneg _) hnle _
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖))
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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)
rw [← MulZeroClass.zero_mul ‖y‖]
no goals
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
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‖))
refine' (_root_.tendsto_pow_atTop_nhds_0_of_lt_1 _ _).mul tendsto_const_nhds <;> norm_num