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

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

Tactic:
simpa using vle_trans h₂ (mul_vle_mul_left hx t)

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 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))
hx : ¬@vle _ inst _ x 0
hy : @vle _ inst _ y 0
pos : @vle _ inst _ x 0
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)

Tactic:
absurd hx
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : ¬@vle _ inst _ x 0
hy : @vle _ inst _ y 0
pos : @vle _ inst _ (x * (↑t : R)) (0 * (↑t : R))
⊢ @vle _ inst _ x 0

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

Tactic:
simpa using vle_trans h₁ (mul_vle_mul_left hy s)

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 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))
hx : ¬@vle _ inst _ x 0
hy : ¬@vle _ inst _ y 0
neg :
  Eq (α := ValueGroupWithZero R)
    (ValueGroupWithZero.mk (↑s : R)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx))
    (ValueGroupWithZero.mk (↑t : R)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy))
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)

Tactic:
simp only [dif_neg hx, dif_neg hy]

Premises used: dif_neg
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : ¬@vle _ inst _ x 0
hy : ¬@vle _ inst _ y 0
neg :
  @vle _ inst _
    ((↑s : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy) : R))
    ((↑t : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx) : R))
neg₁ :
  @vle _ inst _
    ((↑t : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx) : R))
    ((↑s : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy) : R))
⊢ Eq (α := ValueGroupWithZero R)
    (ValueGroupWithZero.mk (↑s : R)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx))
    (ValueGroupWithZero.mk (↑t : R)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy))

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 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))
hx : ¬@vle _ inst _ x 0
hy : ¬@vle _ inst _ y 0
⊢ @vle _ inst _
    ((↑s : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy) : R))
    ((↑t : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx) : R))

Tactic:
simpa [mul_comm] using h₂

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : ¬@vle _ inst _ x 0
hy : ¬@vle _ inst _ y 0
⊢ @vle _ inst _
    ((↑t : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx) : R))
    ((↑s : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy) : R))

Tactic:
simpa [mul_comm] using h₁

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
hx : ¬@vle _ inst _ x 0
⊢ (ValueGroupWithZero.mk x y)⁻¹ =
    ValueGroupWithZero.mk (↑y : R)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx)

Tactic:
dif_neg hx

Premises used: ValuativeRel.ValueGroupWithZero.lift, dif_neg, dite
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 a : R
x : ↥(posSubmonoid R)
ha : 0 < ValueGroupWithZero.mk a x
b : R
y : ↥(posSubmonoid R)
c : R
z : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b y < ValueGroupWithZero.mk c z
⊢ ValueGroupWithZero.mk a x * ValueGroupWithZero.mk b y < ValueGroupWithZero.mk a x * ValueGroupWithZero.mk c z

Tactic:
simp_all [mul_mul_mul_comm _ _ (x : R)]

Premises used: mul_mul_mul_comm, Subtype.val
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
⊢ ∃ (x : ValueGroupWithZero R) (y : ValueGroupWithZero R), x ≠ y

Tactic:
⟨0, 1, fun h => ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
refine : ∀ (h : Eq.{u_1 + 1} (α := ValueGroupWithZero R) 0 1), False
⊢ ∃ (x : ValueGroupWithZero R) (y : ValueGroupWithZero R), x ≠ y

Tactic:
refine ⟨0, 1, fun h => ?_⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
h : Eq.{u_1 + 1} (α := ValueGroupWithZero R) 0 1
⊢ LE.le.{u_1} (α := ValueGroupWithZero R) 1 0

Tactic:
apply ge_of_eq at h

Premises used: ge_of_eq
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
h : LE.le.{u_1} (α := ValueGroupWithZero R) 1 0
⊢ @vle _ inst _ (HMul.hMul (α := R) 1 (↑1 : R)) (HMul.hMul (α := R) 0 (↑1 : R))

Tactic:
rw [← ValueGroupWithZero.mk_zero 1, ← ValueGroupWithZero.mk_one_one,
      ValueGroupWithZero.mk_le_mk] at h

