awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (↑s : 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
-- 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)
⊢ LT.lt.{u_3} (α := Γ) ((v : (a : R) → Γ) (a * (↑s : R)) : Γ) ((v : (a : R) → Γ) (b * (↑r : R)) : Γ)

Tactic:
rw [← map_mul, ← map_mul, (isEquiv (valuation R) v).lt_iff_lt] at h

Premises used: Valuation.IsEquiv.lt_iff_lt, map_mul, ValuativeRel.isEquiv, ValuativeRel.valuation
-- 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 : LT.lt.{u_3} (α := Γ) ((v : (a : R) → Γ) (a * (↑s : R)) : Γ) ((v : (a : R) → Γ) (b * (↑r : R)) : Γ)
simp :
  HMul.hMul (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
            ValueGroup₀ v) :
        Γ) <
    HMul.hMul (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) b :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑r : R) :
            ValueGroup₀ v) :
        Γ)
⊢ HMul.hMul (α := Γ) (β := Γ)
      ((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) a) :
            ValueGroup₀ v) :
        Γ)
      ((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) :
        Γ) <
    HMul.hMul (α := Γ) (β := Γ)
      ((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) b) :
            ValueGroup₀ v) :
        Γ)
      ((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 [embed, coe_mk, ZeroHom.coe_mk, lift_valuation,
      OneMemClass.coe_one, map_one, div_one]

Premises used: MonoidWithZeroHom.coe_mk, OneMemClass.coe_one, ValuativeRel.ValueGroupWithZero.embed, ZeroHom.coe_mk, map_one, ValuativeRel.ValueGroupWithZero.lift_valuation, div_one
-- 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 : LT.lt.{u_3} (α := Γ) ((v : (a : R) → Γ) (a * (↑s : R)) : Γ) ((v : (a : R) → Γ) (b * (↑r : R)) : Γ)
erw :
  HMul.hMul (α := Γ) (β := Γ) ((v.toMonoidWithZeroHom : (a : R) → Γ) a : Γ)
      ((v.toMonoidWithZeroHom : (a : R) → Γ) (↑s : R) : Γ) <
    HMul.hMul (α := Γ) (β := Γ) ((v.toMonoidWithZeroHom : (a : R) → Γ) b : Γ)
      ((v.toMonoidWithZeroHom : (a : R) → Γ) (↑r : R) : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
            ValueGroup₀ v) :
        Γ) <
    HMul.hMul (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) b :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑r : R) :
            ValueGroup₀ v) :
        Γ)

Tactic:
erw [embedding_restrict₀ a, embedding_restrict₀ b, embedding_restrict₀ r.1,
      embedding_restrict₀ s.1]

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀, Subtype.val
-- 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 : LT.lt.{u_3} (α := Γ) ((v : (a : R) → Γ) (a * (↑s : R)) : Γ) ((v : (a : R) → Γ) (b * (↑r : R)) : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v.toMonoidWithZeroHom : (a : R) → Γ) a : Γ)
      ((v.toMonoidWithZeroHom : (a : R) → Γ) (↑s : R) : Γ) <
    HMul.hMul (α := Γ) (β := Γ) ((v.toMonoidWithZeroHom : (a : R) → Γ) b : Γ)
      ((v.toMonoidWithZeroHom : (a : R) → Γ) (↑r : R) : Γ)

Tactic:
simpa using h
-- 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)
⊢ ¬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 : Γ)

Tactic:
simp [restrict₀_apply, embed]

Premises used: ValuativeRel.ValueGroupWithZero.embed, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- 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)
⊢ ¬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 : Γ)

Tactic:
simp [restrict₀_apply, embed]

Premises used: ValuativeRel.ValueGroupWithZero.embed, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- 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
Γ' : Type u_4
inst_4 : LinearOrderedCommGroupWithZero Γ'
w : Valuation R Γ'
inst_5 : w.Compatible
x : ValueGroupWithZero R
h : w.IsEquiv v
simp :
  (h.orderMonoidIso : (a : ValueGroup₀ w) → ValueGroup₀ v)
      (ValueGroupWithZero.lift
        (fun (r : R) (s : ↥(posSubmonoid R)) ↦
          HDiv.hDiv (α := ValueGroup₀ w) (β := ValueGroup₀ w)
            ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) r : ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ'))
            ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) (↑s : R) :
              ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ')))
        ⋯ x) =
    ValueGroupWithZero.lift
      (fun (r : R) (s : ↥(posSubmonoid R)) ↦
        HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) r : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ))
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) (↑s : R) : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ)))
      ⋯ x
