awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
H : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀)
hy : 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 + y)) H) ⋯) :
        WithZero ↥(valueGroup v)) :
      WithZero ↥(valueGroup v))
    (max
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) ⋯) ⋯) :
          WithZero ↥(valueGroup v))
        0 :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
have pos : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: simp [← Units.val_le_val]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) (x + y)) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
    (max
        (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)))
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) ⋯) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
have pos : ∀ (H : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
  (_ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
  LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
    (max 0
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) sorry) sorry) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
Tactic: split_ifs with H _ hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
pos :
  ∀ (H : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
    (_ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
      (max 0
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
        ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) (x + y)) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
    (max
        (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)))
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) ⋯) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
have neg : ∀ (H : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
  (_ : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
  LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
    (max
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) _) sorry) :
          WithZero ↥(valueGroup v))
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) sorry) sorry) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
Tactic: split_ifs with H _ hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
pos :
  ∀ (H : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
    (_ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
      (max 0
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
        ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
neg :
  ∀ (H : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
    (_ : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
      (max
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) x) _) ⋯) :
            WithZero ↥(valueGroup v))
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
        ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) (x + y)) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
    (max
        (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)))
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) ⋯) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
have pos₁ : ∀ (H : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
  (hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (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 + y)) H) sorry) :
        WithZero ↥(valueGroup v)) :
      WithZero ↥(valueGroup v))
    (max 0
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) sorry) sorry) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
Tactic: split_ifs with H _ hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
H : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀)
hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (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 + y)) H) ⋯) :
        WithZero ↥(valueGroup v)) :
      WithZero ↥(valueGroup v))
    (max 0
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) ⋯) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
have pos : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
Tactic: simp [← Units.val_le_val]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
H :
  ¬(Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∨
      Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀))
⊢ LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
have H₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
Tactic: simp only [ne_eq, not_or, Decidable.not_not] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
H :
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
have neg : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀)
Tactic: simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply, H, ↓reduceDIte, max_self,
        le_zero_iff, dite_eq_left_iff, WithZero.coe_ne_zero, imp_false, Decidable.not_not]
-- 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 →*₀ Γ₀)) 0
      (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))) ↔
    LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have pos : ∀ (h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
  LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
    LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: split_ifs with h
-- 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
pos :
  ∀ (h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
    LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
      LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0
      (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))) ↔
    LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have neg : ∀ (h : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
  LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) h) sorry) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v)) ↔
    LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: split_ifs with h
-- 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
⊢ LT.lt.{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))) ↔
    LT.lt.{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 : Γ₀)),
  LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
    LT.lt.{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 : Γ₀)),
    LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ LT.lt.{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))) ↔
    LT.lt.{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 : Γ₀)),
  LT.lt.{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)) ↔
    LT.lt.{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 : Γ₀)),
    LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
      LT.lt.{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 : Γ₀)),
    LT.lt.{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)) ↔
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ LT.lt.{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))) ↔
    LT.lt.{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 : Γ₀) →
    (LT.lt.{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) ↔
      LT.lt.{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 : Γ₀)),
    LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
      LT.lt.{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 : Γ₀)),
    LT.lt.{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)) ↔
      LT.lt.{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 : Γ₀) →
      (LT.lt.{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) ↔
        LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
⊢ LT.lt.{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))) ↔
    LT.lt.{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 : Γ₀)),
  LT.lt.{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)) ↔
    LT.lt.{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 : R
g : ValueGroup₀ v
| LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
have rw : 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 : Γ₀)
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 ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
have conv_rhs : (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 : Γ₀)
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 ↔
    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 : (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.lt_iff_lt, restrict_def]