awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : @vle _ inst _ (a₁ * (↑b₂ : R)) (b₁ * (↑a₂ : R))
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : @vle _ inst _ (b₁ * (↑c₂ : R)) (c₁ * (↑b₂ : R))
⊢ @vle _ inst _ (a₁ * (↑c₂ : R)) (c₁ * (↑a₂ : R))
have mk : @vle _ inst _ (a₁ * (↑c₂ : R) * (↑b₂ : R)) (c₁ * (↑a₂ : R) * (↑b₂ : R))
Tactic: apply vle_mul_cancel b₂.prop
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : @vle _ inst _ (a₁ * (↑b₂ : R)) (b₁ * (↑a₂ : R))
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : @vle _ inst _ (b₁ * (↑c₂ : R)) (c₁ * (↑b₂ : R))
⊢ a₁ * (↑c₂ : R) * (↑b₂ : R) = a₁ * (↑b₂ : R) * (↑c₂ : R)
have rw : a₁ * (↑b₂ : R) * (↑c₂ : R) = a₁ * (↑b₂ : R) * (↑c₂ : R)
Tactic: rw [mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : @vle _ inst _ (a₁ * (↑b₂ : R)) (b₁ * (↑a₂ : R))
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : @vle _ inst _ (b₁ * (↑c₂ : R)) (c₁ * (↑b₂ : R))
⊢ b₁ * (↑a₂ : R) * (↑c₂ : R) = b₁ * (↑c₂ : R) * (↑a₂ : R)
have rw : b₁ * (↑c₂ : R) * (↑a₂ : R) = b₁ * (↑c₂ : R) * (↑a₂ : R)
Tactic: rw [mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : @vle _ inst _ (a₁ * (↑b₂ : R)) (b₁ * (↑a₂ : R))
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : @vle _ inst _ (b₁ * (↑c₂ : R)) (c₁ * (↑b₂ : R))
⊢ c₁ * (↑b₂ : R) * (↑a₂ : R) = c₁ * (↑a₂ : R) * (↑b₂ : R)
have rw : c₁ * (↑a₂ : R) * (↑b₂ : R) = c₁ * (↑a₂ : R) * (↑b₂ : R)
Tactic: rw [mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : @vle _ inst _ (a₁ * (↑b₂ : R)) (b₁ * (↑a₂ : R))
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : @vle _ inst _ (b₁ * (↑c₂ : R)) (c₁ * (↑b₂ : R))
⊢ @vle _ inst _ (a₁ * (↑c₂ : R) * (↑b₂ : R)) (c₁ * (↑a₂ : R) * (↑b₂ : R))
have calc : a₁ * (↑c₂ : R) * (↑b₂ : R) = a₁ * (↑b₂ : R) * (↑c₂ : R)
Tactic: calc a₁ * c₂ * b₂
      _ = a₁ * b₂ * c₂ := by rw [mul_right_comm]
      _ ≤ᵥ b₁ * a₂ * c₂ := mul_vle_mul_left hab _
      _ = b₁ * c₂ * a₂ := by rw [mul_right_comm]
      _ ≤ᵥ c₁ * b₂ * a₂ := mul_vle_mul_left hbc _
      _ = c₁ * a₂ * b₂ := by rw [mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : @vle _ inst _ (a₁ * (↑b₂ : R)) (b₁ * (↑a₂ : R))
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : @vle _ inst _ (b₁ * (↑c₂ : R)) (c₁ * (↑b₂ : R))
calc : a₁ * (↑c₂ : R) * (↑b₂ : R) = a₁ * (↑b₂ : R) * (↑c₂ : R)
⊢ @vle _ inst _ (a₁ * (↑c₂ : R) * (↑b₂ : R)) (c₁ * (↑a₂ : R) * (↑b₂ : R))
have calc₁ : b₁ * (↑a₂ : R) * (↑c₂ : R) = b₁ * (↑c₂ : R) * (↑a₂ : R)
Tactic: calc a₁ * c₂ * b₂
      _ = a₁ * b₂ * c₂ := by rw [mul_right_comm]
      _ ≤ᵥ b₁ * a₂ * c₂ := mul_vle_mul_left hab _
      _ = b₁ * c₂ * a₂ := by rw [mul_right_comm]
      _ ≤ᵥ c₁ * b₂ * a₂ := mul_vle_mul_left hbc _
      _ = c₁ * a₂ * b₂ := by rw [mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : @vle _ inst _ (a₁ * (↑b₂ : R)) (b₁ * (↑a₂ : R))
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : @vle _ inst _ (b₁ * (↑c₂ : R)) (c₁ * (↑b₂ : R))
calc : a₁ * (↑c₂ : R) * (↑b₂ : R) = a₁ * (↑b₂ : R) * (↑c₂ : R)
calc₁ : b₁ * (↑a₂ : R) * (↑c₂ : R) = b₁ * (↑c₂ : R) * (↑a₂ : R)
⊢ @vle _ inst _ (a₁ * (↑c₂ : R) * (↑b₂ : R)) (c₁ * (↑a₂ : R) * (↑b₂ : R))
have calc₂ : c₁ * (↑b₂ : R) * (↑a₂ : R) = c₁ * (↑a₂ : R) * (↑b₂ : R)
Tactic: calc a₁ * c₂ * b₂
      _ = a₁ * b₂ * c₂ := by rw [mul_right_comm]
      _ ≤ᵥ b₁ * a₂ * c₂ := mul_vle_mul_left hab _
      _ = b₁ * c₂ * a₂ := by rw [mul_right_comm]
      _ ≤ᵥ c₁ * b₂ * a₂ := mul_vle_mul_left hbc _
      _ = c₁ * a₂ * b₂ := by rw [mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
a b : ValueGroupWithZero R
hab : a ≤ b
hba : b ≤ a
⊢ a = b
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)) (hab : ValueGroupWithZero.mk x y ≤ b) (hba : b ≤ ValueGroupWithZero.mk x y),
  ValueGroupWithZero.mk x y = b
Tactic: induction a using ValueGroupWithZero.ind
Cleared hypotheses: a, hab, hba
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
b : ValueGroupWithZero R
x_1 : R
y_1 : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x_1 y_1 ≤ b
hba : b ≤ ValueGroupWithZero.mk x_1 y_1
⊢ ValueGroupWithZero.mk x_1 y_1 = b
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)) (hab : ValueGroupWithZero.mk x_1 y_1 ≤ ValueGroupWithZero.mk x y)
  (hba : ValueGroupWithZero.mk x y ≤ ValueGroupWithZero.mk x_1 y_1),
  ValueGroupWithZero.mk x_1 y_1 = ValueGroupWithZero.mk x y
Tactic: induction b using ValueGroupWithZero.ind
Cleared hypotheses: b, hab, hba
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
a b : ValueGroupWithZero R
⊢ a ≤ b ∨ b ≤ a
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)), ValueGroupWithZero.mk x y ≤ b ∨ b ≤ ValueGroupWithZero.mk x y
Tactic: induction a using ValueGroupWithZero.ind
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
b : ValueGroupWithZero R
x_1 : R
y_1 : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x_1 y_1 ≤ b ∨ b ≤ ValueGroupWithZero.mk x_1 y_1
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)),
  ValueGroupWithZero.mk x_1 y_1 ≤ ValueGroupWithZero.mk x y ∨ ValueGroupWithZero.mk x y ≤ ValueGroupWithZero.mk x_1 y_1
