awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
n : ℕ
⊢ ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
have zero : ‖h^[0] y‖ ≤ HPow.hPow (β := ℕ) (1 / 2) 0 * ‖y‖
Tactic: induction n with
    | zero => simp only [one_div, one_mul, iterate_zero_apply, pow_zero, le_rfl]
    | succ n IH =>
      rw [iterate_succ']
      apply le_trans (hle _) _
      rw [pow_succ', mul_assoc]
      gcongr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
n : ℕ
zero : ‖h^[0] y‖ ≤ HPow.hPow (β := ℕ) (1 / 2) 0 * ‖y‖
⊢ ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
have succ : ∀ (n : ℕ) (IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖), ‖h^[n + 1] y‖ ≤ (1 / 2) ^ (n + 1) * ‖y‖
Tactic: induction n with
    | zero => simp only [one_div, one_mul, iterate_zero_apply, pow_zero, le_rfl]
    | succ n IH =>
      rw [iterate_succ']
      apply le_trans (hle _) _
      rw [pow_succ', mul_assoc]
      gcongr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
⊢ ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
have hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
Tactic: have hnle : ∀ n : ℕ, ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖ := by
    intro n
    induction n with
    | zero => simp only [one_div, one_mul, iterate_zero_apply, pow_zero, le_rfl]
    | succ n IH =>
      rw [iterate_succ']
      apply le_trans (hle _) _
      rw [pow_succ', mul_assoc]
      gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → E := fun (n : ℕ) ↦ g (h^[n] y)
n : ℕ
⊢ ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
have apply : C * ‖h^[n] y‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
Tactic: apply le_trans (hg _).2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → E := fun (n : ℕ) ↦ g (h^[n] y)
n : ℕ
⊢ C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖)
have hbc : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → E := fun (n : ℕ) ↦ g (h^[n] y)
n : ℕ
⊢ C * ‖h^[n] y‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
have C₁ : C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖)
Tactic: calc
      C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖) := by gcongr; exact hnle n
      _ = (1 / 2) ^ n * (C * ‖y‖) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → E := fun (n : ℕ) ↦ g (h^[n] y)
n : ℕ
C₁ : C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖)
⊢ C * ‖h^[n] y‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
have C₂ : C * ((1 / 2) ^ n * ‖y‖) = (1 / 2) ^ n * (C * ‖y‖)
Tactic: calc
      C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖) := by gcongr; exact hnle n
      _ = (1 / 2) ^ n * (C * ‖y‖) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → E := fun (n : ℕ) ↦ g (h^[n] y)
⊢ ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
have ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
Tactic: have ule : ∀ n, ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖) := fun n ↦ by
    apply le_trans (hg _).2
    calc
      C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖) := by gcongr; exact hnle n
      _ = (1 / 2) ^ n * (C * ‖y‖) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → E := fun (n : ℕ) ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖u n‖
have refine : Summable (α := ℝ) fun (b : ℕ) ↦ (1 / 2) ^ b * (C * ‖y‖)
Tactic: refine .of_nonneg_of_le (fun n => norm_nonneg _) ule ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → E := fun (n : ℕ) ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
⊢ ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
have sNu : Summable (α := ℝ) fun (n : ℕ) ↦ ‖u n‖
Tactic: have sNu : Summable fun n => ‖u n‖ := by
    refine .of_nonneg_of_le (fun n => norm_nonneg _) ule ?_
    exact Summable.mul_right _ (summable_geometric_of_lt_one (by simp) (by norm_num))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → E := fun (n : ℕ) ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable (α := ℝ) fun (n : ℕ) ↦ ‖u n‖
⊢ ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
have su : Summable u
Tactic: have su : Summable u := sNu.of_norm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → 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‖
have rw : 2 * (C * ‖y‖) = 2 * C * ‖y‖
Tactic: rw [tsum_geometric_two, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → 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
rw : 2 * (C * ‖y‖) = 2 * C * ‖y‖
⊢ (∑' (n : ℕ), (1 / 2) ^ n) * (C * ‖y‖) = 2 * C * ‖y‖
have rw₁ : 2 * (C * ‖y‖) = 2 * (C * ‖y‖)
Tactic: rw [tsum_geometric_two, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → 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 : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
have x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
Tactic: 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‖) :=
        sNu.tsum_le_tsum ule <| 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → 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 : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
⊢ (f : (a : E) → F) (∑ i ∈ Finset.range (n + 1), u i) = y - h^[n + 1] y
have succ : (f : (a : E) → F) (∑ x ∈ Finset.range n, u x + u n) = y - h^[n + 1] y
Tactic: rw [sum_range_succ, f.map_add, IH, iterate_succ_apply', sub_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → 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 : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
succ : (f : (a : E) → F) (∑ x ∈ Finset.range n, u x + u n) = y - h^[n + 1] y
⊢ (f : (a : E) → F) (∑ i ∈ Finset.range (n + 1), u i) = y - h^[n + 1] y
have succ₁ : HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) (∑ x ∈ Finset.range n, u x) : F) ((f : (a : E) → F) (u n) : F) =
  y - h^[n + 1] y
Tactic: rw [sum_range_succ, f.map_add, IH, iterate_succ_apply', sub_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → 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 : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
succ : (f : (a : E) → F) (∑ x ∈ Finset.range n, u x + u n) = y - h^[n + 1] y
succ₁ :
  HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) (∑ x ∈ Finset.range n, u x) : F) ((f : (a : E) → F) (u n) : F) =
    y - h^[n + 1] y
⊢ (f : (a : E) → F) (∑ i ∈ Finset.range (n + 1), u i) = y - h^[n + 1] y
have succ₂ : HAdd.hAdd (β := F) (y - h^[n] y) ((f : (a : E) → F) (u n) : F) = y - h^[n + 1] y
Tactic: rw [sum_range_succ, f.map_add, IH, iterate_succ_apply', sub_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → 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 : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
succ : (f : (a : E) → F) (∑ x ∈ Finset.range n, u x + u n) = y - h^[n + 1] y
succ₁ :
  HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) (∑ x ∈ Finset.range n, u x) : F) ((f : (a : E) → F) (u n) : F) =
    y - h^[n + 1] y
succ₂ : HAdd.hAdd (β := F) (y - h^[n] y) ((f : (a : E) → F) (u n) : F) = y - h^[n + 1] y
⊢ (f : (a : E) → F) (∑ i ∈ Finset.range (n + 1), u i) = y - h^[n + 1] y
have succ₃ : HAdd.hAdd (β := F) (y - h^[n] y) ((f : (a : E) → F) (u n) : F) = y - h (h^[n] y)
Tactic: rw [sum_range_succ, f.map_add, IH, iterate_succ_apply', sub_add]