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 : R
a b c : ValueGroupWithZero R
mk : ∀ (x : R) (y : ↥(posSubmonoid R)), ValueGroupWithZero.mk x y * b * c = ValueGroupWithZero.mk x y * (b * c)
⊢ a * b * c = a * (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)
mk :
  ∀ (x : R) (y : ↥(posSubmonoid R)),
    ValueGroupWithZero.mk x_1 y_1 * ValueGroupWithZero.mk x y * c =
      ValueGroupWithZero.mk x_1 y_1 * (ValueGroupWithZero.mk x y * c)
⊢ ValueGroupWithZero.mk x_1 y_1 * b * c = ValueGroupWithZero.mk x_1 y_1 * (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)
mk :
  ∀ (x : R) (y : ↥(posSubmonoid R)),
    ValueGroupWithZero.mk x_1 y_1 * ValueGroupWithZero.mk x_2 y_2 * ValueGroupWithZero.mk x y =
      ValueGroupWithZero.mk x_1 y_1 * (ValueGroupWithZero.mk x_2 y_2 * ValueGroupWithZero.mk x y)
⊢ ValueGroupWithZero.mk x_1 y_1 * ValueGroupWithZero.mk x_2 y_2 * c =
    ValueGroupWithZero.mk x_1 y_1 * (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)
x_3 : R
y_3 : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x_1 y_1 * ValueGroupWithZero.mk x_2 y_2 * ValueGroupWithZero.mk x_3 y_3 =
    ValueGroupWithZero.mk x_1 y_1 * (ValueGroupWithZero.mk x_2 y_2 * ValueGroupWithZero.mk x_3 y_3)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)), 1 * ValueGroupWithZero.mk x y = ValueGroupWithZero.mk x y

Tactic:
simp [← ValueGroupWithZero.mk_one_one]

Premises used: ValuativeRel.ValueGroupWithZero.mk_one_one
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)), ValueGroupWithZero.mk x y * 1 = ValueGroupWithZero.mk x y

Tactic:
simp [← ValueGroupWithZero.mk_one_one]

Premises used: ValuativeRel.ValueGroupWithZero.mk_one_one
-- 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))
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0)) x
      s)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0)) y
      t)

Tactic:
simp
-- 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))
n : ℕ
ih :
  Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) x s)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) y t)
succ :
  ValueGroupWithZero.mk (y ^ n) (t ^ n) * ValueGroupWithZero.mk x s =
    ValueGroupWithZero.mk (y ^ n) (t ^ n) * ValueGroupWithZero.mk y t
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ (n + 1)) (b ^ (n + 1))) x s)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ (n + 1)) (b ^ (n + 1))) y t)

Tactic:
simp only [pow_succ, ← ValueGroupWithZero.mk_mul_mk, ih]

Premises used: pow_succ, ValuativeRel.ValueGroupWithZero.mk_mul_mk
-- 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))
n : ℕ
ih :
  Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) x s)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) y t)
succ : ValueGroupWithZero.mk x s = ValueGroupWithZero.mk y t
⊢ ValueGroupWithZero.mk (y ^ n) (t ^ n) * ValueGroupWithZero.mk x s =
    ValueGroupWithZero.mk (y ^ n) (t ^ n) * ValueGroupWithZero.mk y t

Tactic:
apply congrArg (_ * ·)

Premises used: HMul.hMul, congrArg
-- 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))
n : ℕ
ih :
  Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) x s)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) y t)
⊢ ValueGroupWithZero.mk x s = ValueGroupWithZero.mk y t

Tactic:
ValueGroupWithZero.sound h₁ h₂

Premises used: ValuativeRel.ValueGroupWithZero.sound
-- 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))
n : ℕ
ih :
  Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) x s)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) y t)
⊢ ValueGroupWithZero.mk x s = ValueGroupWithZero.mk y t

Tactic:
exact ValueGroupWithZero.sound h₁ h₂

