awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₁ : ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₂ : ‖z⁻¹ * (w - z)‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₃ : ‖z⁻¹‖ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₄ : ‖z‖⁻¹ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₅ : ‖z‖⁻¹ * ‖w - z‖ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
rw₆ : ‖w - z‖ * ‖z‖⁻¹ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
rw₇ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = dist z w / (‖z‖ * ‖w‖)
rw₈ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ / (‖z‖ * ‖w‖)
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
have rw₉ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ * (‖z‖ * ‖w‖)⁻¹
Tactic: rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₁ : ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₂ : ‖z⁻¹ * (w - z)‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₃ : ‖z⁻¹‖ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₄ : ‖z‖⁻¹ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₅ : ‖z‖⁻¹ * ‖w - z‖ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
rw₆ : ‖w - z‖ * ‖z‖⁻¹ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
rw₇ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = dist z w / (‖z‖ * ‖w‖)
rw₈ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ / (‖z‖ * ‖w‖)
rw₉ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ * (‖z‖ * ‖w‖)⁻¹
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
have rw₁₀ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹)
Tactic: rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ = 1 ↔ x ≠ 0
have mp : ‖x‖ = 1 → x ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
mp : ‖x‖ = 1 → x ≠ 0
⊢ ‖x‖ = 1 ↔ x ≠ 0
have mpr : x ≠ 0 → ‖x‖ = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : ‖x‖ = 1
⊢ x ≠ 0
have mp : ∀ (hx : x = 0), ‖x‖ ≠ 1
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (hypothesis)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
⊢ ‖x‖ = 1
have this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}
Tactic: have : IsOpen {(0 : 𝕜)} := isOpen_discrete {0}
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (hypothesis)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}
⊢ ‖x‖ = 1
have this₁ : ∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0
Tactic: simp_rw [Metric.isOpen_singleton_iff, dist_eq_norm, sub_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
this : ∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0
⊢ ‖x‖ = 1
have mpr : ∀ (ε : ℝ) (εpos : ε > 0) (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0), ‖x‖ = 1
Tactic: obtain ⟨ε, εpos, h'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
⊢ ‖x‖ = 1
have mpr : ∀
  (H :
    ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
      (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1)
  (h : 1 ≤ ‖x‖), ‖x‖ = 1
Tactic: wlog! h : ‖x‖ < 1 generalizing 𝕜 with H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
mpr :
  ∀
    (H :
      ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
        (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1)
    (h : 1 ≤ ‖x‖), ‖x‖ = 1
⊢ ‖x‖ = 1
have wlog! : ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
  (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
Tactic: wlog! h : ‖x‖ < 1 generalizing 𝕜 with H
Cleared hypotheses: inst_1, x, hx, h'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
h : 1 ≤ ‖x‖
⊢ ‖x‖ = 1
have mpr : ∀ (h : 1 = ‖x‖), ‖x‖ = 1
Tactic: rcases h.eq_or_lt with h | h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
h : 1 ≤ ‖x‖
mpr : ∀ (h : 1 = ‖x‖), ‖x‖ = 1
⊢ ‖x‖ = 1
have mpr₁ : ∀ (h : 1 < ‖x‖), ‖x‖ = 1
Tactic: rcases h.eq_or_lt with h | h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
h_1 : 1 ≤ ‖x‖
h : 1 = ‖x‖
⊢ ‖x‖ = 1
have mpr : ‖x‖ = ‖x‖
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (hypothesis)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
h_1 : 1 ≤ ‖x‖
h : 1 < ‖x‖
⊢ ‖x‖ = 1
have h₁ : ‖x⁻¹‖ < 1
Tactic: replace h := norm_inv x ▸ inv_lt_one_of_one_lt₀ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
h_1 : 1 ≤ ‖x‖
h : ‖x⁻¹‖ < 1
⊢ ‖x‖ = 1
have mpr : ‖x⁻¹‖ = 1
Tactic: rw [← inv_inj, inv_one, ← norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜_1 : Type u_5
inst : NormedDivisionRing 𝕜_1
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst_1 : NormedDivisionRing 𝕜
inst_2 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
⊢ ‖x‖ = 1
have obtain : ∀ (k : ℕ) (hk : ‖x‖ ^ k < ε), ‖x‖ = 1
Tactic: obtain ⟨k, hk⟩ : ∃ k : ℕ, ‖x‖ ^ k < ε := exists_pow_lt_of_lt_one εpos h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (hypothesis)
Goal:
𝕜_1 : Type u_5
inst : NormedDivisionRing 𝕜_1
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst_1 : NormedDivisionRing 𝕜
inst_2 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
k : ℕ
hk : ‖x‖ ^ k < ε
⊢ ‖x‖ = 1
have hk₁ : ‖x ^ k‖ < ε
Tactic: rw [← norm_pow] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (hypothesis)
Goal:
𝕜_1 : Type u_5
inst : NormedDivisionRing 𝕜_1
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst_1 : NormedDivisionRing 𝕜
inst_2 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
k : ℕ
hk : ‖x ^ k‖ < ε
⊢ ‖x‖ = 1
have h'₁ : x ^ k = 0
Tactic: specialize h' _ hk
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ ≤ 1
have inl : norm.{u_5} (E := 𝕜) 0 ≤ 1
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
inl : norm.{u_5} (E := 𝕜) 0 ≤ 1
⊢ ‖x‖ ≤ 1
have inr : ∀ (hx : x ≠ 0), ‖x‖ ≤ 1
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
⊢ Eq.{u_5 + 1} (α := Set 𝕜) (Metric.closedBall 0 1) Set.univ
have h : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 1) x ↔ Membership.mem (γ := Set 𝕜) Set.univ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ≥0∞
hr : r ≠ ∞
⊢ ∃ (x : α), r < ‖x‖ₑ
have lift : ∀ (r : ℝ≥0), ∃ (x : α), (↑r : ℝ≥0∞) < ‖x‖ₑ
Tactic: lift r to ℝ≥0 using hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r
have rwa : ‖w⁻¹‖ ∈ Set.Ioo 0 r
Tactic: rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
rwa : ‖w⁻¹‖ ∈ Set.Ioo 0 r
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r
have rwa₁ : ‖w‖⁻¹ ∈ Set.Ioo 0 r
Tactic: rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
rwa : ‖w⁻¹‖ ∈ Set.Ioo 0 r
rwa₁ : ‖w‖⁻¹ ∈ Set.Ioo 0 r
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r
have rwa₂ : ‖w‖ ∈ (Set.Ioo 0 r)⁻¹
Tactic: rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
rwa : ‖w⁻¹‖ ∈ Set.Ioo 0 r
rwa₁ : ‖w‖⁻¹ ∈ Set.Ioo 0 r
rwa₂ : ‖w‖ ∈ (Set.Ioo 0 r)⁻¹
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r
have rwa₃ : ‖w‖ ∈ Set.Ioi r⁻¹
Tactic: rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NontriviallyNormedField α
x : α
⊢ (𝓝[≠] x).NeBot
have rw : ∀ ε > 0, ∃ (b : α), Membership.mem (γ := Set α) {x}ᶜ b ∧ dist x b < ε
Tactic: rw [← mem_closure_iff_nhdsWithin_neBot, Metric.mem_closure_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
⊢ ∃ (b : α), Membership.mem (γ := Set α) {x}ᶜ b ∧ dist x b < ε
have rcases : ∀ (b : α) (hb0 : 0 < ‖b‖) (hbε : ‖b‖ < ε), ∃ (b : α), Membership.mem (γ := Set α) {x}ᶜ b ∧ dist x b < ε
Tactic: rcases exists_norm_lt α ε0 with ⟨b, hb0, hbε⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ ∃ (b : α), Membership.mem (γ := Set α) {x}ᶜ b ∧ dist x b < ε
have refine : dist x (x + b) < ε
Tactic: refine ⟨x + b, mt (Set.mem_singleton_iff.trans add_eq_left).1 <| norm_pos_iff.1 hb0, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ dist x (x + b) < ε
have rwa : dist (x + b) x < ε
Tactic: rwa [dist_comm, dist_eq_norm, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
rwa : dist (x + b) x < ε
⊢ dist x (x + b) < ε
have rwa₁ : ‖x + b - x‖ < ε
Tactic: rwa [dist_comm, dist_eq_norm, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : DenselyNormedField α
x y : α
hxy :
  LT.lt (α := (↑(Set.range.{0, u_2 + 1} (ι := α) norm) : Type))
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖x‖ ⋯)
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯)
⊢ ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) norm) : Type)),
    Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖x‖ ⋯ < a ∧
      a < Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯
have let : ∀ (z : α)
  (h : ‖x‖ < ‖z‖ ∧ ‖z‖ < (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ sorry) : ℝ)),
  ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) norm) : Type)),
    Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖x‖ sorry < a ∧
      a < Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ sorry
