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 : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      True ∧
        {p : L × L |
            (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
          U) ↔
    ∃ (i : { ε : ℝ // ε > 0 }),
      Membership.mem (γ := Filter (L × L)) (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑i : ℝ)}) U
h₁ :
  Directed (fun (x1 x2 : Filter (L × L)) ↦ x1 ≥ x2) fun (x : { ε : ℝ // ε > 0 }) ↦
    𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑x : ℝ)}
⊢ U ∈ uniformity L ↔
    Membership.mem (γ := Filter (L × L)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < ε}) U

Tactic:
rw [hasBasis_iff.mp (Valued.hasBasis_uniformity L Γ₀), iInf_subtype', mem_iInf_of_directed]

Premises used: iInf_subtype', Filter.hasBasis_iff, Iff.mp, Valued.hasBasis_uniformity, Filter.mem_iInf_of_directed
-- 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)
h :
  (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
        U) ↔
    ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U
⊢ (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      True ∧
        {p : L × L |
            (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
          U) ↔
    ∃ (i : { ε : ℝ // ε > 0 }),
      Membership.mem (γ := Filter (L × L)) (𝓟 {p : L × L | Valuation.norm v (p.1 - p.2) < (↑i : ℝ)}) U

Tactic:
simp only [true_and, mem_principal, Subtype.exists, gt_iff_lt, exists_prop]

Premises used: Subtype.exists, exists_prop, Filter.mem_principal, gt_iff_lt, true_and
-- 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)
⊢ (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
        U) ↔
    ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U

Tactic:
⟨fun ⟨ε, hε⟩ => ?_, fun ⟨r, hr_pos, hr⟩ => ?_⟩

Premises used: Units.val, Valued.v, setOf, HSub.hSub, Exists, HasSubset.Subset, Valuation.norm, Prod.fst, _private.0.Valued.toNormedField.match_8, And, LT.lt, Iff.intro, OfNat.ofNat, Prod.snd, DFunLike.coe, _private.0.Valued.toNormedField.match_7, 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
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
        U) →
    ∀ (ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ)
      (hε :
        {p : L × L |
            (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆
          U),
      ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U
h₁ :
  (∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U) →
    ∀ (r : ℝ) (hr_pos : 0 < r) (hr : {p : L × L | Valuation.norm v (p.1 - p.2) < r} ⊆ U),
      ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
        {p : L × L |
            (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
          U
⊢ (∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
        U) ↔
    ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U

Tactic:
refine ⟨fun ⟨ε, hε⟩ => ?_, fun ⟨r, hr_pos, hr⟩ => ?_⟩
-- 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)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
⊢ let δ : ℝ≥0 :=
    ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v);
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)

Tactic:
set δ : ℝ≥0 := hv.hom _ ε with hδ

Premises used: Units.val, Valuation.RankOne.hom, DFunLike.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 : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
rw :
  LT.lt (α := ℝ≥0) (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) 0 : ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v) :
      ℝ≥0)
⊢ 0 < δ

Tactic:
rw [hδ, ← map_zero hv.hom]

Premises used: Valuation.RankOne.hom, 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
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
⊢ LT.lt (α := ℝ≥0) (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) 0 : ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v) :
      ℝ≥0)

Tactic:
hv.strictMono _ (Units.zero_lt ε)

Premises used: Valuation.RankOne.strictMono, Units.zero_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)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
⊢ LT.lt (α := ℝ≥0) (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) 0 : ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v) :
      ℝ≥0)

Tactic:
exact hv.strictMono _ (Units.zero_lt ε)

Premises used: Valuation.RankOne.strictMono, Units.zero_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)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
⊢ 0 < δ

Tactic:
have hδ_pos : 0 < δ := by
            rw [hδ, ← map_zero hv.hom]
            exact hv.strictMono _ (Units.zero_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)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ_pos : 0 < δ
right : {p : L × L | Valuation.norm v (p.1 - p.2) < (↑δ : ℝ)} ⊆ U
⊢ ∃ (a : ℝ), 0 < a ∧ {p : L × L | Valuation.norm v (p.1 - p.2) < a} ⊆ U

