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 x' y y' : R
h1 : x =ᵥ y
h2 : x' =ᵥ y'
⊢ x * x' =ᵥ y * y'

Tactic:
⟨mul_vle_mul h1.vle h2.vle, mul_vle_mul h1.vge h2.vge⟩

Premises used: ValuativeRel.veq, ValuativeRel.veq.vge, ValuativeRel.veq.vle, And.intro, ValuativeRel.mul_vle_mul, AntisymmRel
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
⊢ @vle _ inst _ (x + y) x ∨ @vle _ inst _ (x + y) y

Tactic:
(vle_total y x).imp (fun h => vle_add .rfl h) (fun h => vle_add h .rfl)

Premises used: ValuativeRel.vle.rfl, ValuativeRel.vle_add, Or.imp, ValuativeRel.vle_total
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : 0 <ᵥ y
contrapose : ∀ (hy : ¬0 <ᵥ x * y), ¬0 <ᵥ y
⊢ 0 <ᵥ x * y

Tactic:
contrapose hy
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : ¬0 <ᵥ x * y
rw : ∀ (hy : @vle _ inst _ (x * y) 0), @vle _ inst _ y 0
⊢ ¬0 <ᵥ y

Tactic:
rw [not_vlt] at hy ⊢

Premises used: ValuativeRel.not_vlt
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : @vle _ inst _ (x * y) 0
⊢ 0 = x * 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : @vle _ inst _ (x * y) 0
⊢ @vle _ inst _ (y * x) (0 * x)

Tactic:
rw [show (0 : R) = x * 0 by simp, mul_comm x y, mul_comm x 0] at hy

Premises used: mul_comm, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : @vle _ inst _ (y * x) (0 * x)
⊢ @vle _ inst _ y 0

Tactic:
vle_mul_cancel hx hy

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 y : R
hx : 0 <ᵥ x
hy : @vle _ inst _ (y * x) (0 * x)
⊢ @vle _ inst _ y 0

Tactic:
exact vle_mul_cancel hx hy

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 : ↥(posSubmonoid R)
⊢ 0 <ᵥ (↑x : R)

Tactic:
x.prop

Premises used: ValuativeRel.vlt, Set.Mem, setOf, Subtype.prop, Not
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
⊢ Membership.mem (γ := Submonoid R) (posSubmonoid R) x ↔ 0 <ᵥ x

Tactic:
Iff.rfl

Premises used: ValuativeRel.vlt, Set.Mem, Iff.rfl, setOf, Not
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
u : ↥(posSubmonoid R)
⊢ @vle _ inst _ (x * (↑u : R)) (y * (↑u : R)) ↔ @vle _ inst _ x y

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
u : ↥(posSubmonoid R)
⊢ @vle _ inst _ ((↑u : R) * x) ((↑u : R) * y) ↔ @vle _ inst _ x y

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ Membership.mem (γ := Submonoid R) (posSubmonoid R) (↑x : R)

Tactic:
have := x.prop
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : ↥(posSubmonoid R)
this : Membership.mem (γ := Submonoid R) (posSubmonoid R) (↑x : R)
⊢ 0 <ᵥ (↑x : R)

Tactic:
rw [posSubmonoid_def] at this

Premises used: ValuativeRel.posSubmonoid_def
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : ↥(posSubmonoid R)
this : 0 <ᵥ (↑x : R)
contrapose : ∀ (this : (↑x : R) = 0), ¬0 <ᵥ (↑x : R)
⊢ (↑x : R) ≠ 0

Tactic:
contrapose this
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : ↥(posSubmonoid R)
this : (↑x : R) = 0
⊢ ¬0 <ᵥ (↑x : R)

Tactic:
simp [this]
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
left : @vle _ inst _ (r * (↑w : R)) (t * (↑u : R))
right : @vle _ inst _ (t * (↑u : R)) (r * (↑w : R))
⊢ match (motive := R × ↥(posSubmonoid R) → Prop) (r, u) with
  | (x, s) =>
    match (motive := R × ↥(posSubmonoid R) → Prop) (t, w) with
    | (y, t) => @vle _ inst _ (x * (↑t : R)) (y * (↑s : R)) ∧ @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
⊢ @vle _ inst _ (r * (↑v : R) * (↑w : R)) (s * (↑u : R) * (↑w : R))

Tactic:
have := mul_vle_mul h1 (vle_refl ↑w)
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (s * (↑u : R) * (↑w : R))
⊢ @vle _ inst _ (r * (↑v : R) * (↑w : R)) (s * (↑w : R) * (↑u : R))

Tactic:
rw [mul_right_comm s] at this

Premises used: mul_right_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (s * (↑w : R) * (↑u : R))
⊢ @vle _ inst _ (r * (↑v : R) * (↑w : R)) (t * (↑v : R) * (↑u : R))

