awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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 : ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk b₁ b₂
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b₁ b₂ ≤ ValueGroupWithZero.mk c₁ c₂
mk :
  ∀ (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))
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk c₁ c₂

Tactic:
rw [ValueGroupWithZero.mk_le_mk] at hab hbc ⊢

Premises used: ValuativeRel.ValueGroupWithZero.mk_le_mk
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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))
mk : @vle _ inst _ (a₁ * (↑c₂ : R) * (↑b₂ : R)) (c₁ * (↑a₂ : R) * (↑b₂ : R))
⊢ @vle _ inst _ (a₁ * (↑c₂ : R)) (c₁ * (↑a₂ : R))

Tactic:
apply vle_mul_cancel b₂.prop

Premises used: Subtype.prop, ValuativeRel.vle_mul_cancel
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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))
rw rw₁ : a₁ * (↑b₂ : R) * (↑c₂ : R) = a₁ * (↑b₂ : R) * (↑c₂ : R)
⊢ a₁ * (↑c₂ : R) * (↑b₂ : R) = a₁ * (↑b₂ : R) * (↑c₂ : R)

Tactic:
rw [mul_right_comm]

Premises used: mul_right_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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₁ * (↑b₂ : R) * (↑c₂ : R)) (b₁ * (↑a₂ : R) * (↑c₂ : R))

Tactic:
mul_vle_mul_left hab _

Premises used: ValuativeRel.mul_vle_mul_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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))
rw rw₁ : b₁ * (↑c₂ : R) * (↑a₂ : R) = b₁ * (↑c₂ : R) * (↑a₂ : R)
⊢ b₁ * (↑a₂ : R) * (↑c₂ : R) = b₁ * (↑c₂ : R) * (↑a₂ : R)

Tactic:
rw [mul_right_comm]

Premises used: mul_right_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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 _ (b₁ * (↑c₂ : R) * (↑a₂ : R)) (c₁ * (↑b₂ : R) * (↑a₂ : R))

Tactic:
mul_vle_mul_left hbc _

Premises used: ValuativeRel.mul_vle_mul_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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))
rw rw₁ : c₁ * (↑a₂ : R) * (↑b₂ : R) = c₁ * (↑a₂ : R) * (↑b₂ : R)
⊢ c₁ * (↑b₂ : R) * (↑a₂ : R) = c₁ * (↑a₂ : R) * (↑b₂ : R)

Tactic:
rw [mul_right_comm]

Premises used: mul_right_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
calc₂ : c₁ * (↑b₂ : R) * (↑a₂ : R) = c₁ * (↑a₂ : R) * (↑b₂ : R)
⊢ @vle _ inst _ (a₁ * (↑c₂ : R) * (↑b₂ : 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]

Premises used: ValuativeRel.mul_vle_mul_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
mk :
  ∀ (x : R) (y : ↥(posSubmonoid R)) (hab : ValueGroupWithZero.mk x y ≤ b) (hba : b ≤ ValueGroupWithZero.mk x y),
    ValueGroupWithZero.mk x y = b
⊢ a = b

Tactic:
induction a using ValueGroupWithZero.ind

Premises used: ValuativeRel.ValueGroupWithZero.ind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
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
⊢ ValueGroupWithZero.mk x_1 y_1 = b

Tactic:
induction b using ValueGroupWithZero.ind

Premises used: ValuativeRel.ValueGroupWithZero.ind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
hba : ValueGroupWithZero.mk x_2 y_2 ≤ ValueGroupWithZero.mk x_1 y_1
⊢ ValueGroupWithZero.mk x_1 y_1 = ValueGroupWithZero.mk x_2 y_2

Tactic:
ValueGroupWithZero.sound hab hba

Premises used: ValuativeRel.ValueGroupWithZero.sound
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
hba : ValueGroupWithZero.mk x_2 y_2 ≤ ValueGroupWithZero.mk x_1 y_1
⊢ ValueGroupWithZero.mk x_1 y_1 = ValueGroupWithZero.mk x_2 y_2

Tactic:
exact ValueGroupWithZero.sound hab hba

Premises used: ValuativeRel.ValueGroupWithZero.sound
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
a b : ValueGroupWithZero R
mk : ∀ (x : R) (y : ↥(posSubmonoid R)), ValueGroupWithZero.mk x y ≤ b ∨ b ≤ ValueGroupWithZero.mk x y
⊢ a ≤ b ∨ b ≤ a

Tactic:
induction a using ValueGroupWithZero.ind

Premises used: ValuativeRel.ValueGroupWithZero.ind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
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
⊢ ValueGroupWithZero.mk x_1 y_1 ≤ b ∨ b ≤ ValueGroupWithZero.mk x_1 y_1

Tactic:
induction b using ValueGroupWithZero.ind

Premises used: ValuativeRel.ValueGroupWithZero.ind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
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))
⊢ ValueGroupWithZero.mk x_1 y_1 ≤ ValueGroupWithZero.mk x_2 y_2 ∨
    ValueGroupWithZero.mk x_2 y_2 ≤ ValueGroupWithZero.mk x_1 y_1