Tactic: induction b using ValueGroupWithZero.ind
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z x_1 : R
y_1 : ↥(posSubmonoid R)
x_2 : R
y_2 : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x_1 y_1 ≤ ValueGroupWithZero.mk x_2 y_2 ∨
    ValueGroupWithZero.mk x_2 y_2 ≤ ValueGroupWithZero.mk x_1 y_1
have mk : @vle _ inst _ (x_1 * (↑y_2 : R)) (x_2 * (↑y_1 : R)) ∨ @vle _ inst _ (x_2 * (↑y_1 : R)) (x_1 * (↑y_2 : R))
Tactic: rw [ValueGroupWithZero.mk_le_mk, ValueGroupWithZero.mk_le_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
t s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x t < ValueGroupWithZero.mk y s ↔ x * (↑s : R) <ᵥ y * (↑t : R)
have rw : ¬ValueGroupWithZero.mk y s ≤ ValueGroupWithZero.mk x t ↔ x * (↑s : R) <ᵥ y * (↑t : R)
Tactic: rw [lt_iff_not_ge, ← not_vle, mk_le_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
t s : ↥(posSubmonoid R)
rw : ¬ValueGroupWithZero.mk y s ≤ ValueGroupWithZero.mk x t ↔ x * (↑s : R) <ᵥ y * (↑t : R)
⊢ ValueGroupWithZero.mk x t < ValueGroupWithZero.mk y s ↔ x * (↑s : R) <ᵥ y * (↑t : R)
have rw₁ : ¬ValueGroupWithZero.mk y s ≤ ValueGroupWithZero.mk x t ↔ ¬@vle _ inst _ (y * (↑t : R)) (x * (↑s : R))
Tactic: rw [lt_iff_not_ge, ← not_vle, mk_le_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
t s : ↥(posSubmonoid R)
rw : ¬ValueGroupWithZero.mk y s ≤ ValueGroupWithZero.mk x t ↔ x * (↑s : R) <ᵥ y * (↑t : R)
rw₁ : ¬ValueGroupWithZero.mk y s ≤ ValueGroupWithZero.mk x t ↔ ¬@vle _ inst _ (y * (↑t : R)) (x * (↑s : R))
⊢ ValueGroupWithZero.mk x t < ValueGroupWithZero.mk y s ↔ x * (↑s : R) <ᵥ y * (↑t : R)
have rw₂ : ¬@vle _ inst _ (y * (↑t : R)) (x * (↑s : R)) ↔ ¬@vle _ inst _ (y * (↑t : R)) (x * (↑s : R))
Tactic: rw [lt_iff_not_ge, ← not_vle, mk_le_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x : R
y : ↥(posSubmonoid R)
⊢ ⊥ ≤ ValueGroupWithZero.mk x y
have rw : @vle _ inst _ (0 * (↑y : R)) (x * (↑1 : R))
Tactic: rw [ValueGroupWithZero.bot_eq_zero, ← ValueGroupWithZero.mk_zero 1, ValueGroupWithZero.mk_le_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
a b : ValueGroupWithZero R
hab : a ≤ b
c : ValueGroupWithZero R
⊢ a * c ≤ b * c
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)) (hab : ValueGroupWithZero.mk x y ≤ b), ValueGroupWithZero.mk x y * c ≤ b * c
Tactic: induction a using ValueGroupWithZero.ind
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
b c : ValueGroupWithZero R
x_1 : R
y_1 : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x_1 y_1 ≤ b
⊢ ValueGroupWithZero.mk x_1 y_1 * c ≤ b * c
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)) (hab : ValueGroupWithZero.mk x_1 y_1 ≤ ValueGroupWithZero.mk x y),
  ValueGroupWithZero.mk x_1 y_1 * c ≤ ValueGroupWithZero.mk x y * c
Tactic: induction b using ValueGroupWithZero.ind
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
c : ValueGroupWithZero R
x_1 : R
y_1 : ↥(posSubmonoid R)
x_2 : R
y_2 : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x_1 y_1 ≤ ValueGroupWithZero.mk x_2 y_2
⊢ ValueGroupWithZero.mk x_1 y_1 * c ≤ ValueGroupWithZero.mk x_2 y_2 * c
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)),
  ValueGroupWithZero.mk x_1 y_1 * ValueGroupWithZero.mk x y ≤ ValueGroupWithZero.mk x_2 y_2 * ValueGroupWithZero.mk x y
