awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
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
this : Nontrivial.{u_2} Γ₀ˣ
u : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hu :
  (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑u : ValueGroup₀ v)) :
      ℝ) <
    r
x : L × L
hx :
  Membership.mem (γ := Set (L × L))
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑u : ValueGroup₀ v)} x
rw :
  LT.lt (α := ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
        ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x.2 - x.1)) :
      ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑u : ValueGroup₀ v) :
      ℝ≥0)
⊢ (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x.1 - x.2))) :
      ℝ) <
    (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          (↑u : ValueGroup₀ v)) :
      ℝ)

Tactic:
rw [NNReal.coe_lt_coe, ← neg_sub, Valuation.map_neg]

Premises used: neg_sub, Valuation.map_neg, NNReal.coe_lt_coe
-- 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_1 : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
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
this : Nontrivial.{u_2} Γ₀ˣ
u : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hu :
  (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑u : ValueGroup₀ v)) :
      ℝ) <
    r
x : L × L
hx :
  Membership.mem (γ := Set (L × L))
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑u : ValueGroup₀ v)} x
⊢ LT.lt (α := ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
        ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x.2 - x.1)) :
      ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑u : ValueGroup₀ v) :
      ℝ≥0)

Tactic:
(RankOne.strictMono Valued.v).lt_iff_lt.mpr hx

Premises used: Iff.mpr, StrictMono.lt_iff_lt
-- 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_1 : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
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
this : Nontrivial.{u_2} Γ₀ˣ
u : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hu :
  (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑u : ValueGroup₀ v)) :
      ℝ) <
    r
x : L × L
hx :
  Membership.mem (γ := Set (L × L))
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑u : ValueGroup₀ v)} x
⊢ LT.lt (α := ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
        ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x.2 - x.1)) :
      ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑u : ValueGroup₀ v) :
      ℝ≥0)

Tactic:
exact (RankOne.strictMono Valued.v).lt_iff_lt.mpr hx

Premises used: Iff.mpr, StrictMono.lt_iff_lt
-- 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 }
U : Set (L × L)
x y : { ε : ℝ // ε > 0 }
h :
  GE.ge.{u_1} (α := Filter (L × L)) (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑x : ℝ)})
      (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑(min x y) : ℝ)}) ∧
    GE.ge.{u_1} (α := Filter (L × L)) (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑y : ℝ)})
      (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑(min x y) : ℝ)})
⊢ ∃ (z : { ε : ℝ // ε > 0 }),
    GE.ge.{u_1} (α := Filter (L × L)) (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑x : ℝ)})
        (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑z : ℝ)}) ∧
      GE.ge.{u_1} (α := Filter (L × L)) (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑y : ℝ)})
        (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑z : ℝ)})

Tactic:
use min x y

Premises used: Min.min
-- 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 }
U : Set (L × L)
x y : { ε : ℝ // ε > 0 }
h :
  (∀ (a b : L), Valuation.norm v (a - b) < (↑(min x y) : ℝ) → Valuation.norm v (a - b) < (↑x : ℝ)) ∧
    ∀ (a b : L), Valuation.norm v (a - b) < (↑(min x y) : ℝ) → Valuation.norm v (a - b) < (↑y : ℝ)
⊢ GE.ge.{u_1} (α := Filter (L × L)) (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑x : ℝ)})
      (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑(min x y) : ℝ)}) ∧
    GE.ge.{u_1} (α := Filter (L × L)) (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑y : ℝ)})
      (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑(min x y) : ℝ)})

Tactic:
simp only [le_principal_iff, mem_principal, setOf_subset_setOf, Prod.forall]

Premises used: Filter.le_principal_iff, Filter.mem_principal, Set.setOf_subset_setOf, Prod.forall
-- 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 }
U : Set (L × L)
x y : { ε : ℝ // ε > 0 }
⊢ (∀ (a b : L), Valuation.norm v (a - b) < (↑(min x y) : ℝ) → Valuation.norm v (a - b) < (↑x : ℝ)) ∧
    ∀ (a b : L), Valuation.norm v (a - b) < (↑(min x y) : ℝ) → Valuation.norm v (a - b) < (↑y : ℝ)

Tactic:
⟨fun a b hab => lt_of_lt_of_le hab (min_le_left _ _), fun a b hab =>
            lt_of_lt_of_le hab (min_le_right _ _)⟩

Premises used: min_le_left, And.intro, min_le_right, Subtype.val, lt_of_lt_of_le
-- 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 }
U : Set (L × L)
x y : { ε : ℝ // ε > 0 }
⊢ (∀ (a b : L), Valuation.norm v (a - b) < (↑(min x y) : ℝ) → Valuation.norm v (a - b) < (↑x : ℝ)) ∧
    ∀ (a b : L), Valuation.norm v (a - b) < (↑(min x y) : ℝ) → Valuation.norm v (a - b) < (↑y : ℝ)

Tactic:
exact ⟨fun a b hab => lt_of_lt_of_le hab (min_le_left _ _), fun a b hab =>
            lt_of_lt_of_le hab (min_le_right _ _)⟩
-- 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 →*₀ Γ₀)) (-(x - y)))) :
      ℝ) =
    (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (-x + y))) :
      ℝ)
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 →*₀ Γ₀)) (-x + y))) :
      ℝ)
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 →*₀ Γ₀)) (-x + y))) :
      ℝ)
