awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
K : Type u_1
hK : NormedField K
inst : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H :
  ∀ {γ : ℝ≥0},
    γ ≠ 0 →
      ∃ (x : K),
        x ≠ 0 ∧
          (RankLeOne.hom' valuation : (a : ValueGroup₀ valuation) → ℝ≥0)
              (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                  (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
                x) <
            γ
x : K
hx : x ≠ 0
hxy :
  (RankLeOne.hom' valuation : (a : ValueGroup₀ valuation) → ℝ≥0)
      (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
          (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
        x) <
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
y : K
hy :
  Membership.mem (γ := Set K)
    {x_1 : K |
      LT.lt (α := ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
        (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x_1 :
          ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
        ((↑(Units.mk0
                (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                    (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
                  x)
                ⋯) :
            ValueGroup₀ (F := Valuation K ℝ≥0) valuation) :
          ValueGroup₀ (F := Valuation K ℝ≥0) valuation)}
    y
⊢ y ∈ U
have h₁ : Membership.mem (γ := Set K) (Metric.ball 0 ε) y
Tactic: apply h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
K : Type u_1
hK : NormedField K
inst : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H :
  ∀ {γ : ℝ≥0},
    γ ≠ 0 →
      ∃ (x : K),
        x ≠ 0 ∧
          (RankLeOne.hom' valuation : (a : ValueGroup₀ valuation) → ℝ≥0)
              (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                  (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
                x) <
            γ
x : K
hx : x ≠ 0
hxy :
  (RankLeOne.hom' valuation : (a : ValueGroup₀ valuation) → ℝ≥0)
      (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
          (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
        x) <
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
y : K
hy :
  Membership.mem (γ := Set K)
    {x_1 : K |
      LT.lt (α := ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
        (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x_1 :
          ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
        ((↑(Units.mk0
                (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                    (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
                  x)
                ⋯) :
            ValueGroup₀ (F := Valuation K ℝ≥0) valuation) :
          ValueGroup₀ (F := Valuation K ℝ≥0) valuation)}
    y
⊢ Membership.mem (γ := Set K) (Metric.ball 0 ε) y
have h₁ : ‖y‖ < ε
Tactic: simp only [Metric.mem_ball, dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (hypothesis)
Goal:
K : Type u_1
hK : NormedField K
inst : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H :
  ∀ {γ : ℝ≥0},
    γ ≠ 0 →
      ∃ (x : K),
        x ≠ 0 ∧
          (RankLeOne.hom' valuation : (a : ValueGroup₀ valuation) → ℝ≥0)
              (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                  (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
                x) <
            γ
x : K
hx : x ≠ 0
hxy :
  (RankLeOne.hom' valuation : (a : ValueGroup₀ valuation) → ℝ≥0)
      (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
          (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
        x) <
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
y : K
hy :
  Membership.mem (γ := Set K)
    {x_1 : K |
      LT.lt (α := ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
        (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x_1 :
          ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
        ((↑(Units.mk0
                (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                    (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
                  x)
                ⋯) :
            ValueGroup₀ (F := Valuation K ℝ≥0) valuation) :
          ValueGroup₀ (F := Valuation K ℝ≥0) valuation)}
    y
⊢ ‖y‖ < ε
have hy₁ : (↑(((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) y) : ℝ) < (↑(((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) x) : ℝ)
Tactic: simp only [Units.val_mk0, mem_setOf_eq, restrict_lt_iff, ← NNReal.coe_lt_coe] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
K : Type u_1
hK : NormedField K
inst : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H :
  ∀ {γ : ℝ≥0},
    γ ≠ 0 →
      ∃ (x : K),
        x ≠ 0 ∧
          (RankLeOne.hom' valuation : (a : ValueGroup₀ valuation) → ℝ≥0)
              (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                  (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
                x) <
            γ
x : K
hx : x ≠ 0
hxy :
  (RankLeOne.hom' valuation : (a : ValueGroup₀ valuation) → ℝ≥0)
      (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
          (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
        x) <
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
y : K
hy :
  (↑(((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) y) : ℝ) <
    (↑(((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) x) : ℝ)
⊢ ‖y‖ < ε
have h₁ : (↑(((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) x) : ℝ) < ε
Tactic: apply lt_trans hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
K : Type u_1
hK : NormedField K
inst : IsUltrametricDist K
U : Set K
ε : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ
hε :
  {x : K |
      ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
            (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
          x <
        (↑ε : ValueGroup₀ valuation)} ⊆
    U
⊢ ∃ ε > 0, Metric.ball 0 ε ⊆ U
have refine_2 : (↑((embedding : (a : ValueGroup₀ valuation) → ℝ≥0) (↑ε : ValueGroup₀ valuation)) : ℝ) > 0
Tactic: refine ⟨(embedding ε.1 : ℝ≥0), ?_, fun x hx ↦ hε ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
K : Type u_1
hK : NormedField K
inst : IsUltrametricDist K
U : Set K
ε : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ
hε :
  {x : K |
      ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
            (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
          x <
        (↑ε : ValueGroup₀ valuation)} ⊆
    U
refine_2 : (↑((embedding : (a : ValueGroup₀ valuation) → ℝ≥0) (↑ε : ValueGroup₀ valuation)) : ℝ) > 0
⊢ ∃ ε > 0, Metric.ball 0 ε ⊆ U
have refine_2₁ : ∀ (x : K)
  (hx :
    Membership.mem (γ := Set K)
      (Metric.ball 0 (↑((embedding : (a : ValueGroup₀ valuation) → ℝ≥0) (↑ε : ValueGroup₀ valuation)) : ℝ)) x),
  Membership.mem (γ := Set K)
    {x : K |
      ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
            (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
          x <
        (↑ε : ValueGroup₀ valuation)}
    x
Tactic: refine ⟨(embedding ε.1 : ℝ≥0), ?_, fun x hx ↦ hε ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (hypothesis)
Goal:
K_1 : Type u_1
hK : NormedField K_1
inst : IsUltrametricDist K_1
K : Type u_2
inst_1 : NontriviallyNormedField K
inst_2 : IsUltrametricDist K
x : K
h : 1 < ‖x‖
⊢ Ne (α := ℝ≥0) (((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0) ∧
    Ne (α := ℝ≥0) (((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
have h' : x ≠ 0
Tactic: have h' : x ≠ 0 := norm_eq_zero.not.mp (h.gt.trans' (by simp)).ne'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x y : L
⊢ v.norm (x + y) ≤ max (v.norm x) (v.norm y)
have simp : LE.le.{u_2} (α := ValueGroup₀ v)
    ((v.restrict : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x + y) : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
    ((v.restrict : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀)) ∨
  LE.le.{u_2} (α := ValueGroup₀ v)
    ((v.restrict : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x + y) : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
    ((v.restrict : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) y : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
Tactic: simp only [norm, NNReal.coe_le_coe, le_max_iff, StrictMono.le_iff_le hv.strictMono]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
⊢ 0 < v.norm x ↔ LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀)
have rw : LT.lt.{u_2} (α := ValueGroup₀ v) (0 : ValueGroup₀ v)
    ((v.restrict : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀)) ↔
  LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀)
Tactic: rw [norm_def, ← NNReal.coe_zero, NNReal.coe_lt_coe, ← map_zero (RankOne.hom v),
    StrictMono.lt_iff_lt (RankOne.strictMono v)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
⊢ LT.lt.{u_2} (α := ValueGroup₀ v) (0 : ValueGroup₀ v)
      ((v.restrict : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀)) ↔
    LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀)
have rw : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) ↔ LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀)
Tactic: rw [v.restrict_pos_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
x y : L
⊢ (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x - y))) :
      ℝ) =
    (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (y - x))) :
      ℝ)
have rw : (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
        ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (-(y - x)))) :
    ℝ) =
  (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
        ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (y - x))) :
    ℝ)
Tactic: rw [← neg_sub, Valuation.map_neg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
x y : L
rw :
  (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (-(y - x)))) :
      ℝ) =
    (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (y - x))) :
      ℝ)
⊢ (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x - y))) :
      ℝ) =
    (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (y - x))) :
      ℝ)
have rw₁ : (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
        ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (y - x))) :
    ℝ) =
  (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
        ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (y - x))) :
    ℝ)
Tactic: rw [← neg_sub, Valuation.map_neg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
x y z : L
⊢ Valuation.norm v (x - z) ≤ Valuation.norm v (x - y) + Valuation.norm v (y - z)
have simp : Valuation.norm v (x - y + (y - z)) ≤ Valuation.norm v (x - y) + Valuation.norm v (y - z)
Tactic: simp only [← sub_add_sub_cancel x y z]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (hypothesis)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
⊢ uniformity L = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < ε}
have this : Nonempty { ε : ℝ // ε > 0 }
Tactic: haveI : Nonempty { ε : ℝ // ε > 0 } := nonempty_Ioi_subtype
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
this : Nonempty { ε : ℝ // ε > 0 }
⊢ uniformity L = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < ε}
have h : ∀ (U : Set (L × L)),
  U ∈ uniformity L ↔
    Membership.mem (γ := Filter (L × L)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < ε}) U
Tactic: ext U
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
⊢ U ∈ uniformity L ↔
    Membership.mem (γ := Filter (L × L)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < ε}) U
have h : (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    True ∧
      {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
        U) ↔
  ∃ (i : { ε : ℝ // ε > 0 }),
    Membership.mem (γ := Filter (L × L)) (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑i : ℝ)}) U
Tactic: rw [hasBasis_iff.mp (Valued.hasBasis_uniformity L Γ₀), iInf_subtype', mem_iInf_of_directed]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      True ∧
        {p : L × L |
            (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
          U) ↔
    ∃ (i : { ε : ℝ // ε > 0 }),
      Membership.mem (γ := Filter (L × L)) (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑i : ℝ)}) U
⊢ U ∈ uniformity L ↔
    Membership.mem (γ := Filter (L × L)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < ε}) U
have h₁ : Directed (fun (x1 x2 : Filter (L × L)) ↦ x1 ≥ x2) fun (x : { ε : ℝ // ε > 0 }) ↦
  𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑x : ℝ)}
Tactic: rw [hasBasis_iff.mp (Valued.hasBasis_uniformity L Γ₀), iInf_subtype', mem_iInf_of_directed]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
⊢ (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      True ∧
        {p : L × L |
            (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
          U) ↔
    ∃ (i : { ε : ℝ // ε > 0 }),
      Membership.mem (γ := Filter (L × L)) (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑i : ℝ)}) U
have h : (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
      U) ↔
  ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U
Tactic: simp only [true_and, mem_principal, Subtype.exists, gt_iff_lt, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
⊢ (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
        U) ↔
    ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U
have h : (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
      U) →
  ∀ (ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ)
    (hε :
      {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆
        U),
    ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U
Tactic: refine ⟨fun ⟨ε, hε⟩ => ?_, fun ⟨r, hr_pos, hr⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
        U) →
    ∀ (ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ)
      (hε :
        {p : L × L |
            (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆
          U),
      ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U
⊢ (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
        U) ↔
    ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U
have h₁ : (∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U) →
  ∀ (r : ℝ) (hr_pos : 0 < r) (hr : {p : L × L | Valuation.norm v (p.1 - p.2) < r} ⊆ U),
    ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
        U
Tactic: refine ⟨fun ⟨ε, hε⟩ => ?_, fun ⟨r, hr_pos, hr⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (hypothesis)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
⊢ ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U
have hδ : let δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v);
δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
Tactic: set δ : ℝ≥0 := hv.hom _ ε with hδ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
⊢ 0 < δ
have rw : LT.lt (α := ℝ≥0) (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) 0 : ℝ≥0)
  (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v) :
    ℝ≥0)
Tactic: rw [hδ, ← map_zero hv.hom]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (hypothesis)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
⊢ ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U
have hδ_pos : 0 < δ
Tactic: have hδ_pos : 0 < δ := by
            rw [hδ, ← map_zero hv.hom]
            exact hv.strictMono _ (Units.zero_lt ε)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ_pos : 0 < δ
⊢ ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U
have right : {p : L × L | Valuation.norm v (p.1 - p.2) < (↑δ : ℝ)} ⊆ U
Tactic: use δ, hδ_pos