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
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
A :
  Eq.{u_4 + 1} (α := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H :
  ball a ε ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ)))
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜')
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this_1 : a + d • y ∈ ball a ε
z₁ : F
z₁im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₁
x₁ : E
h₁ : dist (a + d • y) ((f : (a : E) → F) x₁) < δ
hx₁ : ‖x₁‖ < (↑n : ℝ)
xz₁ : (f : (a : E) → F) x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₂
x₂ : E
h₂ : dist a ((f : (a : E) → F) x₂) < δ
hx₂ : ‖x₂‖ < (↑n : ℝ)
xz₂ : (f : (a : E) → F) x₂ = z₂
x : E := x₁ - x₂
I : ‖HSub.hSub (α := F) ((f : (a : E) → F) x : F) (d • y)‖ ≤ 2 * δ
J : dist ((f : (a : E) → F) (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖
have rw : norm.{u_1} (E := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) * ‖x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖
Tactic: rw [norm_smul, RingHomIsometric.norm_map, norm_inv]
-- 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
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
A :
  Eq.{u_4 + 1} (α := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H :
  ball a ε ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ)))
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜')
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this_1 : a + d • y ∈ ball a ε
z₁ : F
z₁im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₁
x₁ : E
h₁ : dist (a + d • y) ((f : (a : E) → F) x₁) < δ
hx₁ : ‖x₁‖ < (↑n : ℝ)
xz₁ : (f : (a : E) → F) x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₂
x₂ : E
h₂ : dist a ((f : (a : E) → F) x₂) < δ
hx₂ : ‖x₂‖ < (↑n : ℝ)
xz₂ : (f : (a : E) → F) x₂ = z₂
x : E := x₁ - x₂
I : ‖HSub.hSub (α := F) ((f : (a : E) → F) x : F) (d • y)‖ ≤ 2 * δ
J : dist ((f : (a : E) → F) (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x)) y ≤ 1 / 2 * ‖y‖
rw : norm.{u_1} (E := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) * ‖x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖
⊢ ‖HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖
have rw₁ : ‖d⁻¹‖ * ‖x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖
Tactic: rw [norm_smul, RingHomIsometric.norm_map, norm_inv]
-- 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
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
A :
  Eq.{u_4 + 1} (α := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H :
  ball a ε ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ)))
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜')
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this_1 : a + d • y ∈ ball a ε
z₁ : F
z₁im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₁
x₁ : E
h₁ : dist (a + d • y) ((f : (a : E) → F) x₁) < δ
hx₁ : ‖x₁‖ < (↑n : ℝ)
xz₁ : (f : (a : E) → F) x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₂
x₂ : E
h₂ : dist a ((f : (a : E) → F) x₂) < δ
hx₂ : ‖x₂‖ < (↑n : ℝ)
xz₂ : (f : (a : E) → F) x₂ = z₂
x : E := x₁ - x₂
I : ‖HSub.hSub (α := F) ((f : (a : E) → F) x : F) (d • y)‖ ≤ 2 * δ
J : dist ((f : (a : E) → F) (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x)) y ≤ 1 / 2 * ‖y‖
rw : norm.{u_1} (E := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) * ‖x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖
rw₁ : ‖d⁻¹‖ * ‖x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖
⊢ ‖HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖
have rw₂ : ‖d‖⁻¹ * ‖x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖
Tactic: rw [norm_smul, RingHomIsometric.norm_map, norm_inv]
-- 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
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
A :
  Eq.{u_4 + 1} (α := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H :
  ball a ε ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ)))
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜')
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this_1 : a + d • y ∈ ball a ε
z₁ : F
z₁im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₁
x₁ : E
h₁ : dist (a + d • y) ((f : (a : E) → F) x₁) < δ
hx₁ : ‖x₁‖ < (↑n : ℝ)
xz₁ : (f : (a : E) → F) x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₂
x₂ : E
h₂ : dist a ((f : (a : E) → F) x₂) < δ
hx₂ : ‖x₂‖ < (↑n : ℝ)
xz₂ : (f : (a : E) → F) x₂ = z₂
x : E := x₁ - x₂
I : ‖HSub.hSub (α := F) ((f : (a : E) → F) x : F) (d • y)‖ ≤ 2 * δ
J : dist ((f : (a : E) → F) (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖d‖⁻¹ * ‖x₁ - x₂‖ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)
have h₃ : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖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
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
A :
  Eq.{u_4 + 1} (α := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H :
  ball a ε ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ)))
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜')
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this_1 : a + d • y ∈ ball a ε
z₁ : F
z₁im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₁
x₁ : E
h₁ : dist (a + d • y) ((f : (a : E) → F) x₁) < δ
hx₁ : ‖x₁‖ < (↑n : ℝ)
xz₁ : (f : (a : E) → F) x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₂
x₂ : E
h₂ : dist a ((f : (a : E) → F) x₂) < δ
hx₂ : ‖x₂‖ < (↑n : ℝ)
xz₂ : (f : (a : E) → F) x₂ = z₂
x : E := x₁ - x₂
I : ‖HSub.hSub (α := F) ((f : (a : E) → F) x : F) (d • y)‖ ≤ 2 * δ
J : dist ((f : (a : E) → F) (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x)) y ≤ 1 / 2 * ‖y‖
h₃ : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
⊢ ‖d‖⁻¹ * ‖x₁ - x₂‖ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)
have h₄ : ‖x₁ - x₂‖ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)
Tactic: gcongr
-- 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
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
A :
  Eq.{u_4 + 1} (α := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H :
  ball a ε ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ)))
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜')
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this_1 : a + d • y ∈ ball a ε
z₁ : F
z₁im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₁
x₁ : E
h₁ : dist (a + d • y) ((f : (a : E) → F) x₁) < δ
hx₁ : ‖x₁‖ < (↑n : ℝ)
xz₁ : (f : (a : E) → F) x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₂
x₂ : E
h₂ : dist a ((f : (a : E) → F) x₂) < δ
hx₂ : ‖x₂‖ < (↑n : ℝ)
xz₂ : (f : (a : E) → F) x₂ = z₂
x : E := x₁ - x₂
I : ‖HSub.hSub (α := F) ((f : (a : E) → F) x : F) (d • y)‖ ≤ 2 * δ
J : dist ((f : (a : E) → F) (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x)) y ≤ 1 / 2 * ‖y‖
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have K : ‖HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
Tactic: have K : ‖σ' d⁻¹ • x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖ :=
      calc
        ‖σ' d⁻¹ • x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖ := by rw [norm_smul, RingHomIsometric.norm_map, norm_inv]
        _ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖ * (n + n) := by
          gcongr
          · simpa using dinv
          · exact le_trans (norm_sub_le _ _) (by gcongr)
        _ = (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖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 > 0, ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
have obtain : ∀ (C : ℝ) (C0 : C ≥ 0) (hC : ∀ (y : F), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖),
  ∃ C > 0, ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
Tactic: obtain ⟨C, C0, hC⟩ := exists_approx_preimage_norm_le f surj
-- 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
hC : ∀ (y : F), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
⊢ ∃ C > 0, ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
have choose : ∀ (g : (y : F) → E) (hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖),
  ∃ C > 0, ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
Tactic: choose g hg using hC
Cleared hypotheses: hC
-- 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)
y : F
⊢ ‖h y‖ ≤ 1 / 2 * ‖y‖
have rw : dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖
Tactic: rw [← dist_eq_norm, dist_comm]
-- 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)
⊢ ∃ C > 0, ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
have hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
Tactic: have hle : ∀ y, ‖h y‖ ≤ 1 / 2 * ‖y‖ := by
    intro y
    rw [← dist_eq_norm, dist_comm]
    exact (hg y).1