rw₃ rw₄ :
  (↑(((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 →*₀ Γ₀)) (-x + y))) :
      ℝ)
⊢ (↑(((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 →*₀ Γ₀)) (-x + y))) :
      ℝ)

Tactic:
rw [← v.restrict.map_neg, neg_sub, sub_eq_add_neg, add_comm]

Premises used: neg_sub, Valued.v, sub_eq_add_neg, add_comm, Valuation.map_neg, Valuation.restrict
-- 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
⊢ Valuation.norm v (x * y) = Valuation.norm v x * Valuation.norm v y

Tactic:
simp only [Valuation.norm, ← NNReal.coe_mul, map_mul]

Premises used: Valuation.norm, map_mul, NNReal.coe_mul
-- 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
⊢ IsNonarchimedean (R := ℝ) fun (x : L) ↦ ‖x‖

Tactic:
Valuation.norm_add_le _

Premises used: Valuation.norm_add_le, IsNonarchimedean
-- 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
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
(Valuation.norm_add_le _ (x - y) (y - z)).trans_eq' ?_

Premises used: Valuation.norm_add_le, HSub.hSub, LE.le.trans_eq'
-- 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
refine : Valuation.norm v (x - y + (y - z)) = dist x z
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
refine (Valuation.norm_add_le _ (x - y) (y - z)).trans_eq' ?_

Premises used: Valuation.norm_add_le, HSub.hSub, LE.le.trans_eq'
-- 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 - z) = dist x z
⊢ Valuation.norm v (x - y + (y - z)) = dist x z

Tactic:
simp only [sub_add_sub_cancel]

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 - z) = dist x z

Tactic:
rfl
-- 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
⊢ Eq.{u_1 + 1} (α := (a : L) → ℝ≥0) (⇑NormedField.valuation : (a : L) → ℝ≥0)
    (Function.comp (β := ValueGroup₀ (F := Valuation L Γ₀) v) (⇑(RankOne.hom v) : (a : ValueGroup₀ v) → ℝ≥0)
      (⇑(Valuation.restrict v) : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)))

Tactic:
rfl

Premises used: NNReal.mk, NNReal, Valuation.norm, NNReal.toReal, rfl
-- 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
⊢ ‖x‖ =
    (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x)) :
      ℝ)

Tactic:
rfl

Premises used: Set.Mem, setOf, Valuation.norm, NNReal.toReal, rfl
-- 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 x' : L
rw :
  ‖x‖ ≤ ‖x'‖ ↔
    LE.le (α := ℝ≥0)
      (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x) :
        ℝ≥0)
      (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x') :
        ℝ≥0)
⊢ ‖x‖ ≤ ‖x'‖ ↔ LE.le.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) ((v : (a : L) → Γ₀) x' : Γ₀)

Tactic:
rw [← v.restrict_le_iff, ← (Valuation.RankOne.strictMono val.v).le_iff_le]

Premises used: Valuation.restrict_le_iff, Valued.v, Valuation.RankOne.strictMono, StrictMono.le_iff_le
-- 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 x' : L
⊢ ‖x‖ ≤ ‖x'‖ ↔
    LE.le (α := ℝ≥0)
      (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x) :
        ℝ≥0)
      (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x') :
        ℝ≥0)

Tactic:
rfl
-- 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 x' : L
rw :
  ‖x‖ < ‖x'‖ ↔
    LT.lt (α := ℝ≥0)
      (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x) :
        ℝ≥0)
      (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x') :
        ℝ≥0)
⊢ ‖x‖ < ‖x'‖ ↔ LT.lt.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) ((v : (a : L) → Γ₀) x' : Γ₀)

Tactic:
rw [← v.restrict_lt_iff, ← (Valuation.RankOne.strictMono val.v).lt_iff_lt]

Premises used: Valued.v, StrictMono.lt_iff_lt, Valuation.RankOne.strictMono, Valuation.restrict_lt_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 x' : L
⊢ ‖x‖ < ‖x'‖ ↔
    LT.lt (α := ℝ≥0)
      (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x) :
        ℝ≥0)
      (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
          ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x') :
        ℝ≥0)