Premises used: ValuativeRel.ValueGroupWithZero.mk_one_one, ValuativeRel.ValueGroupWithZero.mk_zero, ValuativeRel.ValueGroupWithZero.mk_le_mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
h : @vle _ inst _ (HMul.hMul (α := R) 1 (↑1 : R)) (HMul.hMul (α := R) 0 (↑1 : R))
⊢ False

Tactic:
simp [not_vle_one_zero] at h

Premises used: ValuativeRel.not_vle_one_zero
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x : R
y : ↥(posSubmonoid R)
h : ValueGroupWithZero.mk x y ≠ 0
⊢ ¬(@vle _ inst _ (x * (↑1 : R)) (0 * (↑y : R)) ∧ @vle _ inst _ (0 * (↑y : R)) (x * (↑1 : R)))

Tactic:
rw [ne_eq, ← ValueGroupWithZero.mk_zero 1, ValueGroupWithZero.mk_eq_mk] at h

Premises used: ValuativeRel.ValueGroupWithZero.mk_eq_mk, ne_eq, ValuativeRel.ValueGroupWithZero.mk_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x : R
y : ↥(posSubmonoid R)
h : ¬(@vle _ inst _ (x * (↑1 : R)) (0 * (↑y : R)) ∧ @vle _ inst _ (0 * (↑y : R)) (x * (↑1 : R)))
⊢ ¬@vle _ inst _ x 0

Tactic:
simp only [Submonoid.coe_one, mul_one, zero_mul, zero_vle, and_true] at h

Premises used: and_true, MulZeroClass.zero_mul, Submonoid.coe_one, ValuativeRel.zero_vle, mul_one
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x : R
y : ↥(posSubmonoid R)
h : ¬@vle _ inst _ x 0
rw :
  @vle _ inst _ (x * (↑y : R) * (↑1 : R))
      (1 * (↑(y * Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) : R)) ∧
    @vle _ inst _
      (1 * (↑(y * Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) : R))
      (x * (↑y : R) * (↑1 : R))
⊢ ValueGroupWithZero.mk x y * (ValueGroupWithZero.mk x y)⁻¹ = 1

Tactic:
rw [ValueGroupWithZero.inv_mk x y h, ← ValueGroupWithZero.mk_one_one,
      ValueGroupWithZero.mk_mul_mk, ValueGroupWithZero.mk_eq_mk]

Premises used: ValuativeRel.ValueGroupWithZero.mk_one_one, ValuativeRel.ValueGroupWithZero.inv_mk, ValuativeRel.ValueGroupWithZero.mk_eq_mk, ValuativeRel.ValueGroupWithZero.mk_mul_mk
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x : R
y : ↥(posSubmonoid R)
h : ¬@vle _ inst _ x 0
⊢ @vle _ inst _ (x * (↑y : R) * (↑1 : R))
      (1 * (↑(y * Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) : R)) ∧
    @vle _ inst _
      (1 * (↑(y * Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) : R))
      (x * (↑y : R) * (↑1 : R))

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z x_1 x_2 : R
⊢ ValueGroupWithZero.mk (x_1 * x_2) 1 =
    HMul.hMul (α := ValueGroupWithZero R) (ValueGroupWithZero.mk x_1 1) (ValueGroupWithZero.mk x_2 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
⊢ ∀ (x y : R),
    LE.le (α := ValueGroupWithZero R) (ValueGroupWithZero.mk (x + y) 1)
      (max (ValueGroupWithZero.mk x 1) (ValueGroupWithZero.mk y 1))

Tactic:
simp [vle_add_cases]

Premises used: ValuativeRel.vle_add_cases
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z x_1 x_2 : R
⊢ @vle _ inst _ x_1 x_2 ↔
    LE.le (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) x_1 : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) x_2 : ValueGroupWithZero R)

Tactic:
simp [valuation]

