awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
⊢ IsClopen.{u_1} (X := R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
have h : Eq.{u_1 + 1} (α := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
  ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
    {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
Tactic: have h : {x : R | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r} := by
    ext x
    simp [← le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
    ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
⊢ IsClopen.{u_1} (X := R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
have rw : IsClopen.{u_1} (X := R)
  ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
    {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
⊢ IsClosed[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
have inl : IsClosed[_t]
  {x : R |
    Eq.{u_3 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (0 : ValueGroup₀ v)}
Tactic: rcases eq_or_ne r 0 with rfl | hr
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
inl :
  IsClosed[_t]
    {x : R |
      Eq.{u_3 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ v)}
⊢ IsClosed[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
have inr : ∀ (hr : r ≠ 0), IsClosed[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
Tactic: rcases eq_or_ne r 0 with rfl | hr
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
⊢ IsClosed[_t]
    {x : R |
      Eq.{u_3 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ v)}
have h : ∀ (x : R),
  Eq.{u_3 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (0 : ValueGroup₀ v) ↔
    LE.le.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (0 : ValueGroup₀ v)
Tactic: convert! v.isClosed_closedBall 0 using 3
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
⊢ IsOpen[_t] (↑v.integer : Set R)
have simp : IsOpen[_t]
  {x : R |
    LE.le.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}
Tactic: simp only [integer, Subring.coe_set_mk, Subsemiring.coe_set_mk, Submonoid.coe_set_mk,
    Subsemigroup.coe_set_mk, ← v.restrict_le_one_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
⊢ IsClosed[_t] (↑v.integer : Set R)
have simp : IsClosed[_t]
  {x : R |
    LE.le.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}
Tactic: simp only [integer, Subring.coe_set_mk, Subsemiring.coe_set_mk, Submonoid.coe_set_mk,
    Subsemigroup.coe_set_mk, ← v.restrict_le_one_iff]
-- 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
⊢ Membership.mem (γ := Filter K) (nhds 0) U ↔
    ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
      {x : K |
          ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
              x <
            (↑γ : ValueGroup₀ valuation)} ⊆
        U
have rw : (∃ ε > 0, Metric.ball 0 ε ⊆ U) ↔
  ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    {x : K |
        ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x <
          (↑γ : ValueGroup₀ valuation)} ⊆
      U
Tactic: rw [Metric.mem_nhds_iff]
-- 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
⊢ (∃ ε > 0, Metric.ball 0 ε ⊆ U) ↔
    ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
      {x : K |
          ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
              x <
            (↑γ : ValueGroup₀ valuation)} ⊆
        U
have refine_1 : (∃ ε > 0, Metric.ball 0 ε ⊆ U) →
  ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    {x : K |
        ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x <
          (↑γ : ValueGroup₀ valuation)} ⊆
      U
Tactic: refine ⟨?_, ?_⟩
-- 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
refine_1 :
  (∃ ε > 0, Metric.ball 0 ε ⊆ U) →
    ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
      {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) ↔
    ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
      {x : K |
          ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
              x <
            (↑γ : ValueGroup₀ valuation)} ⊆
        U
have refine_2 : (∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    {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
Tactic: refine ⟨?_, ?_⟩
-- 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
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    {x : K |
        ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x <
          (↑γ : ValueGroup₀ valuation)} ⊆
      U
have refine_1 : ∀ (H : Subsingleton (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
  ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    {x : K |
        ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x <
          (↑γ : ValueGroup₀ valuation)} ⊆
      U
Tactic: rcases RankLeOne.exists_val_lt (valuation (K := K)) with H | 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
refine_1 :
  ∀ (H : Subsingleton (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
      {x : K |
          ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
              x <
            (↑γ : ValueGroup₀ valuation)} ⊆
        U
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    {x : K |
        ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x <
          (↑γ : ValueGroup₀ valuation)} ⊆
      U
have refine_1₁ : ∀
  (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) <
              γ),
  ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    {x : K |
        ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x <
          (↑γ : ValueGroup₀ valuation)} ⊆
      U
Tactic: rcases RankLeOne.exists_val_lt (valuation (K := K)) with H | 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 : Subsingleton (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    {x : K |
        ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x <
          (↑γ : ValueGroup₀ valuation)} ⊆
      U
have h₁ : {x : K |
    ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
          (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
        x <
      (↑(Units.mk0
            (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
              1)
            sorry) :
        ValueGroup₀ valuation)} ⊆
  U
Tactic: use Units.mk0 (valuation.restrict 1) (by simp)
-- 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 : Subsingleton (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ
x : K
hx :
  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 <
        (↑(Units.mk0
              (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
                  (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
                1)
              ⋯) :
          ValueGroup₀ valuation)}
    x
⊢ x ∈ U
have hx₁ : 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 :
    ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
  (1 : ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
Tactic: simp only [Units.val_mk0, mem_setOf_eq, map_one] at hx
Cleared hypotheses: hx
-- 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 : Subsingleton (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ
x : K
hx :
  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 :
      ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
    (1 : ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
⊢ x ∈ U
have pos : ∀ (hx0 : x = 0), x ∈ U
Tactic: by_cases hx0 : x = 0
-- 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 : Subsingleton (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ
x : K
hx :
  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 :
      ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
    (1 : ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
pos : ∀ (hx0 : x = 0), x ∈ U
⊢ x ∈ U
have neg : ∀ (hx0 : ¬x = 0), x ∈ U
Tactic: by_cases hx0 : x = 0
-- 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 : Subsingleton (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ
x : K
hx :
  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 :
      ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
    (1 : ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
hx0 : ¬x = 0
⊢ x ∈ U
have neg : False
Tactic: exfalso
-- 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 : Subsingleton (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ
x : K
hx :
  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 :
      ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
    (1 : ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
hx0 : ¬x = 0
⊢ False
have hx0₁ : IsUnit (M := 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 :
    ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
Tactic: rw [← (valuation (K := K)).restrict.zero_iff, ← ne_eq, ← isUnit_iff_ne_zero] at hx0
Cleared hypotheses: hx0
-- 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 : Subsingleton (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ
x : K
hx :
  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 :
      ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
    (1 : ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
hx0 :
  IsUnit (M := 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 :
      ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
⊢ LE.le (α := ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
    (1 : 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 :
      ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
have neg : Eq (α := ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
  (1 : 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 :
    ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
Tactic: apply le_of_eq
-- 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 : Subsingleton (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ
x : K
hx :
  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 :
      ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
    (1 : ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
hx0 :
  IsUnit (M := 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 :
      ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
⊢ Eq (α := ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
    (1 : 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 :
      ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
have neg : Eq (α := 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 :
    ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
  (1 : ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))
Tactic: rw [eq_comm]
-- 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) <
            γ
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    {x : K |
        ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x <
          (↑γ : ValueGroup₀ valuation)} ⊆
      U
have refine_1 : ∀ (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) ε sorry),
  ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    {x : K |
        ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x <
          (↑γ : ValueGroup₀ valuation)} ⊆
      U
Tactic: obtain ⟨x, hx, hxy⟩ := H (γ := ⟨ε, le_of_lt hε⟩) (pos_iff_ne_zero.mp 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) ε ⋯
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation K ℝ≥0) valuation)ˣ),
    {x : K |
        ((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
              (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
            x <
          (↑γ : ValueGroup₀ valuation)} ⊆
      U
have h₁ : {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)
              sorry) :
          ValueGroup₀ (F := Valuation K ℝ≥0) valuation) :
        ValueGroup₀ (F := Valuation K ℝ≥0) valuation)} ⊆
  U
Tactic: use Units.mk0 (valuation.restrict x) (by simp [Valuation.restrict_def, hx])