Tactic:
rfl
-- 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
rw :
  ‖x‖ ≤ 1 ↔
    LE.le.{u_2} (α := ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) 1 : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
⊢ ‖x‖ ≤ 1 ↔ LE.le.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [← map_one val.v, ← v.restrict_le_iff]

Premises used: Valuation.restrict_le_iff, Valued.v, map_one
-- 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
⊢ ‖x‖ ≤ 1 ↔
    LE.le.{u_2} (α := ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) 1 : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))

Tactic:
simpa only [map_one] using (Valuation.RankOne.strictMono val.v).le_iff_le (b := 1)

Premises used: Valued.v, Valuation.RankOne.strictMono, map_one, StrictMono.le_iff_le
-- 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
rw :
  ‖x‖ < 1 ↔
    LT.lt.{u_2} (α := ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) 1 : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
⊢ ‖x‖ < 1 ↔ LT.lt.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [← map_one val.v, ← v.restrict_lt_iff]

Premises used: Valued.v, map_one, Valuation.restrict_lt_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
⊢ ‖x‖ < 1 ↔
    LT.lt.{u_2} (α := ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) 1 : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))

Tactic:
simpa only [map_one] using (Valuation.RankOne.strictMono val.v).lt_iff_lt (b := 1)

Premises used: Valued.v, StrictMono.lt_iff_lt, Valuation.RankOne.strictMono, map_one
-- 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
rw :
  1 ≤ ‖x‖ ↔
    LE.le.{u_2} (α := ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) 1 : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
⊢ 1 ≤ ‖x‖ ↔ LE.le.{u_2} (α := Γ₀) (1 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀)

Tactic:
rw [← map_one val.v, ← v.restrict_le_iff]

Premises used: Valuation.restrict_le_iff, Valued.v, map_one
-- 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
⊢ 1 ≤ ‖x‖ ↔
    LE.le.{u_2} (α := ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) 1 : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))

Tactic:
simpa only [map_one] using (Valuation.RankOne.strictMono val.v).le_iff_le (a := 1)

Premises used: Valued.v, Valuation.RankOne.strictMono, map_one, StrictMono.le_iff_le
-- 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
rw :
  1 < ‖x‖ ↔
    LT.lt.{u_2} (α := ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) 1 : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
⊢ 1 < ‖x‖ ↔ LT.lt.{u_2} (α := Γ₀) (1 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀)

Tactic:
rw [← map_one val.v, ← v.restrict_lt_iff]

Premises used: Valued.v, map_one, Valuation.restrict_lt_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
⊢ 1 < ‖x‖ ↔
    LT.lt.{u_2} (α := ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) 1 : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
      ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))

Tactic:
simpa only [map_one] using (Valuation.RankOne.strictMono val.v).lt_iff_lt (a := 1)

Premises used: Valued.v, StrictMono.lt_iff_lt, Valuation.RankOne.strictMono, map_one
-- 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
h :
  ∀ (x : L),
    Membership.mem (γ := Set L) {x : L | Membership.mem (γ := Subring L) (integer v) x} x ↔
      Membership.mem (γ := Set L) (Metric.closedBall 0 1) x
⊢ Eq.{u_1 + 1} (α := Set L) {x : L | Membership.mem (γ := Subring L) (integer v) x} (Metric.closedBall 0 1)

Tactic:
ext x
-- 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
⊢ Membership.mem (γ := Set L) {x : L | Membership.mem (γ := Subring L) (integer v) x} x ↔
    Membership.mem (γ := Set L) (Metric.closedBall 0 1) x

Tactic:
simp [mem_integer_iff]

Premises used: Valuation.mem_integer_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
obtain :
  ∀ (x : L)
    (hx :
      Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
        Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)),
    ∃ (x : L), 1 < ‖x‖
⊢ ∃ (x : L), 1 < ‖x‖

Tactic:
obtain ⟨x, hx⟩ := Valuation.RankOne.nontrivial val.v

Premises used: Valued.v, Valuation.RankOne.nontrivial
-- 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
hx :
  Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)
inl : ∀ (h : LE.le.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)), ∃ (x : L), 1 < ‖x‖
inr : ∀ (h : LE.le.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)), ∃ (x : L), 1 < ‖x‖
⊢ ∃ (x : L), 1 < ‖x‖

Tactic:
rcases Valuation.val_le_one_or_val_inv_le_one val.v x with h | h

Premises used: Valuation.val_le_one_or_val_inv_le_one, Valued.v
-- 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
hx :
  Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)
h : LE.le.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)
h₁ : 1 < ‖x⁻¹‖
⊢ ∃ (x : L), 1 < ‖x‖

Tactic:
use x⁻¹