Premises used: ValuativeRel.ValueGroupWithZero.sound
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z : R
n : ℕ
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))
zero :
  Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0)) x
      s)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0)) y
      t)
succ :
  ∀ (n : ℕ)
    (ih :
      Eq.{u_1 + 1} (α := ValueGroupWithZero R)
        ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) x s)
        ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) y t)),
    Eq.{u_1 + 1} (α := ValueGroupWithZero R)
      ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ (n + 1)) (b ^ (n + 1))) x s)
      ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ (n + 1)) (b ^ (n + 1))) y t)
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) x s)
    ((fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) y t)

Tactic:
induction n with
    | zero => simp
    | succ n ih =>
      simp only [pow_succ, ← ValueGroupWithZero.mk_mul_mk, ih]
      apply congrArg (_ * ·)
      exact ValueGroupWithZero.sound h₁ h₂

Premises used: HMul.hMul, congrArg, pow_succ, ValuativeRel.ValueGroupWithZero.mk_mul_mk, 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
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)),
    ValueGroupWithZero.lift
        (fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0))
        ⋯ (ValueGroupWithZero.mk x y) =
      1

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
n : ℕ
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)),
    ValueGroupWithZero.lift (fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ (n + 1)) (b ^ (n + 1))) ⋯
        (ValueGroupWithZero.mk x y) =
      ValueGroupWithZero.lift (fun (a : R) (b : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a ^ n) (b ^ n)) ⋯
          (ValueGroupWithZero.mk x y) *
        ValueGroupWithZero.mk x y

Tactic:
simp [pow_succ]

Premises used: pow_succ
-- 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)
⊢ 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:
simp [mul_comm]

Premises used: 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
x_2 : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk (0 * x_1) (1 * x_2) = ValueGroupWithZero.mk 0 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z x_1 : R
x_2 : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk (x_1 * 0) (x_2 * 1) = ValueGroupWithZero.mk 0 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
pos :
  ∀ (hw : @vle _ inst _ w 0),
    Eq (α := Prop)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        x s z v)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        y t w u)
neg :
  ∀ (hw : ¬@vle _ inst _ w 0),
    Eq (α := Prop)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        x s z v)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        y t w u)
⊢ Eq (α := Prop)
    ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
      x s z v)
    ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
      y t w u)

Tactic:
by_cases hw : w ≤ᵥ 0
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
pos :
  ∀ (hz : @vle _ inst _ z 0),
    Eq (α := Prop)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        x s z v)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        y t w u)
neg :
  ∀ (hz : ¬@vle _ inst _ z 0),
    Eq (α := Prop)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        x s z v)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        y t w u)
⊢ Eq (α := Prop)
    ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
      x s z v)
    ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
      y t w u)

Tactic:
by_cases hz : z ≤ᵥ 0
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : ¬@vle _ inst _ w 0
pos :
  ∀ (hz : @vle _ inst _ z 0),
    Eq (α := Prop)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        x s z v)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        y t w u)
neg :
  ∀ (hz : ¬@vle _ inst _ z 0),
    Eq (α := Prop)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        x s z v)
      ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        y t w u)
⊢ Eq (α := Prop)
    ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
      x s z v)
    ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
      y t w u)

Tactic:
by_cases hz : z ≤ᵥ 0
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
hz : @vle _ inst _ z 0
⊢ Eq (α := Prop)
    ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
      x s z v)
    ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
      y t w u)

Tactic:
propext ⟨fun h => vle_trans ?_ (zero_vle _), fun h => vle_trans ?_ (zero_vle _)⟩