-- 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‖
⊢ 2 * C + 1 > 0
have linarith : 2 * C + 1 ≤ 0 → -1 + 2 * (0 - C) + (2 * C + 1 - 0) = 0
Tactic: linarith
-- 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‖
linarith : 2 * C + 1 ≤ 0 → -1 + 2 * (0 - C) + (2 * C + 1 - 0) = 0
⊢ 2 * C + 1 > 0
have linarith₁ : 2 * C + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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‖
⊢ ∃ C > 0, ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
have refine : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
Tactic: refine ⟨2 * C + 1, by linarith, fun y => ?_⟩
-- 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 : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ ‖h^[n + 1] y‖ ≤ (1 / 2) ^ (n + 1) * ‖y‖
have succ : ‖(h ∘ h^[n]) y‖ ≤ (1 / 2) ^ (n + 1) * ‖y‖
Tactic: rw [iterate_succ']
-- 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 : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ ‖(h ∘ h^[n]) y‖ ≤ (1 / 2) ^ (n + 1) * ‖y‖
have apply : 1 / 2 * ‖h^[n] y‖ ≤ (1 / 2) ^ (n + 1) * ‖y‖
Tactic: apply le_trans (hle _) _
-- 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 : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ 1 / 2 * ‖h^[n] y‖ ≤ (1 / 2) ^ (n + 1) * ‖y‖
have rw : 1 / 2 * ‖h^[n] y‖ ≤ 1 / 2 * ((1 / 2) ^ n * ‖y‖)
Tactic: rw [pow_succ', 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
n : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ 1 / 2 * ‖h^[n] y‖ ≤ 1 / 2 * ((1 / 2) ^ n * ‖y‖)
have ha : 0 ≤ 1 / 2
Tactic: gcongr