⊢ Eq.{u_3 + 1} (α := ValueGroup₀ v)
    ((h.orderMonoidIso : (a : ValueGroup₀ w) → ValueGroup₀ v)
        (((embed w : MonoidWithZeroHom.{u_2, u_4} (ValueGroupWithZero R) (ValueGroup₀ w)) :
            (a : ValueGroupWithZero R) → ValueGroup₀ w)
          x) :
      ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        x :
      ValueGroup₀ v)

Tactic:
simp only [embed, ← Valuation.restrict_def, coe_mk, ZeroHom.coe_mk]

Premises used: MonoidWithZeroHom.coe_mk, ValuativeRel.ValueGroupWithZero.embed, ZeroHom.coe_mk, Valuation.restrict_def
-- 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
Γ' : Type u_4
inst_4 : LinearOrderedCommGroupWithZero Γ'
w : Valuation R Γ'
inst_5 : w.Compatible
h : w.IsEquiv v
r : R
s : ↥(posSubmonoid R)
⊢ (h.orderMonoidIso : (a : ValueGroup₀ w) → ValueGroup₀ v)
      (ValueGroupWithZero.lift
        (fun (r : R) (s : ↥(posSubmonoid R)) ↦
          HDiv.hDiv (α := ValueGroup₀ w) (β := ValueGroup₀ w)
            ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) r : ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ'))
            ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) (↑s : R) :
              ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ')))
        ⋯ (ValueGroupWithZero.mk r s)) =
    ValueGroupWithZero.lift
      (fun (r : R) (s : ↥(posSubmonoid R)) ↦
        HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) r : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ))
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) (↑s : R) : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ)))
      ⋯ (ValueGroupWithZero.mk r s)

Tactic:
simp
-- 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
Γ' : Type u_4
inst_4 : LinearOrderedCommGroupWithZero Γ'
w : Valuation R Γ'
inst_5 : w.Compatible
x : ValueGroupWithZero R
h : w.IsEquiv v
mk :
  ∀ (r : R) (s : ↥(posSubmonoid R)),
    (h.orderMonoidIso : (a : ValueGroup₀ w) → ValueGroup₀ v)
        (ValueGroupWithZero.lift
          (fun (r : R) (s : ↥(posSubmonoid R)) ↦
            HDiv.hDiv (α := ValueGroup₀ w) (β := ValueGroup₀ w)
              ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) r : ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ'))
              ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) (↑s : R) :
                ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ')))
          ⋯ (ValueGroupWithZero.mk r s)) =
      ValueGroupWithZero.lift
        (fun (r : R) (s : ↥(posSubmonoid R)) ↦
          HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) r : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) (↑s : R) : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ)))
        ⋯ (ValueGroupWithZero.mk r s)
⊢ (h.orderMonoidIso : (a : ValueGroup₀ w) → ValueGroup₀ v)
      (ValueGroupWithZero.lift
        (fun (r : R) (s : ↥(posSubmonoid R)) ↦
          HDiv.hDiv (α := ValueGroup₀ w) (β := ValueGroup₀ w)
            ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) r : ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ'))
            ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) (↑s : R) :
              ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ')))
        ⋯ x) =
    ValueGroupWithZero.lift
      (fun (r : R) (s : ↥(posSubmonoid R)) ↦
        HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) r : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ))
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) (↑s : R) : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ)))
      ⋯ x

Tactic:
induction x using ValueGroupWithZero.ind with
| mk r s =>
  simp

Premises used: ValuativeRel.ValueGroupWithZero.ind, ValuativeRel.mk
-- 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 : ValueGroupWithZero R
⊢ (fun (x : ValueGroup₀ v) ↦
        ((embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
            (((Valuation.IsEquiv.orderMonoidIso ⋯ :
                  OrderMonoidIso.{u_3, u_2} (ValueGroup₀ v)
                    (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))) :
                (a : ValueGroup₀ v) → ValueGroup₀ (valuation R))
              x) :
          ValueGroupWithZero R))
      (ZeroHom.toFun (↑(embed v) : ZeroHom (ValueGroupWithZero R) (ValueGroup₀ v)) x) =
    x