Tactic: induction c using ValueGroupWithZero.ind
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z x_1 : R
y_1 : ↥(posSubmonoid R)
x_2 : R
y_2 : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x_1 y_1 ≤ ValueGroupWithZero.mk x_2 y_2
x_3 : R
y_3 : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x_1 y_1 * ValueGroupWithZero.mk x_3 y_3 ≤
    ValueGroupWithZero.mk x_2 y_2 * ValueGroupWithZero.mk x_3 y_3
have mk : @vle _ inst _ (x_1 * x_3 * ((↑y_2 : R) * (↑y_3 : R))) (x_2 * x_3 * ((↑y_1 : R) * (↑y_3 : R)))
Tactic: simp only [ValueGroupWithZero.mk_mul_mk, ValueGroupWithZero.mk_le_mk, Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z x_1 : R
y_1 : ↥(posSubmonoid R)
x_2 : R
y_2 : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x_1 y_1 ≤ ValueGroupWithZero.mk x_2 y_2
x_3 : R
y_3 : ↥(posSubmonoid R)
⊢ @vle _ inst _ (x_1 * x_3 * ((↑y_2 : R) * (↑y_3 : R))) (x_2 * x_3 * ((↑y_1 : R) * (↑y_3 : R)))
have mk : @vle _ inst _ (x_1 * (↑y_2 : R) * (x_3 * (↑y_3 : R))) (x_2 * x_3 * ((↑y_1 : R) * (↑y_3 : R)))
Tactic: conv_lhs => apply mul_mul_mul_comm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z x_1 : R
y_1 : ↥(posSubmonoid R)
x_2 : R
y_2 : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x_1 y_1 ≤ ValueGroupWithZero.mk x_2 y_2
x_3 : R
y_3 : ↥(posSubmonoid R)
⊢ @vle _ inst _ (x_1 * (↑y_2 : R) * (x_3 * (↑y_3 : R))) (x_2 * x_3 * ((↑y_1 : R) * (↑y_3 : R)))
have mk : @vle _ inst _ (x_1 * (↑y_2 : R) * (x_3 * (↑y_3 : R))) (x_2 * (↑y_1 : R) * (x_3 * (↑y_3 : R)))
Tactic: conv_rhs => apply mul_mul_mul_comm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
have pos : ∀ (hx : @vle _ inst _ x 0),
  Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
Tactic: by_cases hx : x ≤ᵥ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
pos :
  ∀ (hx : @vle _ inst _ x 0),
    Eq.{u_1 + 1} (α := ValueGroupWithZero R)
      ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
          (if h : @vle _ inst _ x 0 then 0
            else
              ValueGroupWithZero.mk (↑s : R)
                (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
            ValueGroupWithZero R))
        x s)
      ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
          (if h : @vle _ inst _ x 0 then 0
            else
              ValueGroupWithZero.mk (↑s : R)
                (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
            ValueGroupWithZero R))
        y t)
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
have neg : ∀ (hx : ¬@vle _ inst _ x 0),
  Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
