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
α : Type u_2
inst_2 : Mul α
f : R → ↥(posSubmonoid R) → α
hf :
  ∀ (x y : R) (t s : ↥(posSubmonoid R)),
    @vle _ inst _ (x * (↑t : R)) (y * (↑s : R)) → @vle _ inst _ (y * (↑s : R)) (x * (↑t : R)) → f x s = f y t
hdist : ∀ (a b : R) (r s : ↥(posSubmonoid R)), f (a * b) (r * s) = f a r * f b s
b : ValueGroupWithZero R
x : R
y : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x y * b) =
    ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x y) * ValueGroupWithZero.lift f hf b
have mk : ∀ (x_1 : R) (y_1 : ↥(posSubmonoid R)),
  ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x y * ValueGroupWithZero.mk x_1 y_1) =
    ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x y) *
      ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x_1 y_1)
Tactic: induction b using ValueGroupWithZero.ind
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
a b c : ValueGroupWithZero R
⊢ a * b * c = a * (b * c)
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)), ValueGroupWithZero.mk x y * b * c = ValueGroupWithZero.mk x y * (b * c)
Tactic: induction a using ValueGroupWithZero.ind
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
b c : ValueGroupWithZero R
x_1 : R
y_1 : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x_1 y_1 * b * c = ValueGroupWithZero.mk x_1 y_1 * (b * c)
have 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)
Tactic: induction b using ValueGroupWithZero.ind
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
c : ValueGroupWithZero R
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 * c =
    ValueGroupWithZero.mk x_1 y_1 * (ValueGroupWithZero.mk x_2 y_2 * c)
have 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)
Tactic: induction c using ValueGroupWithZero.ind
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_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)
⊢ 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)
have succ : ValueGroupWithZero.mk (y ^ n) (t ^ n) * ValueGroupWithZero.mk x s =
  ValueGroupWithZero.mk (y ^ n) (t ^ n) * ValueGroupWithZero.mk y t
Tactic: simp only [pow_succ, ← ValueGroupWithZero.mk_mul_mk, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
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 (y ^ n) (t ^ n) * ValueGroupWithZero.mk x s =
    ValueGroupWithZero.mk (y ^ n) (t ^ n) * ValueGroupWithZero.mk y t
have succ : ValueGroupWithZero.mk x s = ValueGroupWithZero.mk y t
Tactic: apply congrArg (_ * ·)
-- 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 : 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))
⊢ 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)
have 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)
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₂
Cleared hypotheses: n
-- 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 : 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)
⊢ 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)
have 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)
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₂
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
a b : ValueGroupWithZero R
⊢ a * b = b * a
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)), ValueGroupWithZero.mk x y * b = b * ValueGroupWithZero.mk x y
Tactic: induction a using ValueGroupWithZero.ind
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
b : ValueGroupWithZero R
x_1 : R
y_1 : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x_1 y_1 * b = b * ValueGroupWithZero.mk x_1 y_1
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)),
  ValueGroupWithZero.mk x_1 y_1 * ValueGroupWithZero.mk x y = ValueGroupWithZero.mk x y * ValueGroupWithZero.mk x_1 y_1
Tactic: induction b using ValueGroupWithZero.ind
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_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))
⊢ 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 : ∀ (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)
Tactic: by_cases hw : w ≤ᵥ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_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)
⊢ 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 : ∀ (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)
Tactic: by_cases hw : w ≤ᵥ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_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
⊢ 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 : ∀ (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: by_cases hz : z ≤ᵥ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_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)
⊢ 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 : ∀ (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: by_cases hz : z ≤ᵥ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_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
⊢ 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 : ∀ (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: by_cases hz : z ≤ᵥ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_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)
⊢ 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 : ∀ (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: by_cases hz : z ≤ᵥ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_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 : ∀
  (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
Tactic: refine propext ⟨fun h => vle_trans ?_ (zero_vle _), fun h => vle_trans ?_ (zero_vle _)⟩
-- 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
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
⊢ 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₁ : ∀
  (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
Tactic: refine propext ⟨fun h => vle_trans ?_ (zero_vle _), fun h => vle_trans ?_ (zero_vle _)⟩
-- 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)) 0
have pos : @vle _ inst _ (y * (↑u : R) * (↑(s * v) : R)) (0 * (↑(s * v) : R))
Tactic: apply vle_mul_cancel (s * 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
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 * v) : R)) (0 * (↑(s * v) : R))
have pos : @vle _ inst _ (y * (↑s : R) * (↑v : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
Tactic: rw [mul_right_comm, Submonoid.coe_mul, ← mul_assoc]
-- 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 * (↑s : R) * (↑v : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
have pos : @vle _ inst _ (x * (↑t : R) * (↑v : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
Tactic: apply (mul_vle_mul_left (mul_vle_mul_left h₂ v) u).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))) x
    s z v
⊢ @vle _ inst _ (x * (↑t : R) * (↑v : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
have pos : @vle _ inst _ (x * (↑v : R) * (↑t : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
Tactic: rw [mul_right_comm x]
-- 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 _ (x * (↑v : R) * (↑t : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
have pos : @vle _ inst _ (z * (↑s : R) * (↑t : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
Tactic: apply (mul_vle_mul_left (mul_vle_mul_left h t) u).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))) x
    s z v
⊢ @vle _ inst _ (z * (↑s : R) * (↑t : R) * (↑u : R)) (0 * ((↑s : R) * (↑v : R)))
have pos : @vle _ inst _ (0 * (↑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)
-- 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)) 0
have pos : @vle _ inst _ (x * (↑v : R) * (↑(t * u) : R)) (0 * (↑(t * u) : R))
Tactic: apply vle_mul_cancel (t * 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
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 * u) : R)) (0 * (↑(t * u) : R))
have pos : @vle _ inst _ (x * (↑t : R) * (↑u : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
Tactic: rw [mul_right_comm, Submonoid.coe_mul, ← mul_assoc]
-- 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 * (↑t : R) * (↑u : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
have pos : @vle _ inst _ (y * (↑s : R) * (↑u : R) * (↑v : R)) (0 * ((↑t : R) * (↑u : R)))
Tactic: apply (mul_vle_mul_left (mul_vle_mul_left h₁ u) v).trans