Premises used: ValuativeRel.valuation
-- 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
⊢ ValueGroupWithZero.lift f hf ((valuation R : (a : R) → ValueGroupWithZero R) x) = f x 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 : R
⊢ Eq (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)
      (0 : ValueGroupWithZero R) ↔
    @vle _ inst _ x 0

Tactic:
ValueGroupWithZero.mk_eq_zero _ _

Premises used: ValuativeRel.ValueGroupWithZero.mk_eq_zero, ValuativeRel.ValueGroupWithZero.mk
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : ↥(posSubmonoid R)
rw : ¬@vle _ inst _ (↑x : R) 0
⊢ Ne (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (↑x : R) : ValueGroupWithZero R)
    (0 : ValueGroupWithZero R)

Tactic:
rw [ne_eq, valuation_eq_zero_iff]

Premises used: ValuativeRel.valuation_eq_zero_iff, ne_eq
-- 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) 0

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 : ↥(posSubmonoid R)
⊢ ¬@vle _ inst _ (↑x : R) 0

Tactic:
exact x.prop

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
r : R
s : ↥(posSubmonoid R)
rw :
  HMul.hMul (β := ValueGroupWithZero R) (ValueGroupWithZero.mk r s)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) =
    (valuation R : (a : R) → ValueGroupWithZero R) r
⊢ ValueGroupWithZero.mk r s =
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) r : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)

Tactic:
rw [eq_div_iff (valuation_posSubmonoid_ne_zero _)]

Premises used: ValuativeRel.valuation_posSubmonoid_ne_zero, eq_div_iff
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
r : R
s : ↥(posSubmonoid R)
⊢ HMul.hMul (β := ValueGroupWithZero R) (ValueGroupWithZero.mk r s)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) =
    (valuation R : (a : R) → ValueGroupWithZero R) r

Tactic:
simp [valuation, mk_eq_mk]

Premises used: ValuativeRel.ValueGroupWithZero.mk_eq_mk, ValuativeRel.valuation
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
S : Type u_2
Γ : Type u_3
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x_1 y_1 : S
h_1 : LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) y_1 : Γ)
h : S
simp :
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) h : Γ) ≤
    HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) y_1 : Γ) ((v : (a : S) → Γ) h : Γ)
⊢ LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) (x_1 * h) : Γ) ((v : (a : S) → Γ) (y_1 * h) : Γ)

Tactic:
simp only [map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
S : Type u_2
Γ : Type u_3
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x_1 y_1 : S
h_1 : LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) y_1 : Γ)
h : S
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) h : Γ) ≤
    HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) y_1 : Γ) ((v : (a : S) → Γ) h : Γ)

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
S : Type u_2
Γ : Type u_3
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x_1 y_1 z_1 : S
h0 : ¬LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) z_1 : Γ) ((v : (a : S) → Γ) 0 : Γ)
h : LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) (x_1 * z_1) : Γ) ((v : (a : S) → Γ) (y_1 * z_1) : Γ)
⊢ ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : S) → Γ) z_1 : Γ) (0 : Γ)

Tactic:
rw [map_zero, le_zero_iff] at h0

Premises used: le_zero_iff, map_zero
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
S : Type u_2
Γ : Type u_3
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x_1 y_1 z_1 : S
h0 : ¬LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) z_1 : Γ) ((v : (a : S) → Γ) 0 : Γ)
h : LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) (x_1 * z_1) : Γ) ((v : (a : S) → Γ) (y_1 * z_1) : Γ)
h0₁ : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : S) → Γ) z_1 : Γ) (0 : Γ)
⊢ LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) (x_1 * z_1) : Γ) ((v : (a : S) → Γ) (y_1 * z_1) : Γ)

Tactic:
rw [map_zero, le_zero_iff] at h0

