awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
g : ValueGroup₀ v
rw :
  (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < g ↔
    ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x < g
⊢ (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < g ↔
    LT.lt (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x :
            ValueGroup₀ v) :
        Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
have rw₁ : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x < g ↔
  ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x < g
Tactic: rw [embedding_strictMono.lt_iff_lt, restrict_def]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
g : ValueGroup₀ v
| LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
have rw : LE.le (α := Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀)
      (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v) :
    Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
Tactic: rw [← ValueGroup₀.embedding_restrict₀ x]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
g : ValueGroup₀ v
⊢ (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ g ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
have conv_rhs : (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ g ↔
  LE.le (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v) :
      Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
Tactic: conv_rhs => rw [← ValueGroup₀.embedding_restrict₀ x]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
g : ValueGroup₀ v
⊢ (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ g ↔
    LE.le (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x :
            ValueGroup₀ v) :
        Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
have rw : (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ g ↔
  ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x ≤ g
Tactic: rw [embedding_strictMono.le_iff_le, restrict_def]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
g : ValueGroup₀ v
rw :
  (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ g ↔
    ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x ≤ g
⊢ (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ g ↔
    LE.le (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x :
            ValueGroup₀ v) :
        Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
have rw₁ : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x ≤ g ↔
  ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x ≤ g
Tactic: rw [embedding_strictMono.le_iff_le, restrict_def]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
⊢ LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have rw : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) 1 : Γ₀) ↔
  LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rw [restrict_lt_iff_lt_embedding, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
rw :
  LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) 1 : Γ₀) ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have rw₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rw [restrict_lt_iff_lt_embedding, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have rw : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) 1 : Γ₀) ↔
  LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rw [restrict_le_iff_le_embedding, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
rw :
  LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) 1 : Γ₀) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have rw₁ : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rw [restrict_le_iff_le_embedding, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
⊢ Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
have rw : Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
    (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
Tactic: rw [restrict_def, restrict₀_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
rw :
  Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
      (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
have rw₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
Tactic: rw [restrict_def, restrict₀_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
⊢ Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have rw : Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
    (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rw [restrict_def, restrict₀_eq_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
rw :
  Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have rw₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rw [restrict_def, restrict₀_eq_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) h) ⋯) :
          WithZero ↥(valueGroup v)))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
          WithZero ↥(valueGroup v))) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have pos : ∀ (hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
  (hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
  LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
Tactic: split_ifs with hx hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
pos :
  ∀ (hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) h) ⋯) :
          WithZero ↥(valueGroup v)))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
          WithZero ↥(valueGroup v))) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have neg : ∀ (hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
  (hy : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
  LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) hy) sorry) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v)) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
Tactic: split_ifs with hx hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
pos :
  ∀ (hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
neg :
  ∀ (hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (hy : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) hy) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) ↔
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) h) ⋯) :
          WithZero ↥(valueGroup v)))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
          WithZero ↥(valueGroup v))) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have pos₁ : ∀ (hx : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) →
    (LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) x) hx) sorry) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        (0 : ValueGroup₀ v) ↔
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
Tactic: split_ifs with hx hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
pos :
  ∀ (hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
neg :
  ∀ (hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (hy : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) hy) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) ↔
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
pos₁ :
  ∀ (hx : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) →
      (LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ₀) x) hx) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v))
          (0 : ValueGroup₀ v) ↔
        LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) h) ⋯) :
          WithZero ↥(valueGroup v)))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
          WithZero ↥(valueGroup v))) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have neg₁ : ∀ (hx : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
  (h : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
  LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) hx) sorry) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) h) sorry) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v)) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
Tactic: split_ifs with hx hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ValueGroup₀ v)ˣ
⊢ ∃ (r : R) (s : R),
    LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ∧
      LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ∧
        HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (β := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) =
          (↑γ : ValueGroup₀ v)
have hu_def : let u := WithZero.unzero sorry;
u = WithZero.unzero sorry
Tactic: set u := WithZero.unzero (Units.ne_zero γ) with hu_def
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ValueGroup₀ v)ˣ
u : ↥(valueGroup v) := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
⊢ ∃ (r : R) (s : R),
    LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ∧
      LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ∧
        HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (β := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) =
          (↑γ : ValueGroup₀ v)
have obtain : ∀ (a : R) (ha : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)) (x : R)
  (hax : HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (v : (a : R) → Γ₀) x),
  ∃ (r : R) (s : R),
    LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ∧
      LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ∧
        HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (β := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) =
          (↑γ : ValueGroup₀ v)
Tactic: obtain ⟨a, ⟨ha, x, hax⟩⟩ := (mem_valueGroup_iff_of_comm _).mp u.2
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ValueGroup₀ v)ˣ
u : ↥(valueGroup v) := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
x : R
hax : HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (v : (a : R) → Γ₀) x
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have rw : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
Tactic: rw [← restrict_pos_iff, restrict_def, WithZero.pos_iff_ne_zero, ne_eq, restrict₀_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ValueGroup₀ v)ˣ
u : ↥(valueGroup v) := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
x : R
hax : HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (v : (a : R) → Γ₀) x
⊢ ∃ (r : R) (s : R),
    LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ∧
      LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ∧
        HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (β := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) =
          (↑γ : ValueGroup₀ v)
have hx : LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: have hx : 0 < v x := by
    rw [← restrict_pos_iff, restrict_def, WithZero.pos_iff_ne_zero, ne_eq, restrict₀_eq_zero_iff]
    aesop