awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
R : Type u_2
Γ : Type u_3
inst_2 : CommRing R
inst_3 : ValuativeRel R
inst_4 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_5 : v.Compatible
x_1 x_2 : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
h_1 : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
⊢ 0 /
      HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) z) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) w) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) =
    HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) x) h_1) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) z) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) *
      HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v) (0 : ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) w) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))

Tactic:
try simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
R : Type u_2
Γ : Type u_3
inst_2 : CommRing R
inst_3 : ValuativeRel R
inst_4 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_5 : v.Compatible
x_1 x_2 : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
h_1 : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
⊢ 0 /
      HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) z) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) w) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) =
    HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v) (0 : ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) z) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) *
      HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) y) h) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) w) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
R : Type u_2
Γ : Type u_3
inst_2 : CommRing R
inst_3 : ValuativeRel R
inst_4 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_5 : v.Compatible
x_1 x_2 : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
h_1 : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
⊢ 0 /
      HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) z) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) w) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) =
    HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v) (0 : ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) z) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) *
      HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) y) h) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) w) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))

Tactic:
try simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
R : Type u_2
Γ : Type u_3
inst_2 : CommRing R
inst_3 : ValuativeRel R
inst_4 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_5 : v.Compatible
x_1 x_2 : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
h_1 : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
⊢ HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) x) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) y) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) /
      HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) z) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) w) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) =
    HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) x) h_1) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) z) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) *
      HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) y) h) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) w) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))

Tactic:
simp [field, ← WithZero.coe_mul, ← Units.val_inj]

Premises used: Units.val_inj, WithZero.coe_mul
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
x : R
s : ↥(posSubmonoid R)
⊢ ((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
        (a : ValueGroupWithZero R) → ValueGroup₀ v)
      (ValueGroupWithZero.mk x s) =
    HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
      (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
      (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
        ValueGroup₀ v)

Tactic:
rfl

Premises used: Set.Mem, setOf, ValuativeRel.ValueGroupWithZero.lift, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
x : R
⊢ ((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
        (a : ValueGroupWithZero R) → ValueGroup₀ v)
      (ValueGroupWithZero.mk x 1) =
    HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
      (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
      (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑1 : R) :
        ValueGroup₀ v)

Tactic:
embed_mk v x 1

Premises used: ValuativeRel.ValueGroupWithZero.embed_mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
x : R
h :
  ((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x =
    HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
      (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
      (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑1 : R) :
        ValueGroup₀ v)
⊢ Eq.{u_3 + 1} (α := ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        ((valuation R : (a : R) → ValueGroupWithZero R) x) :
      ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)

Tactic:
convert! embed_mk v x 1

Premises used: ValuativeRel.ValueGroupWithZero.embed_mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
x : R
⊢ ((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x =
    HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
      (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
      (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑1 : R) :
        ValueGroup₀ v)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
γ : ValueGroupWithZero R
mk :
  ∀ (x : R) (y : ↥(posSubmonoid R)),
    (embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
        ((embed (valuation R) : (a : ValueGroupWithZero R) → ValueGroup₀ (valuation R)) (ValueGroupWithZero.mk x y)) =
      ValueGroupWithZero.mk x y
⊢ (embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
      ((embed (valuation R) : (a : ValueGroupWithZero R) → ValueGroup₀ (valuation R)) γ) =
    γ

Tactic:
induction γ using ValueGroupWithZero.ind

Premises used: ValuativeRel.ValueGroupWithZero.ind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
⊢ (embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
      ((embed (valuation R) : (a : ValueGroupWithZero R) → ValueGroup₀ (valuation R)) (ValueGroupWithZero.mk x y)) =
    ValueGroupWithZero.mk x y

Tactic:
simp [mk_eq_div]

Premises used: ValuativeRel.ValueGroupWithZero.mk_eq_div
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
a b : ValueGroupWithZero R
h : a < b
obtain :
  ∀ (a : R) (r : ↥(posSubmonoid R))
    (h :
      HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R) <
        b),
    LT.lt.{u_3} (α := ValueGroup₀ v)
      (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
            (a : ValueGroupWithZero R) → ValueGroup₀ v)
          (HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
            ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
            ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)) :
        ValueGroup₀ v)
      (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
            (a : ValueGroupWithZero R) → ValueGroup₀ v)
          b :
        ValueGroup₀ v)
⊢ LT.lt.{u_3} (α := ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        a :
      ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        b :
      ValueGroup₀ v)

Tactic:
obtain ⟨a, r, rfl⟩ := exists_valuation_div_valuation_eq a

Premises used: ValuativeRel.exists_valuation_div_valuation_eq, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
b : ValueGroupWithZero R
a : R
r : ↥(posSubmonoid R)
h :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R) <
    b
obtain :
  ∀ (b : R) (s : ↥(posSubmonoid R))
    (h :
      HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R) <
        HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)),
    LT.lt.{u_3} (α := ValueGroup₀ v)
      (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
            (a : ValueGroupWithZero R) → ValueGroup₀ v)
          (HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
            ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
            ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)) :
        ValueGroup₀ v)
      (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
            (a : ValueGroupWithZero R) → ValueGroup₀ v)
          (HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
            ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
            ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)) :
        ValueGroup₀ v)