Tactic:
have := vle_trans this (mul_vle_mul h3 (vle_refl _))
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this_1 : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (s * (↑w : R) * (↑u : R))
this : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (t * (↑v : R) * (↑u : R))
⊢ @vle _ inst _ (r * (↑w : R) * (↑v : R)) (t * (↑u : R) * (↑v : R))

Tactic:
rw [mul_right_comm r, mul_right_comm t] at this

Premises used: mul_right_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this_1 : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (s * (↑w : R) * (↑u : R))
this : @vle _ inst _ (r * (↑w : R) * (↑v : R)) (t * (↑u : R) * (↑v : R))
⊢ @vle _ inst _ (r * (↑w : R)) (t * (↑u : R))

Tactic:
simpa using this
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
⊢ @vle _ inst _ (t * (↑v : R) * (↑u : R)) (s * (↑w : R) * (↑u : R))

Tactic:
have := mul_vle_mul h4 (vle_refl ↑u)
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (s * (↑w : R) * (↑u : R))
⊢ @vle _ inst _ (t * (↑v : R) * (↑u : R)) (s * (↑u : R) * (↑w : R))

Tactic:
rw [mul_right_comm s] at this

Premises used: mul_right_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (s * (↑u : R) * (↑w : R))
⊢ @vle _ inst _ (t * (↑v : R) * (↑u : R)) (r * (↑v : R) * (↑w : R))

Tactic:
have := vle_trans this (mul_vle_mul h2 (vle_refl _))
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this_1 : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (s * (↑u : R) * (↑w : R))
this : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (r * (↑v : R) * (↑w : R))
⊢ @vle _ inst _ (t * (↑u : R) * (↑v : R)) (r * (↑w : R) * (↑v : R))

Tactic:
rw [mul_right_comm t, mul_right_comm r] at this

Premises used: mul_right_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this_1 : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (s * (↑u : R) * (↑w : R))
this : @vle _ inst _ (t * (↑u : R) * (↑v : R)) (r * (↑w : R) * (↑v : R))
⊢ @vle _ inst _ (t * (↑u : R)) (r * (↑w : R))

Tactic:
simpa using this
-- 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)
h₁ : @vle _ inst _ (x * (↑s : R)) (y * (↑t : R))
h₂ : @vle _ inst _ (y * (↑t : R)) (x * (↑s : R))
⊢ ValueGroupWithZero.mk x t = ValueGroupWithZero.mk y s

Tactic:
Quotient.sound ⟨h₁, h₂⟩

Premises used: And.intro, Quotient.sound, ValuativeRel.ValueGroupWithZero, ValuativeRel.ValueGroupWithZero.mk
-- 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)
h : ValueGroupWithZero.mk x t = ValueGroupWithZero.mk y s
⊢ @vle _ inst _ (x * (↑s : R)) (y * (↑t : R)) ∧ @vle _ inst _ (y * (↑t : R)) (x * (↑s : R))

Tactic:
Quotient.exact h

Premises used: Quotient.exact
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
motive : ValueGroupWithZero R → Prop
mk : ∀ (x : R) (y : ↥(posSubmonoid R)), motive (ValueGroupWithZero.mk x y)
t : ValueGroupWithZero R
⊢ motive t

Tactic:
Quotient.ind (fun (x, y) => mk x y) t

Premises used: Quotient.ind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
α : Sort u_2
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
x : R
y : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x y) = f x y

Tactic:
rfl

Premises used: ValuativeRel.ValueGroupWithZero.lift, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
α : Sort u_2
f : R → ↥(posSubmonoid R) → R → ↥(posSubmonoid R) → α
hf :
  ∀ (x y z w : R) (t s u v : ↥(posSubmonoid R)),
    @vle _ inst _ (x * (↑t : R)) (y * (↑s : R)) →
      @vle _ inst _ (y * (↑s : R)) (x * (↑t : R)) →
        @vle _ inst _ (z * (↑u : R)) (w * (↑v : R)) →
          @vle _ inst _ (w * (↑v : R)) (z * (↑u : R)) → f x s z v = f y t w u
x y : R
z w : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.lift₂ f hf (ValueGroupWithZero.mk x z) (ValueGroupWithZero.mk y w) = f x z y w

Tactic:
rfl

Premises used: ValuativeRel.ValueGroupWithZero.lift₂, rfl
-- 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)) ∧ @vle _ inst _ (y * (↑t : R)) (x * (↑s : R))

Tactic:
Quotient.eq

Premises used: Quotient.eq, ValuativeRel.ValueGroupWithZero, ValuativeRel.ValueGroupWithZero.mk
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
h : ValueGroupWithZero.mk x y = 0
⊢ @vle _ inst _ x 0