Premises used: le_zero_iff, map_zero
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
S : Type u_2
Γ : Type u_3
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x_1 y_1 z_1 : S
h0 : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : S) → Γ) z_1 : Γ) (0 : Γ)
h : LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) (x_1 * z_1) : Γ) ((v : (a : S) → Γ) (y_1 * z_1) : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) z_1 : Γ) ≤
    HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) y_1 : Γ) ((v : (a : S) → Γ) z_1 : Γ)

Tactic:
simp only [map_mul] at h

Premises used: map_mul
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
S : Type u_2
Γ : Type u_3
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x_1 y_1 z_1 : S
h0 : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : S) → Γ) z_1 : Γ) (0 : Γ)
h :
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) z_1 : Γ) ≤
    HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) y_1 : Γ) ((v : (a : S) → Γ) z_1 : Γ)
⊢ LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) y_1 : Γ)

Tactic:
le_of_mul_le_mul_right h (lt_of_le_of_ne' zero_le' h0)

Premises used: le_of_mul_le_mul_right, lt_of_le_of_ne', zero_le'
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
S : Type u_2
Γ : Type u_3
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x_1 y_1 z_1 : S
h0 : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : S) → Γ) z_1 : Γ) (0 : Γ)
h :
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) z_1 : Γ) ≤
    HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) y_1 : Γ) ((v : (a : S) → Γ) z_1 : Γ)
⊢ LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) y_1 : Γ)

Tactic:
exact le_of_mul_le_mul_right h (lt_of_le_of_ne' zero_le' h0)

Premises used: le_of_mul_le_mul_right, lt_of_le_of_ne', zero_le'
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
S : Type u_2
Γ : Type u_3
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
⊢ ¬LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) 1 : Γ) ((v : (a : S) → Γ) 0 : Γ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
S : Type u_2
Γ : Type u_3
inst : CommRing S
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
⊢ v.Compatible

Tactic:
letI := ValuativeRel.ofValuation v
  ⟨fun _ _ ↦ Iff.rfl⟩

Premises used: Valuation.Compatible.mk, Iff.rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_2 : LinearOrderedCommMonoidWithZero Γ₁
inst_3 : LinearOrderedCommMonoidWithZero Γ₂
v₁ : Valuation R Γ₁
v₂ : Valuation R Γ₂
inst_4 : v₁.Compatible
inst_5 : v₂.Compatible
x y : R
⊢ LE.le.{u_2} (α := Γ₁) ((v₁ : (a : R) → Γ₁) x : Γ₁) ((v₁ : (a : R) → Γ₁) y : Γ₁) ↔
    LE.le.{u_3} (α := Γ₂) ((v₂ : (a : R) → Γ₂) x : Γ₂) ((v₂ : (a : R) → Γ₂) y : Γ₂)

Tactic:
simp_rw [← Valuation.Compatible.vle_iff_le]

Premises used: Valuation.Compatible.vle_iff_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x y : R
⊢ @vle _ inst _ x y ↔ LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
Compatible.vle_iff_le _ _

Premises used: Valuation.Compatible.vle_iff_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x y : R
⊢ x <ᵥ y ↔ LT.lt.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simp [lt_iff_not_ge, ← Compatible.vle_iff_le]

Premises used: lt_iff_not_ge, Valuation.Compatible.vle_iff_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x y : R
simp_rw :
  @vle _ inst _ x y ∧ @vle _ inst _ y x ↔ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
simp_rw₁ :
  LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ∧
      LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ↔
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ x =ᵥ y ↔ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simp_rw [veq_def, vle_iff_le v, antisymm_iff]

Premises used: antisymm_iff, Valuation.vle_iff_le, ValuativeRel.veq_def
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
⊢ @vle _ inst _ x 1 ↔ LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
simp [v.vle_iff_le]

Premises used: Valuation.vle_iff_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
⊢ x <ᵥ 1 ↔ LT.lt.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
simp [v.vlt_iff_lt]

Premises used: Valuation.vlt_iff_lt
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
⊢ @vle _ inst _ 1 x ↔ LE.le.{u_2} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
simp [v.vle_iff_le]

Premises used: Valuation.vle_iff_le