⊢ LT.lt.{u_3} (α := ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        (HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)) :
      ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        b :
      ValueGroup₀ v)

Tactic:
obtain ⟨b, s, rfl⟩ := exists_valuation_div_valuation_eq b

Premises used: ValuativeRel.exists_valuation_div_valuation_eq, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R) <
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)
rw :
  LT.lt (α := Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
              (a : ValueGroupWithZero R) → ValueGroup₀ v)
            (HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
              ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
              ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)) :
          ValueGroup₀ v) :
      Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
              (a : ValueGroupWithZero R) → ValueGroup₀ v)
            (HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
              ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
              ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)) :
          ValueGroup₀ v) :
      Γ)
⊢ LT.lt.{u_3} (α := ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        (HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)) :
      ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        (HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)) :
      ValueGroup₀ v)

Tactic:
rw [← embedding_strictMono.lt_iff_lt]

Premises used: StrictMono.lt_iff_lt
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h :
  HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) <
    HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)
hb :
  ¬Eq (α := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R)) :
            ValueGroup₀ v) :
        Γ)
      (0 : Γ)
⊢ LT.lt (α := Γ) (0 : Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
              (a : ValueGroupWithZero R) → ValueGroup₀ v)
            ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R)) :
          ValueGroup₀ v) :
      Γ)

Tactic:
simp only [zero_lt_iff, ne_eq, Valuation.apply_posSubmonoid_ne_zero, not_false_eq_true]

Premises used: ne_eq, zero_lt_iff, not_false_eq_true, Valuation.apply_posSubmonoid_ne_zero
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h :
  HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) <
    HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)
hd :
  ¬Eq (α := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R)) :
            ValueGroup₀ v) :
        Γ)
      (0 : Γ)
⊢ LT.lt (α := Γ) (0 : Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
              (a : ValueGroupWithZero R) → ValueGroup₀ v)
            ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R)) :
          ValueGroup₀ v) :
      Γ)

Tactic:
simp only [zero_lt_iff, ne_eq, Valuation.apply_posSubmonoid_ne_zero, not_false_eq_true]

Premises used: ne_eq, zero_lt_iff, not_false_eq_true, Valuation.apply_posSubmonoid_ne_zero
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R) <
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)
⊢ LT.lt (α := ValueGroupWithZero R) (0 : ValueGroupWithZero R)
    ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)

Tactic:
simp only [zero_lt_iff, ne_eq, Valuation.apply_posSubmonoid_ne_zero, not_false_eq_true]

Premises used: ne_eq, zero_lt_iff, not_false_eq_true, Valuation.apply_posSubmonoid_ne_zero