Tactic:
rw [ValueGroupWithZero.mk_le_mk, ValueGroupWithZero.mk_le_mk]

Premises used: ValuativeRel.ValueGroupWithZero.mk_le_mk
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
⊢ @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:
apply vle_total

Premises used: ValuativeRel.vle_total
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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))
rw₂ rw₃ : ¬@vle _ inst _ (y * (↑t : R)) (x * (↑s : R)) ↔ ¬@vle _ inst _ (y * (↑t : R)) (x * (↑s : R))
⊢ ValueGroupWithZero.mk x t < ValueGroupWithZero.mk y s ↔ x * (↑s : R) <ᵥ y * (↑t : R)

Tactic:
rw [lt_iff_not_ge, ← not_vle, mk_le_mk]

Premises used: lt_iff_not_ge, ValuativeRel.ValueGroupWithZero.mk_le_mk, ValuativeRel.not_vle
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk 0 1 < ValueGroupWithZero.mk x s ↔ 0 <ᵥ x

Tactic:
simp [-mk_zero]

Premises used: ValuativeRel.ValueGroupWithZero.mk_zero
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x : R
y : ↥(posSubmonoid R)
rw : @vle _ inst _ (0 * (↑y : R)) (x * (↑1 : R))
⊢ ⊥ ≤ ValueGroupWithZero.mk x y

Tactic:
rw [ValueGroupWithZero.bot_eq_zero, ← ValueGroupWithZero.mk_zero 1, ValueGroupWithZero.mk_le_mk]

Premises used: ValuativeRel.ValueGroupWithZero.bot_eq_zero, ValuativeRel.ValueGroupWithZero.mk_zero, ValuativeRel.ValueGroupWithZero.mk_le_mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x : R
y : ↥(posSubmonoid R)
⊢ @vle _ inst _ (0 * (↑y : R)) (x * (↑1 : R))

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
mk : ∀ (x : R) (y : ↥(posSubmonoid R)) (hab : ValueGroupWithZero.mk x y ≤ b), ValueGroupWithZero.mk x y * c ≤ b * c
⊢ a * c ≤ b * c

Tactic:
induction a using ValueGroupWithZero.ind

Premises used: ValuativeRel.ValueGroupWithZero.ind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
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
⊢ ValueGroupWithZero.mk x_1 y_1 * c ≤ b * c

Tactic:
induction b using ValueGroupWithZero.ind

Premises used: ValuativeRel.ValueGroupWithZero.ind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
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
⊢ ValueGroupWithZero.mk x_1 y_1 * c ≤ ValueGroupWithZero.mk x_2 y_2 * c

Tactic:
induction c using ValueGroupWithZero.ind

Premises used: ValuativeRel.ValueGroupWithZero.ind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
mk : @vle _ inst _ (x_1 * x_3 * ((↑y_2 : R) * (↑y_3 : R))) (x_2 * x_3 * ((↑y_1 : R) * (↑y_3 : 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

Tactic:
simp only [ValueGroupWithZero.mk_mul_mk, ValueGroupWithZero.mk_le_mk, Submonoid.coe_mul]

Premises used: ValuativeRel.ValueGroupWithZero.mk_mul_mk, ValuativeRel.ValueGroupWithZero.mk_le_mk, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
mk : @vle _ inst _ (x_1 * (↑y_2 : R) * (x_3 * (↑y_3 : R))) (x_2 * x_3 * ((↑y_1 : R) * (↑y_3 : R)))
⊢ @vle _ inst _ (x_1 * x_3 * ((↑y_2 : R) * (↑y_3 : R))) (x_2 * x_3 * ((↑y_1 : R) * (↑y_3 : R)))

Tactic:
conv_lhs => apply mul_mul_mul_comm

Premises used: mul_mul_mul_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
mk : @vle _ inst _ (x_1 * (↑y_2 : R) * (x_3 * (↑y_3 : R))) (x_2 * (↑y_1 : R) * (x_3 * (↑y_3 : R)))
⊢ @vle _ inst _ (x_1 * (↑y_2 : R) * (x_3 * (↑y_3 : R))) (x_2 * x_3 * ((↑y_1 : R) * (↑y_3 : R)))

Tactic:
conv_rhs => apply mul_mul_mul_comm

Premises used: mul_mul_mul_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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 * (↑y_1 : R) * (x_3 * (↑y_3 : R)))

Tactic:
mul_vle_mul_left hab _

Premises used: ValuativeRel.mul_vle_mul_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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 * (↑y_1 : R) * (x_3 * (↑y_3 : R)))

Tactic:
exact mul_vle_mul_left hab _

Premises used: ValuativeRel.mul_vle_mul_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y z x : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero R

Tactic:
exact if h : x ≤ᵥ 0 then 0 else .mk s ⟨x, h⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y z x : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero R

Tactic:
classical exact if h : x ≤ᵥ 0 then 0 else .mk s ⟨x, h⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
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)
⊢ 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
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
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)
⊢ 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
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
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)
⊢ 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
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
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:
simp [hx, hy]
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
hy : ¬@vle _ inst _ y 0
neg : @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:
absurd hy