awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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 < δ
⊢ {p : L × L | Valuation.norm v (p.1 - p.2) < (↑δ : ℝ)} ⊆ U
have 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)}
Tactic: apply subset_trans _ hε
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (hypothesis)
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
⊢ Membership.mem (γ := Set (L × L))
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} x
have 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)
Tactic: simp only [mem_setOf_eq, Valuation.norm, hδ, NNReal.coe_lt_coe] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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)
⊢ Membership.mem (γ := Set (L × L))
    {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑ε : ValueGroup₀ v)} x
have rw : (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (x.1 - x.2) < (↑ε : ValueGroup₀ v)
Tactic: rw [mem_setOf, ← neg_sub, Valuation.map_neg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (hypothesis)
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
⊢ ∃ (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
have this₁ : Nontrivial.{u_2} Γ₀ˣ
Tactic: haveI : Nontrivial Γ₀ˣ := (nontrivial_iff_exists_ne (1 : Γ₀ˣ)).mpr
            ⟨RankOne.unit val.v, RankOne.unit_ne_one val.v⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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} Γ₀ˣ
⊢ ∃ (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
have 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
Tactic: obtain ⟨u, hu⟩ := Real.exists_lt_of_strictMono hv.strictMono hr_pos
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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
⊢ ∃ (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
have h : {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑u : ValueGroup₀ v)} ⊆ U
Tactic: use u
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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
⊢ {p : L × L | (Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) (p.2 - p.1) < (↑u : ValueGroup₀ v)} ⊆ U
have 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}
Tactic: apply subset_trans _ hr
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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
⊢ (↑(((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
have 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)) :
    ℝ)
Tactic: apply lt_trans _ hu
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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
⊢ (↑(((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)) :
      ℝ)
have 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)
Tactic: rw [NNReal.coe_lt_coe, ← neg_sub, Valuation.map_neg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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 }
⊢ ∃ (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 : ℝ)})
have 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) : ℝ)})
Tactic: use min x y
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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 }
⊢ 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) : ℝ)})
have 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 : ℝ)
Tactic: simp only [le_principal_iff, mem_principal, setOf_subset_setOf, Prod.forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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
⊢ (↑(((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))) :
      ℝ)
have 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))) :
    ℝ)
Tactic: rw [← v.restrict.map_neg, neg_sub, sub_eq_add_neg, add_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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))) :
      ℝ)
⊢ (↑(((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))) :
      ℝ)
have 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))) :
    ℝ)
Tactic: rw [← v.restrict.map_neg, neg_sub, sub_eq_add_neg, add_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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))) :
      ℝ)
⊢ (↑(((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))) :
      ℝ)
have 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))) :
    ℝ)
Tactic: rw [← v.restrict.map_neg, neg_sub, sub_eq_add_neg, add_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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))) :
      ℝ)
⊢ (↑(((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))) :
      ℝ)
have 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))) :
    ℝ)
Tactic: rw [← v.restrict.map_neg, neg_sub, sub_eq_add_neg, add_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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)
have refine : Valuation.norm v (x - y + (y - z)) = dist x z
Tactic: refine (Valuation.norm_add_le _ (x - y) (y - z)).trans_eq' ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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)) = dist x z
have simp : Valuation.norm v (x - z) = dist x z
Tactic: simp only [sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) ((v : (a : L) → Γ₀) x' : Γ₀)
have 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)
Tactic: rw [← v.restrict_le_iff, ← (Valuation.RankOne.strictMono val.v).le_iff_le]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) ((v : (a : L) → Γ₀) x' : Γ₀)
have 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)
Tactic: rw [← v.restrict_lt_iff, ← (Valuation.RankOne.strictMono val.v).lt_iff_lt]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)
have 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 →*₀ Γ₀))
Tactic: rw [← map_one val.v, ← v.restrict_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)
have 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 →*₀ Γ₀))
Tactic: rw [← map_one val.v, ← v.restrict_lt_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
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} (α := Γ₀) (1 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀)
have 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 →*₀ Γ₀))
Tactic: rw [← map_one val.v, ← v.restrict_le_iff]