Tactic: by_cases hx : x ≤ᵥ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : @vle _ inst _ x 0
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
have pos : ∀ (hy : @vle _ inst _ y 0),
  Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
Tactic: by_cases hy : y ≤ᵥ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : @vle _ inst _ x 0
pos :
  ∀ (hy : @vle _ inst _ y 0),
    Eq.{u_1 + 1} (α := ValueGroupWithZero R)
      ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
          (if h : @vle _ inst _ x 0 then 0
            else
              ValueGroupWithZero.mk (↑s : R)
                (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
            ValueGroupWithZero R))
        x s)
      ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
          (if h : @vle _ inst _ x 0 then 0
            else
              ValueGroupWithZero.mk (↑s : R)
                (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
            ValueGroupWithZero R))
        y t)
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
have neg : ∀ (hy : ¬@vle _ inst _ y 0),
  Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
Tactic: by_cases hy : y ≤ᵥ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : ¬@vle _ inst _ x 0
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
have pos : ∀ (hy : @vle _ inst _ y 0),
  Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
Tactic: by_cases hy : y ≤ᵥ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : ¬@vle _ inst _ x 0
pos :
  ∀ (hy : @vle _ inst _ y 0),
    Eq.{u_1 + 1} (α := ValueGroupWithZero R)
      ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
          (if h : @vle _ inst _ x 0 then 0
            else
              ValueGroupWithZero.mk (↑s : R)
                (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
            ValueGroupWithZero R))
        x s)
      ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
          (if h : @vle _ inst _ x 0 then 0
            else
              ValueGroupWithZero.mk (↑s : R)
                (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
            ValueGroupWithZero R))
        y t)
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
have neg : ∀ (hy : ¬@vle _ inst _ y 0),
  Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
Tactic: by_cases hy : y ≤ᵥ 0