Tactic: let ⟨z, h⟩ := exists_lt_norm_lt α (norm_nonneg _) hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : DenselyNormedField α
x y : α
hxy :
  LT.lt (α := (↑(Set.range.{0, u_2 + 1} (ι := α) nnnorm) : Type))
    (Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯)
    (Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯)
⊢ ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) nnnorm) : Type)),
    Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯ < a ∧
      a < Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯
have let : ∀ (z : α)
  (h :
    (↑(Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ sorry) : ℝ≥0) < ‖z‖₊ ∧
      ‖z‖₊ < (↑(Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ sorry) : ℝ≥0)),
  ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) nnnorm) : Type)),
    Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ sorry < a ∧
      a < Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ sorry
Tactic: let ⟨z, h⟩ := exists_lt_nnnorm_lt α hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
h : ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ ∃ (x : 𝕜), 1 < ‖x‖
have rcases : ∀ (x : 𝕜) (hx : x ≠ 0) (hx1 : ‖x‖ ≠ 1), ∃ (x : 𝕜), 1 < ‖x‖
Tactic: rcases h with ⟨x, hx, hx1⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
⊢ ∃ (x : 𝕜), 1 < ‖x‖
have inl : ∀ (hlt : ‖x‖ < 1), ∃ (x : 𝕜), 1 < ‖x‖
Tactic: rcases hx1.lt_or_gt with hlt | hlt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
inl : ∀ (hlt : ‖x‖ < 1), ∃ (x : 𝕜), 1 < ‖x‖
⊢ ∃ (x : 𝕜), 1 < ‖x‖
have inr : ∀ (hlt : 1 < ‖x‖), ∃ (x : 𝕜), 1 < ‖x‖
Tactic: rcases hx1.lt_or_gt with hlt | hlt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : ‖x‖ < 1
⊢ ∃ (x : 𝕜), 1 < ‖x‖
have h : 1 < ‖x⁻¹‖
Tactic: use x⁻¹
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : ‖x‖ < 1
⊢ 1 < ‖x⁻¹‖
have h : 1 < ‖x‖⁻¹
Tactic: rw [norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
x_1 x_2 : ℝ
h₀ : 0 ≤ x_1
hr : x_1 < x_2
x : ℝ
h : x_1 < x ∧ x < x_2
⊢ x_1 < ‖x‖ ∧ ‖x‖ < x_2
have rwa : x_1 < |x| ∧ |x| < x_2
Tactic: rwa [Real.norm_eq_abs, abs_of_nonneg (h₀.trans h.1.le)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ x.toNNReal * ‖y‖₊ = ‖x * y‖₊
have a : (↑(x.toNNReal * ‖y‖₊) : ℝ) = (↑‖x * y‖₊ : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
⊢ ‖x‖₊ * y.toNNReal = ‖x * y‖₊
have rw : y.toNNReal * ‖x‖₊ = ‖x * y‖₊
Tactic: rw [mul_comm, mul_comm x, toNNReal_mul_nnnorm x hy]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : y.toNNReal * ‖x‖₊ = ‖x * y‖₊
⊢ ‖x‖₊ * y.toNNReal = ‖x * y‖₊
have rw₁ : y.toNNReal * ‖x‖₊ = ‖y * x‖₊
Tactic: rw [mul_comm, mul_comm x, toNNReal_mul_nnnorm x hy]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
rw : y.toNNReal * ‖x‖₊ = ‖x * y‖₊
rw₁ : y.toNNReal * ‖x‖₊ = ‖y * x‖₊
⊢ ‖x‖₊ * y.toNNReal = ‖x * y‖₊
have rw₂ : ‖y * x‖₊ = ‖y * x‖₊
Tactic: rw [mul_comm, mul_comm x, toNNReal_mul_nnnorm x hy]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
⊢ IsAlgClosed L
have H : ∀ (p : L[X]), p.Monic → Irreducible p → ∃ (x : L), eval x p = 0
Tactic: apply IsAlgClosed.of_exists_root
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
⊢ ∃ (x : L), eval x f = 0
have fnatdeg0 : f.natDegree ≠ 0
Tactic: have fnatdeg0 : f.natDegree ≠ 0 := (Irreducible.natDegree_pos firr).ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
⊢ Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
have rw : eval a (map (algebraMap L f.SplittingField) f) = 0
Tactic: rw [← eval_map_algebraMap]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
⊢ ∃ (x : L), eval x f = 0
have fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
Tactic: have fa0 : f.aeval a = 0 := by
    rw [← eval_map_algebraMap]
    exact eval_rootOfSplits (Polynomial.SplittingField.splits f)
      (by simpa using degree_ne_of_natDegree_ne fnatdeg0)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
⊢ δ ≤ ‖a - a'‖
have pos : ∀ (hS : S.Nonempty), δ ≤ ‖a - a'‖
Tactic: by_cases hS : S.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
pos : ∀ (hS : S.Nonempty), δ ≤ ‖a - a'‖
⊢ δ ≤ ‖a - a'‖
have neg : ∀ (hS : ¬S.Nonempty), δ ≤ ‖a - a'‖
Tactic: by_cases hS : S.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : S.Nonempty
⊢ δ ≤ ‖a - a'‖
have pos : Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) sorry ≤ ‖a - a'‖
Tactic: simp only [hS, ↓reduceDIte, δ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : ¬S.Nonempty
⊢ δ ≤ ‖a - a'‖
have neg : 1 ≤ ‖a - a'‖
Tactic: simp only [hS, ↓reduceDIte, δ]