awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ :
  Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ ((f : (a : E) → F) (∑ i ∈ Finset.range n, u i) : F)) atTop
    (𝓝 ((f : (a : E) → F) x) : Filter F)
⊢ Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)

Tactic:
simp only [fsumeq] at L₁
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
⊢ Tendsto (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 (y - 0))

Tactic:
tendsto_const_nhds.sub ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
refine : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ h^[n] y) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 (y - 0))

Tactic:
refine tendsto_const_nhds.sub ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
rw : Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖h^[e] y - 0‖) atTop (𝓝 0)
⊢ Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ h^[n] y) atTop (𝓝 0)

Tactic:
rw [tendsto_iff_norm_sub_tendsto_zero]

Premises used: tendsto_iff_norm_sub_tendsto_zero
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
simp : Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖h^[e] y‖) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖h^[e] y - 0‖) atTop (𝓝 0)

Tactic:
simp only [sub_zero]

Premises used: sub_zero
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
⊢ Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖h^[e] y‖) atTop (𝓝 0)

Tactic:
squeeze_zero (fun _ => norm_nonneg _) hnle ?_

Premises used: squeeze_zero, Nat.iterate, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
refine : Tendsto (β := ℝ) (fun (t : ℕ) ↦ (1 / 2) ^ t * ‖y‖) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖h^[e] y‖) atTop (𝓝 0)

Tactic:
refine squeeze_zero (fun _ => norm_nonneg _) hnle ?_

Premises used: squeeze_zero, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
rw : Tendsto (fun (t : ℕ) ↦ (1 / 2) ^ t * ‖y‖) atTop (𝓝 (0 * ‖y‖))
⊢ Tendsto (β := ℝ) (fun (t : ℕ) ↦ (1 / 2) ^ t * ‖y‖) atTop (𝓝 0)

Tactic:
rw [← zero_mul ‖y‖]

Premises used: Norm.norm, MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
⊢ Tendsto (fun (t : ℕ) ↦ (1 / 2) ^ t * ‖y‖) atTop (𝓝 (0 * ‖y‖))

Tactic:
(_root_.tendsto_pow_atTop_nhds_zero_of_lt_one ?_ ?_).mul tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.mul, tendsto_pow_atTop_nhds_zero_of_lt_one
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
refine_1 : 0 ≤ 1 / 2
refine_2 : 1 / 2 < 1
⊢ Tendsto (fun (t : ℕ) ↦ (1 / 2) ^ t * ‖y‖) atTop (𝓝 (0 * ‖y‖))

Tactic:
refine (_root_.tendsto_pow_atTop_nhds_zero_of_lt_one ?_ ?_).mul tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.mul, tendsto_pow_atTop_nhds_zero_of_lt_one
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
⊢ 0 ≤ 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
⊢ 1 / 2 < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
⊢ Tendsto (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 (y - 0))

Tactic:
have L₂ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (y - 0)) := by
    refine tendsto_const_nhds.sub ?_
    rw [tendsto_iff_norm_sub_tendsto_zero]
    simp only [sub_zero]
    refine squeeze_zero (fun _ => norm_nonneg _) hnle ?_
    rw [← zero_mul ‖y‖]
    refine (_root_.tendsto_pow_atTop_nhds_zero_of_lt_one ?_ ?_).mul tendsto_const_nhds <;> norm_num
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
L₂ : Tendsto (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 (y - 0))
⊢ (f : (a : E) → F) x = y - 0

Tactic:
have feq : f x = y - 0 := tendsto_nhds_unique L₁ L₂
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
L₂ : Tendsto (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 (y - 0))
feq : (f : (a : E) → F) x = y - 0
⊢ (f : (a : E) → F) x = y

Tactic:
rw [sub_zero] at feq

Premises used: sub_zero
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
L₂ : Tendsto (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 (y - 0))
feq : (f : (a : E) → F) x = y
⊢ ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖

Tactic:
⟨x, feq, x_ineq⟩

Premises used: And.intro, Exists.intro