Premises used: HMul.hMul, ValuativeRel.zero_vle, ValuativeRel.vle_trans, Iff.intro, propext, Subtype.val
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
hz : @vle _ inst _ z 0
pos :
  ∀
    (h :
      (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        x s z v),
    @vle _ inst _ (y * (↑u : R)) 0
pos₁ :
  ∀
    (h :
      (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        y t w u),
    @vle _ inst _ (x * (↑v : R)) 0
⊢ Eq (α := Prop)
    ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
      x s z v)
    ((fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
      y t w u)

Tactic:
refine propext ⟨fun h => vle_trans ?_ (zero_vle _), fun h => vle_trans ?_ (zero_vle _)⟩

Premises used: ValuativeRel.zero_vle, ValuativeRel.vle_trans, Iff.intro, propext
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
hz : @vle _ inst _ z 0
h :
  (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) x
    s z v
pos : @vle _ inst _ (y * (↑u : R) * (↑(s * v) : R)) (0 * (↑(s * v) : R))
⊢ @vle _ inst _ (y * (↑u : R)) 0

Tactic:
apply vle_mul_cancel (s * v).prop

Premises used: HMul.hMul, 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_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
hz : @vle _ inst _ z 0
h :
  (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) x
    s z v
pos : @vle _ inst _ (y * (↑s : R) * (↑v : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
⊢ @vle _ inst _ (y * (↑u : R) * (↑(s * v) : R)) (0 * (↑(s * v) : R))

Tactic:
rw [mul_right_comm, Submonoid.coe_mul, ← mul_assoc]

Premises used: mul_assoc, mul_right_comm, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
hz : @vle _ inst _ z 0
h :
  (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) x
    s z v
pos : @vle _ inst _ (x * (↑t : R) * (↑v : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
⊢ @vle _ inst _ (y * (↑s : R) * (↑v : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))

Tactic:
apply (mul_vle_mul_left (mul_vle_mul_left h₂ v) u).trans

Premises used: ValuativeRel.vle.trans, Subtype.val, 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_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
hz : @vle _ inst _ z 0
h :
  (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) x
    s z v
pos : @vle _ inst _ (x * (↑v : R) * (↑t : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
⊢ @vle _ inst _ (x * (↑t : R) * (↑v : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))

Tactic:
rw [mul_right_comm x]

Premises used: mul_right_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
hz : @vle _ inst _ z 0
h :
  (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) x
    s z v
pos : @vle _ inst _ (z * (↑s : R) * (↑t : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
⊢ @vle _ inst _ (x * (↑v : R) * (↑t : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))

Tactic:
apply (mul_vle_mul_left (mul_vle_mul_left h t) u).trans

Premises used: ValuativeRel.vle.trans, Subtype.val, 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_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
hz : @vle _ inst _ z 0
h :
  (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) x
    s z v
pos : @vle _ inst _ (0 * (↑s : R) * (↑t : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
⊢ @vle _ inst _ (z * (↑s : R) * (↑t : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))

Tactic:
apply vle_trans (mul_vle_mul_left (mul_vle_mul_left (mul_vle_mul_left hz s) t) u)

Premises used: ValuativeRel.vle_trans, Subtype.val, 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_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
hz : @vle _ inst _ z 0
h :
  (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) x
    s z v
⊢ @vle _ inst _ (0 * (↑s : R) * (↑t : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
hz : @vle _ inst _ z 0
h :
  (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) y
    t w u
pos : @vle _ inst _ (x * (↑v : R) * (↑(t * u) : R)) (0 * (↑(t * u) : R))
⊢ @vle _ inst _ (x * (↑v : R)) 0

Tactic:
apply vle_mul_cancel (t * u).prop

Premises used: HMul.hMul, 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_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
hw : @vle _ inst _ w 0
hz : @vle _ inst _ z 0
h :
  (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) y
    t w u
pos : @vle _ inst _ (x * (↑t : R) * (↑u : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
⊢ @vle _ inst _ (x * (↑v : R) * (↑(t * u) : R)) (0 * (↑(t * u) : R))

Tactic:
rw [mul_right_comm, Submonoid.coe_mul, ← mul_assoc]

Premises used: mul_assoc, mul_right_comm, Submonoid.coe_mul