Tactic:
use δ, hδ_pos
-- 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)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ_pos : 0 < δ
apply :
  Subset.{u_1} (α := Set (L × L)) {p : L × L | Valuation.norm v (p.1 - p.2) < (↑δ : ℝ)}
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)}
⊢ {p : L × L | Valuation.norm v (p.1 - p.2) < (↑δ : ℝ)} ⊆ U

Tactic:
apply subset_trans _ hε

Premises used: subset_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
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ_pos : 0 < δ
x : L × L
hx : Membership.mem (γ := Set (L × L)) {p : L × L | Valuation.norm v (p.1 - p.2) < (↑δ : ℝ)} 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.1 - x.2)) :
      ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v) :
      ℝ≥0)

Tactic:
simp only [mem_setOf_eq, Valuation.norm, hδ, NNReal.coe_lt_coe] at hx

Premises used: Set.mem_setOf_eq, Valuation.norm, 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 : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ_pos : 0 < δ
x : L × L
hx :
  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.1 - x.2)) :
      ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v) :
      ℝ≥0)
rw : (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x.1 - x.2) < (↑ε : ValueGroup₀ v)
⊢ Membership.mem (γ := Set (L × L))
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} x

Tactic:
rw [mem_setOf, ← neg_sub, Valuation.map_neg]

Premises used: neg_sub, Set.mem_setOf, 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
this : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ_pos : 0 < δ
x : L × L
hx :
  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.1 - x.2)) :
      ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v) :
      ℝ≥0)
⊢ (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x.1 - x.2) < (↑ε : ValueGroup₀ v)

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

Premises used: StrictMono.lt_iff_lt, Iff.mp
-- 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)
h :
  ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U
ε : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ
hε : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} ⊆ U
δ : ℝ≥0 :=
  ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ :
  δ = ((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v)
hδ_pos : 0 < δ
x : L × L
hx :
  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.1 - x.2)) :
      ℝ≥0)
    (((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0) (↑ε : ValueGroup₀ v) :
      ℝ≥0)
⊢ (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x.1 - x.2) < (↑ε : ValueGroup₀ v)

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

Premises used: StrictMono.lt_iff_lt, Iff.mp
-- 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)
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
⊢ Nontrivial.{u_2} Γ₀ˣ

Tactic:
haveI : Nontrivial Γ₀ˣ := (nontrivial_iff_exists_ne (1 : Γ₀ˣ)).mpr
            ⟨RankOne.unit val.v, RankOne.unit_ne_one val.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
this_1 : Nonempty { ε : ℝ // ε > 0 }
U : Set (L × L)
h_1 : ∃ (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} Γ₀ˣ
h :
  ∀ (u : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ)
    (hu :
      (↑(((RankOne.hom v : ValueGroup₀ (F := Valuation L Γ₀) v →*₀ ℝ≥0) : (a : ValueGroup₀ v) → ℝ≥0)
              (↑u : ValueGroup₀ v)) :
          ℝ) <
        r),
    ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
      {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆
        U
⊢ ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U

Tactic:
obtain ⟨u, hu⟩ := Real.exists_lt_of_strictMono hv.strictMono hr_pos

Premises used: Valuation.RankOne.strictMono, Real.exists_lt_of_strictMono
-- 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_1 : ∃ (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
h : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑u : ValueGroup₀ v)} ⊆ U
⊢ ∃ (i : (ValueGroup₀ (F := Valuation L Γ₀) v)ˣ),
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑i : ValueGroup₀ v)} ⊆ U

Tactic:
use u
-- 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
apply :
  Subset.{u_1} (α := Set (L × L))
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑u : ValueGroup₀ v)}
    {p : L × L | Valuation.norm v (p.1 - p.2) < r}
⊢ {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑u : ValueGroup₀ v)} ⊆ U

Tactic:
apply subset_trans _ hr

Premises used: subset_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
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
apply :
  (↑(((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)) :
      ℝ)
⊢ (↑(((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))) :
      ℝ) <
    r

Tactic:
apply lt_trans _ hu

Premises used: lt_trans