awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
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
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 →*₀ Γ₀))}
⊢ IsClosed[_t] (↑v.integer : Set 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]

Premises used: Subring.coe_set_mk, Subsemigroup.coe_set_mk, Valuation.restrict_le_one_iff, Subsemiring.coe_set_mk, Valuation.integer, Submonoid.coe_set_mk
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
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 |
      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:
isClosed_closedBall _

Premises used: Valuation.isClosed_closedBall
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
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 |
      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:
exact isClosed_closedBall _

Premises used: Valuation.isClosed_closedBall
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
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
⊢ IsClopen (↑v.integer : Set R)

Tactic:
⟨isClosed_integer, isOpen_integer⟩

Premises used: Valuation.isOpen_integer, And.intro, Valuation.isClosed_integer, IsClopen
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace K
inst_4 : IsValuativeTopology K
v : Valuation K Γ₀
inst_5 : v.Compatible
⊢ IsOpen[inst_3] (↑v.valuationSubring : Set K)

Tactic:
isOpen_integer

Premises used: Valuation.isOpen_integer, setOf
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace K
inst_4 : IsValuativeTopology K
v : Valuation K Γ₀
inst_5 : v.Compatible
⊢ IsClosed[inst_3] (↑v.valuationSubring : Set K)

Tactic:
isClosed_integer

Premises used: setOf, Valuation.isClosed_integer
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace K
inst_4 : IsValuativeTopology K
v : Valuation K Γ₀
inst_5 : v.Compatible
⊢ IsClopen (↑v.valuationSubring : Set K)

Tactic:
isClopen_integer

Premises used: setOf, Valuation.isClopen_integer
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
Goal:
K : Type u_1
hK : NormedField K
inst : IsUltrametricDist K
x : K
⊢ ((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) x = ‖x‖₊

Tactic:
rfl

Premises used: NNReal.mk, rfl
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
Goal:
K : Type u_1
hK : NormedField K
inst : IsUltrametricDist K
U : Set K
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
⊢ 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

Tactic:
rw [Metric.mem_nhds_iff]

Premises used: Metric.mem_nhds_iff
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
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
⊢ (∃ ε > 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 ⟨?_, ?_⟩
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
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
⊢ ∃ (γ : (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

Premises used: NormedField.valuation, Valuation.RankLeOne.exists_val_lt
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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)ˣ
⊢ Ne (α := ValueGroup₀ (F := Valuation K ℝ≥0) valuation)
    (((Valuation.restrict valuation : Valuation K (ValueGroup₀ (F := K →*₀ ℝ≥0) (↑valuation : K →*₀ ℝ≥0))) :
        (a : K) → ValueGroup₀ (↑valuation : K →*₀ ℝ≥0))
      1)
    0

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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)ˣ
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)
              ⋯) :
          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

Tactic:
use Units.mk0 (valuation.restrict 1) (by simp)

Premises used: Units.mk0, NormedField.valuation, OfNat.ofNat, DFunLike.coe, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
⊢ 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

Premises used: Set.mem_setOf_eq, map_one, Units.val_mk0
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
neg : ∀ (hx0 : ¬x = 0), x ∈ U
⊢ x ∈ U

Tactic:
by_cases hx0 : x = 0
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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

Tactic:
h (hx0 ▸ Metric.mem_ball_self hε)

Premises used: Eq.rec, Metric.mem_ball_self
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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

Tactic:
exact h (hx0 ▸ Metric.mem_ball_self hε)
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
neg : False
⊢ x ∈ U

Tactic:
exfalso
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
⊢ 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

Premises used: Valuation.zero_iff, isUnit_iff_ne_zero, ne_eq, NormedField.valuation, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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))
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))
⊢ 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))

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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))
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))
⊢ 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:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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))
    (((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:
simpa only [Units.ext_iff, hx0.unit_spec, Units.val_one,
              Submonoid.mk_eq_one] using H.elim hx0.unit 1

Premises used: Units.ext_iff, Submonoid.mk_eq_one, Units.val_one, IsUnit.unit, Subsingleton.elim, OfNat.ofNat, IsUnit.unit_spec
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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) <
            γ
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) ε ⋯),
    ∃ (γ : (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

Tactic:
obtain ⟨x, hx, hxy⟩ := H (γ := ⟨ε, le_of_lt hε⟩) (pos_iff_ne_zero.mp hε)

Premises used: Iff.mp, pos_iff_ne_zero
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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) ε ⋯
⊢ Ne (α := ValueGroup₀ (F := Valuation K ℝ≥0) valuation)
    (((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))
    (0 : ValueGroup₀ (F := Valuation K ℝ≥0) valuation)

Tactic:
simp [Valuation.restrict_def, hx]

Premises used: Valuation.restrict_def