awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ε ⋯
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)
                ⋯) :
            ValueGroup₀ (F := Valuation K ℝ≥0) valuation) :
          ValueGroup₀ (F := Valuation K ℝ≥0) 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 x) (by simp [Valuation.restrict_def, hx])

Premises used: Units.mk0, NormedField.valuation, 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 :
  ∀ {γ : ℝ≥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
h₁ : Membership.mem (γ := Set K) (Metric.ball 0 ε) y
⊢ y ∈ U

Tactic:
apply 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 :
  ∀ {γ : ℝ≥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
h₁ : ‖y‖ < ε
⊢ Membership.mem (γ := Set K) (Metric.ball 0 ε) y

Tactic:
simp only [Metric.mem_ball, dist_zero_right]

Premises used: Metric.mem_ball, dist_zero_right
-- 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) ε ⋯
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
⊢ (↑(((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

Premises used: Set.mem_setOf_eq, NNReal.coe_lt_coe, Valuation.restrict_lt_iff, 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 :
  ∀ {γ : ℝ≥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) : ℝ)
h₁ : (↑(((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) x) : ℝ) < ε
⊢ ‖y‖ < ε

Tactic:
apply lt_trans hy

Premises used: lt_trans
-- 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) ε ⋯
y : K
hy :
  (↑(((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) y) : ℝ) <
    (↑(((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) x) : ℝ)
⊢ (↑(((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) x) : ℝ) < ε

Tactic:
simpa [RankLeOne.hom', valuation.restrict_def] using hxy

Premises used: Valuation.restrict_def, NormedField.valuation, Valuation.RankLeOne.hom'
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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

Tactic:
⟨(embedding ε.1 : ℝ≥0), ?_, fun x hx ↦ hε ?_⟩

Premises used: Units.val, And.intro, MonoidWithZeroHom.ValueGroup₀.embedding, Exists.intro, DFunLike.coe, NNReal.toReal
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
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
⊢ ∃ ε > 0, Metric.ball 0 ε ⊆ U

Tactic:
refine ⟨(embedding ε.1 : ℝ≥0), ?_, fun x hx ↦ hε ?_⟩
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
⊢ (↑((embedding : (a : ValueGroup₀ valuation) → ℝ≥0) (↑ε : ValueGroup₀ valuation)) : ℝ) > 0

Tactic:
NNReal.coe_pos.mpr <| embedding_strictMono.lt_iff_lt.mpr ε.zero_lt

Premises used: Iff.mpr, NNReal.coe_pos
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
⊢ (↑((embedding : (a : ValueGroup₀ valuation) → ℝ≥0) (↑ε : ValueGroup₀ valuation)) : ℝ) > 0

Tactic:
exact NNReal.coe_pos.mpr <| embedding_strictMono.lt_iff_lt.mpr ε.zero_lt

Premises used: Iff.mpr, StrictMono.lt_iff_lt, NNReal.coe_pos, Units.zero_lt
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
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:
simpa [restrict_lt_iff_lt_embedding] using (mem_ball_zero_iff.mp hx)

Premises used: Valuation.restrict_lt_iff_lt_embedding, Iff.mp, mem_ball_zero_iff
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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‖
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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‖
⊢ x ≠ 0

Tactic:
have h' : x ≠ 0 := norm_eq_zero.not.mp (h.gt.trans' (by simp)).ne'
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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‖
h' : x ≠ 0
⊢ 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)

Tactic:
simp [valuation_apply, ← NNReal.coe_inj, h.ne', h']

Premises used: LT.lt.ne', NormedField.valuation_apply, NNReal.coe_inj
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
⊢ v.norm x =
    (↑((RankOne.hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x)) : ℝ)

Tactic:
rfl

Premises used: Valuation.norm, rfl
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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

Tactic:
simp only [norm, NNReal.zero_le_coe]

Premises used: Valuation.norm, NNReal.zero_le_coe
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x y : L
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 →*₀ Γ₀))
⊢ v.norm (x + y) ≤ max (v.norm x) (v.norm y)

Tactic:
simp only [norm, NNReal.coe_le_coe, le_max_iff, StrictMono.le_iff_le hv.strictMono]

Premises used: Valuation.RankOne.strictMono, Valuation.norm, le_max_iff, StrictMono.le_iff_le, NNReal.coe_le_coe
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x y : 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 →*₀ Γ₀)) 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:
le_max_iff.mp (Valuation.map_add_le_max' v.restrict _ _)

Premises used: Valuation.map_add_le_max', Iff.mp, le_max_iff, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x y : 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 →*₀ Γ₀)) 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:
exact le_max_iff.mp (Valuation.map_add_le_max' v.restrict _ _)

Premises used: Valuation.map_add_le_max', Iff.mp, le_max_iff, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
hx : v.norm x = 0
⊢ x = 0

Tactic:
simpa [v.restrict_def, norm, NNReal.coe_eq_zero, RankOne.hom_eq_zero_iff, zero_iff] using hx

Premises used: NNReal.coe_eq_zero, Valuation.zero_iff, Valuation.norm, Valuation.restrict_def, Valuation.RankOne.hom_eq_zero_iff
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
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 : Γ₀)
⊢ 0 < v.norm x ↔ 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)]

Premises used: Valuation.RankOne.hom, StrictMono.lt_iff_lt, NNReal.coe_zero, map_zero, Valuation.RankOne.strictMono, NNReal.coe_lt_coe, Valuation.norm_def
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
rw rw₁ :
  LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀)
⊢ 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 [v.restrict_pos_iff]

Premises used: Valuation.restrict_pos_iff
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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 : L
⊢ Valuation.norm v (x - x) = 0

Tactic:
simp only [sub_self, Valuation.norm, Valuation.map_zero, hv.hom.map_zero, NNReal.coe_zero]

Premises used: Valuation.RankOne.hom, sub_self, NNReal.coe_zero, MonoidWithZeroHom.map_zero, Valuation.norm, Valuation.map_zero
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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))) :
      ℝ)
rw₁ 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))) :
      ℝ)

Tactic:
rw [← neg_sub, Valuation.map_neg]

Premises used: neg_sub, Valuation.map_neg
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
simp : Valuation.norm v (x - y + (y - z)) ≤ Valuation.norm v (x - y) + Valuation.norm v (y - z)
⊢ Valuation.norm v (x - z) ≤ Valuation.norm v (x - y) + Valuation.norm v (y - z)

Tactic:
simp only [← sub_add_sub_cancel x y z]

Premises used: sub_add_sub_cancel
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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 - y + (y - z)) ≤ Valuation.norm v (x - y) + Valuation.norm v (y - z)

Tactic:
le_trans (val.v.norm_add_le _ _)
        (max_le_add_of_nonneg (val.v.norm_nonneg _) (val.v.norm_nonneg _))

Premises used: Valuation.norm_add_le, Valued.v, Valuation.norm_nonneg, max_le_add_of_nonneg, le_trans
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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 - y + (y - z)) ≤ Valuation.norm v (x - y) + Valuation.norm v (y - z)

Tactic:
exact le_trans (val.v.norm_add_le _ _)
        (max_le_add_of_nonneg (val.v.norm_nonneg _) (val.v.norm_nonneg _))

Premises used: Valuation.norm_add_le, Valued.v, Valuation.norm_nonneg, max_le_add_of_nonneg, le_trans
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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
⊢ Nonempty { ε : ℝ // ε > 0 }

Tactic:
haveI : Nonempty { ε : ℝ // ε > 0 } := nonempty_Ioi_subtype
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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 }
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
⊢ uniformity L = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < ε}

Tactic:
ext U