Tactic:
simp
-- 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
rw :
  Function.Injective (α := ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R)) (β :=
    ValueGroupWithZero R) (⇑embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
⊢ Function.Injective.{u_3 + 1, u_2 + 1} (β := ValueGroupWithZero R) fun (x : ValueGroup₀ v) ↦
    (embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
      (((Valuation.IsEquiv.orderMonoidIso ⋯ :
            OrderMonoidIso.{u_3, u_2} (ValueGroup₀ v)
              (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))) :
          (a : ValueGroup₀ v) → ValueGroup₀ (valuation R))
        x)

Tactic:
rw [← Function.comp_def, EquivLike.injective_comp]

Premises used: EquivLike.injective_comp, Function.comp_def
-- 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
⊢ Function.Injective (α := ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R)) (β :=
    ValueGroupWithZero R) (⇑embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)

Tactic:
embedding_strictMono.injective

Premises used: StrictMono.injective
-- 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
⊢ Function.Injective (α := ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R)) (β :=
    ValueGroupWithZero R) (⇑embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)

Tactic:
exact embedding_strictMono.injective

Premises used: StrictMono.injective
-- 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 : ValueGroupWithZero R
⊢ (embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
      (((Valuation.IsEquiv.orderMonoidIso ⋯ :
            OrderMonoidIso.{u_3, u_2} (ValueGroup₀ v)
              (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))) :
          (a : ValueGroup₀ v) → ValueGroup₀ (valuation R))
        (ZeroHom.toFun (↑(embed v) : ZeroHom (ValueGroupWithZero R) (ValueGroup₀ v)) x)) =
    x

Tactic:
simp
-- 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)
⊢ ((orderMonoidIso v : OrderMonoidIso.{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, Option.map₂
-- 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
⊢ Eq.{u_3 + 1} (α := ValueGroup₀ v)
    (((orderMonoidIso v : OrderMonoidIso.{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:
embed_valuation_eq_restrict₀ v x

Premises used: ValuativeRel.ValueGroupWithZero.lift, ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
γ : ValueGroupWithZero R
⊢ (embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
      ((orderMonoidIso (valuation R) : (a : ValueGroupWithZero R) → ValueGroup₀ (valuation R)) γ) =
    γ

Tactic:
embedding_embed_valuation_eq γ

Premises used: ValuativeRel.ValueGroupWithZero.lift, ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq
-- 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
⊢ StrictMono.{u_2, u_3} (α := ValueGroupWithZero R) (β := ValueGroup₀ v)
    (⇑(orderMonoidIso v) : (a : ValueGroupWithZero R) → ValueGroup₀ v)

Tactic:
embed_strictMono v

Premises used: ValuativeRel.ValueGroupWithZero.embed_strictMono, ValuativeRel.ValueGroupWithZero.lift
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
⊢ Function.LeftInverse (α := ValueGroupWithZero R) (β :=
    ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))
    (⇑embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
    (⇑(orderMonoidIso (valuation R)) : (a : ValueGroupWithZero R) → ValueGroup₀ (valuation R))

Tactic:
embedding_orderMonoidIso_valuation_eq

Premises used: Function.LeftInverse, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq
-- 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
γ : ValueGroup₀ v
x : R
⊢ LT.lt.{u_3} (α := ValueGroup₀ v)
      (((orderMonoidIso v : OrderMonoidIso.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
            (a : ValueGroupWithZero R) → ValueGroup₀ v)
          ((valuation R : (a : R) → ValueGroupWithZero R) x) :
        ValueGroup₀ v)
      (((orderMonoidIso v : OrderMonoidIso.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
            (a : ValueGroupWithZero R) → ValueGroup₀ v)
          (((OrderMonoidIso.symm (orderMonoidIso v) :
                OrderMonoidIso.{u_3, u_2} (ValueGroup₀ v) (ValueGroupWithZero R)) :
              (a : ValueGroup₀ v) → ValueGroupWithZero R)
            γ) :
        ValueGroup₀ v) ↔
    (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) x < γ

Tactic:
simp [v.restrict_def x]

Premises used: Valuation.restrict_def
-- 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
γ : ValueGroupWithZero R
x : R
⊢ LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) x : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ))
      (((orderMonoidIso v : OrderMonoidIso.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
            (a : ValueGroupWithZero R) → ValueGroup₀ v)
          γ :
        ValueGroup₀ v) ↔
    (valuation R : (a : R) → ValueGroupWithZero R) x < γ

Tactic:
simpa using (valuation_lt_symm_orderMonoidIso v (orderMonoidIso v γ) x).symm

Premises used: ValuativeRel.ValueGroupWithZero.orderMonoidIso, ValuativeRel.valuation_lt_symm_orderMonoidIso, DFunLike.coe, Iff.symm