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)
y : F
h : Membership.mem (γ := Set F) Set.univ y
x : E
hx : (f : (a : E) → F) x = y
n : ℕ
hn : ‖x‖ < (↑n : ℝ)
⊢ Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) y
have refine : Membership.mem (γ := Set E) (ball 0 (↑n : ℝ)) x
Tactic: refine (mem_image _ _ _).2 ⟨x, ⟨?_, hx⟩⟩
-- 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)
y : F
h : Membership.mem (γ := Set F) Set.univ y
x : E
hx : (f : (a : E) → F) x = y
n : ℕ
hn : ‖x‖ < (↑n : ℝ)
⊢ Membership.mem (γ := Set E) (ball 0 (↑n : ℝ)) x
have rwa : dist x 0 < (↑n : ℝ)
Tactic: rwa [mem_ball, dist_eq_norm, sub_zero]
-- 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)
y : F
h : Membership.mem (γ := Set F) Set.univ y
x : E
hx : (f : (a : E) → F) x = y
n : ℕ
hn : ‖x‖ < (↑n : ℝ)
rwa : dist x 0 < (↑n : ℝ)
⊢ Membership.mem (γ := Set E) (ball 0 (↑n : ℝ)) x
have rwa₁ : ‖x - 0‖ < (↑n : ℝ)
Tactic: rwa [mem_ball, dist_eq_norm, sub_zero]
-- 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)
⊢ ∃ C ≥ 0, ∀ (y : F), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
have 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
Tactic: have A : ⋃ n : ℕ, closure (f '' ball 0 n) = Set.univ := by
    refine Subset.antisymm (subset_univ _) fun y _ => ?_
    rcases surj y with ⟨x, hx⟩
    rcases exists_nat_gt ‖x‖ with ⟨n, hn⟩
    refine mem_iUnion.2 ⟨n, subset_closure ?_⟩
    refine (mem_image _ _ _).2 ⟨x, ⟨?_, hx⟩⟩
    rwa [mem_ball, dist_eq_norm, sub_zero]
-- 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
⊢ ∃ C ≥ 0, ∀ (y : F), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
have this : ∃ (n : ℕ) (x : F),
  Membership.mem (γ := Set F)
    (interior
      (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ)))))
    x
Tactic: have : ∃ (n : ℕ) (x : _), x ∈ interior (closure (f '' ball 0 n)) :=
    nonempty_interior_of_iUnion_of_closed (fun n => isClosed_closure) A
-- 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
this :
  ∃ (n : ℕ) (x : F),
    Membership.mem (γ := Set F)
      (interior
        (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
          (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ)))))
      x
⊢ ∃ C ≥ 0, ∀ (y : F), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
have this₁ : ∃ (n : ℕ) (x : F),
  ∃ ε > 0,
    ball x ε ⊆
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ)))
Tactic: simp only [mem_interior_iff_mem_nhds, Metric.mem_nhds_iff] at this
Cleared hypotheses: this
-- 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
this :
  ∃ (n : ℕ) (x : F),
    ∃ ε > 0,
      ball x ε ⊆
        closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
          (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ)))
⊢ ∃ C ≥ 0, ∀ (y : F), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
have rcases : ∀ (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 ≥ 0, ∀ (y : F), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
Tactic: rcases this with ⟨n, a, ε, ⟨εpos, H⟩⟩
Cleared hypotheses: this
-- 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 ≥ 0, ∀ (y : F), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
have rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ∃ C ≥ 0, ∀ (y : F), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
Tactic: rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, 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
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‖
⊢ ∃ C ≥ 0, ∀ (y : F), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
have refine : ∀ (y : F), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
Tactic: refine ⟨(ε / 2)⁻¹ * ‖c‖ * 2 * n, by positivity, 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
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
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have inl : ∃ (x : E),
  dist.{u_4} (α := F) ((f : (a : E) → F) x : F) (0 : F) ≤ 1 / 2 * norm.{u_4} (E := F) 0 ∧
    ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * norm.{u_4} (E := F) 0
Tactic: rcases eq_or_ne y 0 with rfl | hy
Cleared hypotheses: 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
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
inl :
  ∃ (x : E),
    dist.{u_4} (α := F) ((f : (a : E) → F) x : F) (0 : F) ≤ 1 / 2 * norm.{u_4} (E := F) 0 ∧
      ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * norm.{u_4} (E := F) 0
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have inr : ∀ (hy : y ≠ 0), ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
Tactic: rcases eq_or_ne y 0 with rfl | hy
-- 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
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have hc' : 1 < norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜')
Tactic: have hc' : 1 < ‖σ c‖ := by simp only [RingHomIsometric.norm_map, 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
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 : 𝕜')
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have inr : ∀ (d : 𝕜') (hd : d ≠ 0) (ydlt : ‖d • y‖ < ε / 2)
  (dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') * ‖y‖),
  ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
Tactic: rcases rescale_to_shell hc' (half_pos εpos) hy with ⟨d, hd, ydlt, -, dinv⟩
-- 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
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have δpos : 0 < δ
Tactic: have δpos : 0 < δ := by positivity
-- 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 < δ
⊢ ∃ (x : E), dist ((f : (a : E) → F) x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * (↑n : ℝ) * ‖y‖
have this : a + d • y ∈ ball a ε
Tactic: have : a + d • y ∈ ball a ε := by
      simp [dist_eq_norm, lt_of_le_of_lt ydlt.le (half_lt_self ε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 : a + d • y ∈ 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 + d • y) 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 : 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₁
h₁ : dist (a + d • y) 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 : 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₁
h₁ : dist (a + d • y) 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 + d • y) ((f : (a : E) → F) x₁) < δ
Tactic: rw [← xz₁] at h₁
Cleared hypotheses: h₁, hx₁, xz₁