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_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 * (↑s : R) * (↑u : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
have pos : @vle _ inst _ (y * (↑u : R) * (↑s : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
Tactic: rw [mul_right_comm y]
-- 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_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) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
have pos : @vle _ inst _ (w * (↑t : R) * (↑s : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
Tactic: apply (mul_vle_mul_left (mul_vle_mul_left h s) v).trans
-- 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_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 _ (w * (↑t : R) * (↑s : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
have pos : @vle _ inst _ (0 * (↑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)
-- 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_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)
have neg : @vle _ inst _ z 0
Tactic: absurd hz
-- 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_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 0
have neg : @vle _ inst _ (z * (↑u : R)) (0 * (↑u : R))
Tactic: apply vle_mul_cancel u.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_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)
have pos : @vle _ inst _ w 0
Tactic: absurd hw
-- 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_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 0
have pos : @vle _ inst _ (w * (↑v : R)) (0 * (↑v : R))
Tactic: apply vle_mul_cancel v.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_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)
have 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
Tactic: refine propext ⟨fun h => ?_, fun h => ?_⟩
-- 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_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
⊢ 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)
have 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
Tactic: refine propext ⟨fun h => ?_, fun h => ?_⟩
-- 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_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
⊢ (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) y
    t w u
have neg : @vle _ inst _ (y * (↑u : R) * (↑s : R)) (w * (↑t : R) * (↑s : R))
Tactic: apply vle_mul_cancel s.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_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 * (↑u : R) * (↑s : R)) (w * (↑t : R) * (↑s : R))
have neg : @vle _ inst _ (y * (↑u : R) * (↑s : R) * z) (w * (↑t : R) * (↑s : R) * z)
Tactic: apply vle_mul_cancel hz
-- 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_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 * (↑u : R) * (↑s : R) * z) (w * (↑t : R) * (↑s : R) * z)
have calc : y * (↑u : R) * (↑s : R) * z = y * (↑s : R) * (z * (↑u : R))
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
-- 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_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))
⊢ @vle _ inst _ (y * (↑u : R) * (↑s : R) * z) (w * (↑t : R) * (↑s : R) * z)
have calc₁ : @vle _ inst _ (y * (↑s : R) * (z * (↑u : R))) (x * (↑t : R) * (w * (↑v : R)))
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
-- 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_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)))
⊢ @vle _ inst _ (y * (↑u : R) * (↑s : R) * z) (w * (↑t : R) * (↑s : R) * z)
have calc₂ : x * (↑t : R) * (w * (↑v : R)) = x * (↑v : R) * ((↑t : R) * w)
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
-- 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_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)
⊢ @vle _ inst _ (y * (↑u : R) * (↑s : R) * z) (w * (↑t : R) * (↑s : R) * z)
have calc₃ : @vle _ inst _ (x * (↑v : R) * ((↑t : R) * w)) (z * (↑s : R) * ((↑t : R) * w))
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
-- 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_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))
⊢ @vle _ inst _ (y * (↑u : R) * (↑s : R) * z) (w * (↑t : R) * (↑s : R) * z)
have calc₄ : z * (↑s : R) * ((↑t : R) * w) = 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
-- 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_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
⊢ (fun (a : R) (s : ↥(posSubmonoid R)) (b : R) (t : ↥(posSubmonoid R)) ↦ @vle _ inst _ (a * (↑t : R)) (b * (↑s : R))) x
    s z v
have neg : @vle _ inst _ (x * (↑v : R) * (↑t : R)) (z * (↑s : R) * (↑t : R))
Tactic: apply vle_mul_cancel t.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_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 * (↑v : R) * (↑t : R)) (z * (↑s : R) * (↑t : R))
have neg : @vle _ inst _ (x * (↑v : R) * (↑t : R) * w) (z * (↑s : R) * (↑t : R) * w)
Tactic: apply vle_mul_cancel hw
-- 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_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 * (↑v : R) * (↑t : R) * w) (z * (↑s : R) * (↑t : R) * w)
have calc : x * (↑v : R) * (↑t : R) * w = x * (↑t : R) * (w * (↑v : R))
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
-- 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_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))
⊢ @vle _ inst _ (x * (↑v : R) * (↑t : R) * w) (z * (↑s : R) * (↑t : R) * w)
have calc₁ : @vle _ inst _ (x * (↑t : R) * (w * (↑v : R))) (y * (↑s : R) * (z * (↑u : R)))
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
-- 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_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)))
⊢ @vle _ inst _ (x * (↑v : R) * (↑t : R) * w) (z * (↑s : R) * (↑t : R) * w)
have calc₂ : y * (↑s : R) * (z * (↑u : R)) = y * (↑u : R) * ((↑s : R) * z)
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
-- 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_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)
⊢ @vle _ inst _ (x * (↑v : R) * (↑t : R) * w) (z * (↑s : R) * (↑t : R) * w)
have calc₃ : @vle _ inst _ (y * (↑u : R) * ((↑s : R) * z)) (w * (↑t : R) * ((↑s : R) * z))
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
-- 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_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))
⊢ @vle _ inst _ (x * (↑v : R) * (↑t : R) * w) (z * (↑s : R) * (↑t : R) * w)
have calc₄ : w * (↑t : R) * ((↑s : R) * z) = 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
-- 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 c : ValueGroupWithZero R
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c
have mk : ∀ (a₁ : R) (a₂ : ↥(posSubmonoid R)) (hab : ValueGroupWithZero.mk a₁ a₂ ≤ b), ValueGroupWithZero.mk a₁ a₂ ≤ c
Tactic: induction a using ValueGroupWithZero.ind with | mk a₁ a₂
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
hbc : b ≤ c
a₁ : R
a₂ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk a₁ a₂ ≤ b
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ c
have 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
Tactic: induction b using ValueGroupWithZero.ind with | mk b₁ b₂
Cleared hypotheses: b, hbc, 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
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₂
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ c
have mk : ∀ (c₁ : R) (c₂ : ↥(posSubmonoid R)) (hbc : ValueGroupWithZero.mk b₁ b₂ ≤ ValueGroupWithZero.mk c₁ c₂),
  ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk c₁ c₂
Tactic: induction c using ValueGroupWithZero.ind with | mk c₁ c₂
Cleared hypotheses: c, hbc
-- 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 : ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk b₁ b₂
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b₁ b₂ ≤ ValueGroupWithZero.mk c₁ c₂
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk c₁ c₂
have 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))
Tactic: rw [ValueGroupWithZero.mk_le_mk] at hab hbc ⊢
Cleared hypotheses: hab, c₁, c₂, hbc