awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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₁ : Membership.mem (γ := Set E) (ball 0 (↑n : ℝ)) x₁
xz₁ : (f : (a : E) → F) x₁ = z₁
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have hx₂ : ‖x₁‖ < (↑n : ℝ)
Tactic: rw [mem_ball, dist_eq_norm, sub_zero] at hx₁
Cleared hypotheses: hx₁, xz₁
-- 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 : 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₁
⊢ a ∈ ball a ε
have simp : 0 < ε
Tactic: simp only [mem_ball, dist_self]
-- 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 : 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₁
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have this₁ : a ∈ ball a ε
Tactic: have : a ∈ ball a ε := by
      simp only [mem_ball, dist_self]
      exact εpos
-- 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 ε
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have inr : ∀ (z₂ : F) (z₂im : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) z₂)
  (h₂ : dist a z₂ < δ),
  ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
Tactic: rcases Metric.mem_closure_iff.1 (H this) _ δpos with ⟨z₂, z₂im, h₂⟩
-- 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₂
h₂ : dist a z₂ < δ
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have inr : ∀ (x₂ : E) (hx₂ : Membership.mem (γ := Set E) (ball 0 (↑n : ℝ)) x₂) (xz₂ : (f : (a : E) → F) x₂ = z₂),
  ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
Tactic: rcases (mem_image _ _ _).1 z₂im with ⟨x₂, hx₂, xz₂⟩
-- 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₂
h₂ : dist a z₂ < δ
x₂ : E
hx₂ : Membership.mem (γ := Set E) (ball 0 (↑n : ℝ)) x₂
xz₂ : (f : (a : E) → F) x₂ = z₂
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have h₃ : dist a ((f : (a : E) → F) x₂) < δ
Tactic: rw [← xz₂] at h₂
Cleared hypotheses: h₂, hx₂, xz₂
-- 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₂ : Membership.mem (γ := Set E) (ball 0 (↑n : ℝ)) x₂
xz₂ : (f : (a : E) → F) x₂ = z₂
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have hx₃ : ‖x₂‖ < (↑n : ℝ)
Tactic: rw [mem_ball, dist_eq_norm, sub_zero] at hx₂
Cleared hypotheses: hx₂, xz₂
-- 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₂
⊢ ‖HSub.hSub (α := F) ((f : (a : E) → F) x : F) (d • y)‖ =
    ‖HSub.hSub (α := F) ((f : (a : E) → F) x₁ : F) (a + d • y) - HSub.hSub (α := F) ((f : (a : E) → F) x₂ : F) a‖
have e_a : HSub.hSub (α := F) ((f : (a : E) → F) x : F) (d • y) =
  HSub.hSub (α := F) ((f : (a : E) → F) x₁ : F) (a + d • y) - HSub.hSub (α := F) ((f : (a : E) → F) x₂ : F) a
Tactic: congr 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
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₂
⊢ HSub.hSub (α := F) ((f : (a : E) → F) x : F) (d • y) =
    HSub.hSub (α := F) ((f : (a : E) → F) x₁ : F) (a + d • y) - HSub.hSub (α := F) ((f : (a : E) → F) x₂ : F) a
have e_a : HSub.hSub (α := F) (β := F) ((f : (a : E) → F) x₁ : F) ((f : (a : E) → F) x₂ : F) - d • y =
  HSub.hSub (α := F) ((f : (a : E) → F) x₁ : F) (a + d • y) - HSub.hSub (α := F) ((f : (a : E) → F) x₂ : F) a
Tactic: simp only [x, f.map_sub]
-- 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₂
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have I : ‖HSub.hSub (α := F) ((f : (a : E) → F) x : F) (d • y)‖ ≤ 2 * δ
Tactic: have I : ‖f x - d • y‖ ≤ 2 * δ :=
      calc
        ‖f x - d • y‖ = ‖f x₁ - (a + d • y) - (f x₂ - a)‖ := by
          congr 1
          simp only [x, f.map_sub]
          abel
        _ ≤ ‖f x₁ - (a + d • y)‖ + ‖f x₂ - a‖ := norm_sub_le _ _
        _ ≤ 2 * δ := by grind [dist_eq_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
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 * δ
⊢ ‖HSub.hSub (α := F) ((f : (a : E) → F) (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x) : F)
        y‖ =
    ‖HSMul.hSMul (β := F) d⁻¹ ((f : (a : E) → F) x : F) - (d⁻¹ * d) • y‖
have rwa : ‖HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') (β := F) ((σ : (a : 𝕜) → 𝕜') ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) : 𝕜')
        ((f : (a : E) → F) x : F) -
      y‖ =
  ‖HSMul.hSMul (β := F) d⁻¹ ((f : (a : E) → F) x : F) - (d⁻¹ * d) • y‖
Tactic: rwa [f.map_smulₛₗ _, inv_mul_cancel₀, one_smul, map_inv₀, map_inv₀,
            RingHomCompTriple.comp_apply, RingHom.id_apply]
-- 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 * δ
rwa :
  ‖HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') (β := F) ((σ : (a : 𝕜) → 𝕜') ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) : 𝕜')
          ((f : (a : E) → F) x : F) -
        y‖ =
    ‖HSMul.hSMul (β := F) d⁻¹ ((f : (a : E) → F) x : F) - (d⁻¹ * d) • y‖
⊢ ‖HSub.hSub (α := F) ((f : (a : E) → F) (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) x) : F)
        y‖ =
    ‖HSMul.hSMul (β := F) d⁻¹ ((f : (a : E) → F) x : F) - (d⁻¹ * d) • y‖
have rwa₁ : ‖HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') (β := F) ((σ : (a : 𝕜) → 𝕜') ((σ' : (a : 𝕜') → 𝕜) d⁻¹ : 𝕜) : 𝕜')
        ((f : (a : E) → F) x : F) -
      y‖ =
  ‖HSMul.hSMul (β := F) d⁻¹ ((f : (a : E) → F) x : F) - HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') 1 y‖
Tactic: rwa [f.map_smulₛₗ _, inv_mul_cancel₀, one_smul, map_inv₀, map_inv₀,
            RingHomCompTriple.comp_apply, RingHom.id_apply]