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_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 _ (y * (↑s : R) * (↑u : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
⊢ @vle _ inst _ (x * (↑t : R) * (↑u : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))

Tactic:
apply (mul_vle_mul_left (mul_vle_mul_left h₁ u) v).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))) y
    t w u
pos : @vle _ inst _ (y * (↑u : R) * (↑s : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
⊢ @vle _ inst _ (y * (↑s : R) * (↑u : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))

Tactic:
rw [mul_right_comm y]

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))) y
    t w u
pos : @vle _ inst _ (w * (↑t : R) * (↑s : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
⊢ @vle _ inst _ (y * (↑u : R) * (↑s : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))

Tactic:
apply (mul_vle_mul_left (mul_vle_mul_left h s) v).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))) y
    t w u
pos : @vle _ inst _ (0 * (↑t : R) * (↑s : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
⊢ @vle _ inst _ (w * (↑t : R) * (↑s : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))

Tactic:
apply vle_trans (mul_vle_mul_left (mul_vle_mul_left (mul_vle_mul_left hw t) s) v)

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))) y
    t w u
⊢ @vle _ inst _ (0 * (↑t : R) * (↑s : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : 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
neg : @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:
absurd hz
-- 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
neg : @vle _ inst _ (z * (↑u : R)) (0 * (↑u : R))
⊢ @vle _ inst _ z 0

Tactic:
apply vle_mul_cancel u.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_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
⊢ @vle _ inst _ (z * (↑u : R)) (0 * (↑u : R))

Tactic:
simpa using h₃.trans (mul_vle_mul_left hw v)

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
pos : @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)

Tactic:
absurd hw
-- 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 : @vle _ inst _ (w * (↑v : R)) (0 * (↑v : R))
⊢ @vle _ inst _ w 0

Tactic:
apply vle_mul_cancel v.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_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
⊢ @vle _ inst _ (w * (↑v : R)) (0 * (↑v : R))

Tactic:
simpa using h₄.trans (mul_vle_mul_left hz 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
⊢ 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 => ?_, fun h => ?_⟩

Premises used: 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
neg :
  ∀
    (h :
      (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₁ :
  ∀
    (h :
      (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦
          @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
        y t w u),
    (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R)))
      x s z v
⊢ 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 => ?_, fun h => ?_⟩

Premises used: 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
neg : @vle _ inst _ (y * (↑u : R) * (↑s : R)) (w * (↑t : R) * (↑s : R))
⊢ (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) y
    t w u

Tactic:
apply vle_mul_cancel s.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_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
neg : @vle _ inst _ (y * (↑u : R) * (↑s : R) * z) (w * (↑t : R) * (↑s : R) * z)
⊢ @vle _ inst _ (y * (↑u : R) * (↑s : R)) (w * (↑t : R) * (↑s : R))

Tactic:
apply vle_mul_cancel hz

Premises used: 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
⊢ y * (↑u : R) * (↑s : R) * z = y * (↑s : R) * (z * (↑u : R))

Tactic:
ring
-- 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 _ (y * (↑s : R) * (z * (↑u : R))) (x * (↑t : R) * (w * (↑v : R)))

Tactic:
gcongr
-- 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
⊢ x * (↑t : R) * (w * (↑v : R)) = x * (↑v : R) * ((↑t : R) * w)

Tactic:
ring
-- 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 _ (x * (↑v : R) * ((↑t : R) * w)) (z * (↑s : R) * ((↑t : R) * w))

Tactic:
gcongr
-- 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
⊢ z * (↑s : R) * ((↑t : R) * w) = w * (↑t : R) * (↑s : R) * z

Tactic:
ring
-- 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
calc : y * (↑u : R) * (↑s : R) * z = y * (↑s : R) * (z * (↑u : R))
calc₁ : @vle _ inst _ (y * (↑s : R) * (z * (↑u : R))) (x * (↑t : R) * (w * (↑v : R)))
calc₂ : x * (↑t : R) * (w * (↑v : R)) = x * (↑v : R) * ((↑t : R) * w)
calc₃ : @vle _ inst _ (x * (↑v : R) * ((↑t : R) * w)) (z * (↑s : R) * ((↑t : R) * w))
calc₄ : z * (↑s : R) * ((↑t : R) * w) = w * (↑t : R) * (↑s : R) * z
⊢ @vle _ inst _ (y * (↑u : R) * (↑s : R) * z) (w * (↑t : R) * (↑s : R) * z)

Tactic:
calc y * u * s * z
          _ = y * s * (z * u) := by ring
          _ ≤ᵥ x * t * (w * v) := by gcongr
          _ = x * v * (t * w) := by ring
          _ ≤ᵥ z * s * (t * w) := by gcongr
          _ = w * t * s * z := by ring

Premises used: HMul.hMul, 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
h :
  (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) y
    t w u
neg : @vle _ inst _ (x * (↑v : R) * (↑t : R)) (z * (↑s : R) * (↑t : R))
⊢ (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) x
    s z v

Tactic:
apply vle_mul_cancel t.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_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
neg : @vle _ inst _ (x * (↑v : R) * (↑t : R) * w) (z * (↑s : R) * (↑t : R) * w)
⊢ @vle _ inst _ (x * (↑v : R) * (↑t : R)) (z * (↑s : R) * (↑t : R))

Tactic:
apply vle_mul_cancel hw

Premises used: 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
⊢ x * (↑v : R) * (↑t : R) * w = x * (↑t : R) * (w * (↑v : R))

Tactic:
ring
-- 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
⊢ @vle _ inst _ (x * (↑t : R) * (w * (↑v : R))) (y * (↑s : R) * (z * (↑u : R)))

Tactic:
gcongr
-- 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
⊢ y * (↑s : R) * (z * (↑u : R)) = y * (↑u : R) * ((↑s : R) * z)

Tactic:
ring
-- 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
⊢ @vle _ inst _ (y * (↑u : R) * ((↑s : R) * z)) (w * (↑t : R) * ((↑s : R) * z))

Tactic:
gcongr
-- 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
⊢ w * (↑t : R) * ((↑s : R) * z) = z * (↑s : R) * (↑t : R) * w

Tactic:
ring
-- 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
calc : x * (↑v : R) * (↑t : R) * w = x * (↑t : R) * (w * (↑v : R))
calc₁ : @vle _ inst _ (x * (↑t : R) * (w * (↑v : R))) (y * (↑s : R) * (z * (↑u : R)))
calc₂ : y * (↑s : R) * (z * (↑u : R)) = y * (↑u : R) * ((↑s : R) * z)
calc₃ : @vle _ inst _ (y * (↑u : R) * ((↑s : R) * z)) (w * (↑t : R) * ((↑s : R) * z))
calc₄ : w * (↑t : R) * ((↑s : R) * z) = z * (↑s : R) * (↑t : R) * w
⊢ @vle _ inst _ (x * (↑v : R) * (↑t : R) * w) (z * (↑s : R) * (↑t : R) * w)

Tactic:
calc x * v * t * w
          _ = x * t * (w * v) := by ring
          _ ≤ᵥ y * s * (z * u) := by gcongr
          _ = y * u * (s * z) := by ring
          _ ≤ᵥ w * t * (s * z) := by gcongr
          _ = z * s * t * w := by ring

Premises used: HMul.hMul, Subtype.val
-- 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)
⊢ ValueGroupWithZero.mk x t ≤ ValueGroupWithZero.mk y s ↔ @vle _ inst _ (x * (↑s : R)) (y * (↑t : R))

Tactic:
Iff.rfl

Premises used: Iff.rfl, ValuativeRel.ValueGroupWithZero.lift₂
-- 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
hab : a ≤ b
hbc : b ≤ c
mk : ∀ (a₁ : R) (a₂ : ↥(posSubmonoid R)) (hab : ValueGroupWithZero.mk a₁ a₂ ≤ b), ValueGroupWithZero.mk a₁ a₂ ≤ c
⊢ a ≤ c

Tactic:
induction a using ValueGroupWithZero.ind with | mk a₁ a₂

Premises used: ValuativeRel.ValueGroupWithZero.ind, ValuativeRel.mk
-- 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
hbc : b ≤ c
a₁ : R
a₂ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk a₁ a₂ ≤ b
mk :
  ∀ (b₁ : R) (b₂ : ↥(posSubmonoid R)) (hbc : ValueGroupWithZero.mk b₁ b₂ ≤ c)
    (hab : ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk b₁ b₂), ValueGroupWithZero.mk a₁ a₂ ≤ c
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ c

Tactic:
induction b using ValueGroupWithZero.ind with | mk b₁ b₂

Premises used: ValuativeRel.ValueGroupWithZero.ind, ValuativeRel.mk
-- 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
a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b₁ b₂ ≤ c
hab : ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk b₁ b₂
mk :
  ∀ (c₁ : R) (c₂ : ↥(posSubmonoid R)) (hbc : ValueGroupWithZero.mk b₁ b₂ ≤ ValueGroupWithZero.mk c₁ c₂),
    ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk c₁ c₂
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ c

Tactic:
induction c using ValueGroupWithZero.ind with | mk c₁ c₂

Premises used: ValuativeRel.ValueGroupWithZero.ind, ValuativeRel.mk