Tactic:
simpa using ValueGroupWithZero.mk_eq_mk.mp h

Premises used: ValuativeRel.ValueGroupWithZero.mk_eq_mk, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
h : @vle _ inst _ x 0
⊢ @vle _ inst _ (x * (↑1 : R)) (0 * (↑y : R))

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
h : @vle _ inst _ x 0
⊢ @vle _ inst _ (0 * (↑y : R)) (x * (↑1 : R))

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

Tactic:
(ValueGroupWithZero.mk_eq_zero 0 x).mpr .rfl

Premises used: Iff.mpr, ValuativeRel.vle.rfl, ValuativeRel.ValueGroupWithZero.mk_eq_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ @vle _ inst _ ((↑x : R) * (↑1 : R)) (1 * (↑x : R))

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ @vle _ inst _ (1 * (↑x : R)) ((↑x : R) * (↑1 : R))

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
⊢ @vle _ inst _ (HMul.hMul (α := R) 1 (↑1 : R)) (HMul.hMul (α := R) 1 (↑1 : R))

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x y = 1 ↔ @vle _ inst _ x (↑y : R) ∧ @vle _ inst _ (↑y : R) x

Tactic:
simp [← mk_one_one, mk_eq_mk]

Premises used: ValuativeRel.ValueGroupWithZero.mk_one_one, ValuativeRel.ValueGroupWithZero.mk_eq_mk
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
α : Sort u_2
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
⊢ ValueGroupWithZero.lift f hf 0 = f 0 1

Tactic:
rfl

Premises used: ValuativeRel.ValueGroupWithZero.lift, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
α : Sort u_2
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
⊢ ValueGroupWithZero.lift f hf 1 = f 1 1

Tactic:
rfl

Premises used: ValuativeRel.ValueGroupWithZero.lift, rfl
-- 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))
h₅ : @vle _ inst _ (x * z * (↑(t * u) : R)) (y * w * (↑(s * v) : R))
h₆ : @vle _ inst _ (y * w * (↑(s * v) : R)) (x * z * (↑(t * u) : R))
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (a : R) (b : ↥(posSubmonoid R)) (c : R) (d : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a * c) (b * d)) x s z
      v)
    ((fun (a : R) (b : ↥(posSubmonoid R)) (c : R) (d : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a * c) (b * d)) y t w
      u)

Tactic:
apply ValueGroupWithZero.sound

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

Tactic:
rw [Submonoid.coe_mul, Submonoid.coe_mul,
        mul_mul_mul_comm x, mul_mul_mul_comm y]

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

Tactic:
mul_vle_mul h₁ h₃

Premises used: ValuativeRel.mul_vle_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))
⊢ @vle _ inst _ (x * (↑t : R) * (z * (↑u : R))) (y * (↑s : R) * (w * (↑v : R)))

Tactic:
exact mul_vle_mul h₁ h₃

Premises used: ValuativeRel.mul_vle_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))
h₅ : @vle _ inst _ (y * (↑s : R) * (w * (↑v : R))) (x * (↑t : R) * (z * (↑u : R)))
⊢ @vle _ inst _ (y * w * (↑(s * v) : R)) (x * z * (↑(t * u) : R))

Tactic:
rw [Submonoid.coe_mul, Submonoid.coe_mul,
        mul_mul_mul_comm x, mul_mul_mul_comm y]

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

Tactic:
mul_vle_mul h₂ h₄

Premises used: ValuativeRel.mul_vle_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))
⊢ @vle _ inst _ (y * (↑s : R) * (w * (↑v : R))) (x * (↑t : R) * (z * (↑u : R)))

Tactic:
exact mul_vle_mul h₂ h₄

Premises used: ValuativeRel.mul_vle_mul
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
c d : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk a c * ValueGroupWithZero.mk b d = ValueGroupWithZero.mk (a * b) (c * d)

Tactic:
rfl

Premises used: ValuativeRel.ValueGroupWithZero.lift₂, rfl, ValuativeRel.ValueGroupWithZero.mk
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
a b : ValueGroupWithZero R
mk :
  ∀ (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
⊢ ValueGroupWithZero.lift f hf (a * b) = ValueGroupWithZero.lift f hf a * ValueGroupWithZero.lift f hf b

Tactic:
induction a using ValueGroupWithZero.ind

Premises used: ValuativeRel.ValueGroupWithZero.ind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
α : 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)
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)
⊢ ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x y * b) =
    ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x y) * ValueGroupWithZero.lift f hf b

Tactic:
induction b using ValueGroupWithZero.ind

Premises used: ValuativeRel.ValueGroupWithZero.ind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
α : 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
x : R
y : ↥(posSubmonoid R)
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:
simpa using hdist _ _ _ _