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 y : R
r s : ↥(posSubmonoid R)
simp :
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    Eq.{u_3 + 1} (α := ValueGroup₀ v)
      (if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ) then 0
      else
        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) → Γ) (↑r : R)) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v)))
      (if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ) then 0
      else
        HMul.hMul (α := ValueGroup₀ v) (β := 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))
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) (↑s : R)) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v)))
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    HMul.hMul (α := 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) (↑r : R) :
          ValueGroup₀ v) =
      HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) y : ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
          ValueGroup₀ v)

Tactic:
simp only [ValueGroup₀.restrict₀_apply, Valuation.apply_posSubmonoid_ne_zero, ↓reduceDIte,
        dite_mul, zero_mul]

Premises used: MulZeroClass.zero_mul, reduceDIte, dite_mul, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply, Valuation.apply_posSubmonoid_ne_zero
-- 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 y : R
r s : ↥(posSubmonoid R)
h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
h_1 : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    Eq.{u_3 + 1} (α := ValueGroup₀ v) 0 0

Tactic:
simp_all [← WithZero.coe_mul, ← Units.val_inj]

Premises used: Units.val_inj, WithZero.coe_mul
-- 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 y : R
r s : ↥(posSubmonoid R)
h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
h_1 : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    Eq.{u_3 + 1} (α := ValueGroup₀ v) 0 0

Tactic:
try simp_all [← WithZero.coe_mul, ← Units.val_inj]

Premises used: Units.val_inj, WithZero.coe_mul
-- 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 y : R
r s : ↥(posSubmonoid R)
h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
h_1 : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    0 =
      HMul.hMul (α := ValueGroup₀ v) (β := 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))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) (↑s : R)) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))

Tactic:
simp_all [← WithZero.coe_mul, ← Units.val_inj]

Premises used: Units.val_inj, WithZero.coe_mul
-- 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 y : R
r s : ↥(posSubmonoid R)
h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
h_1 : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    0 =
      HMul.hMul (α := ValueGroup₀ v) (β := 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))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) (↑s : R)) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))

Tactic:
try simp_all [← WithZero.coe_mul, ← Units.val_inj]

Premises used: Units.val_inj, WithZero.coe_mul
-- 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 y : R
r s : ↥(posSubmonoid R)
h : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
h_1 : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    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) → Γ) (↑r : R)) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) =
      0

Tactic:
simp_all [← WithZero.coe_mul, ← Units.val_inj]

Premises used: Units.val_inj, WithZero.coe_mul
-- 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 y : R
r s : ↥(posSubmonoid R)
h : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
h_1 : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    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) → Γ) (↑r : R)) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) =
      0

Tactic:
try simp_all [← WithZero.coe_mul, ← Units.val_inj]

Premises used: Units.val_inj, WithZero.coe_mul
-- 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 y : R
r s : ↥(posSubmonoid R)
h : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
h_1 : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    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) → Γ) (↑r : R)) ⋯) ⋯) :
            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) → Γ) y) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) (↑s : R)) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))

Tactic:
simp_all [← WithZero.coe_mul, ← Units.val_inj]

Premises used: Units.val_inj, WithZero.coe_mul
-- 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 y : R
r s : ↥(posSubmonoid R)
h : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)
h_1 : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    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) → Γ) (↑r : R)) ⋯) ⋯) :
            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) → Γ) y) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) (↑s : R)) ⋯) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))

Tactic:
try simp_all [← WithZero.coe_mul, ← Units.val_inj]

Premises used: Units.val_inj, WithZero.coe_mul
-- 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 y : R
r s : ↥(posSubmonoid R)
⊢ Ne.{u_3 + 1} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
      ValueGroup₀ v)
    (0 : ValueGroup₀ v)

Tactic:
simp [ValueGroup₀.restrict₀]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀
-- 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 y : R
r s : ↥(posSubmonoid R)
⊢ Ne.{u_3 + 1} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑r : R) :
      ValueGroup₀ v)
    (0 : ValueGroup₀ v)

Tactic:
simp [ValueGroup₀.restrict₀]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀
-- 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
⊢ ValueGroupWithZero.lift
      (fun (r : R) (s : ↥(posSubmonoid R)) ↦
        HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) r : ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
            ValueGroup₀ v))
      ⋯ 0 =
    0

Tactic:
simp [lift_zero, ValueGroup₀.restrict₀]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀, ValuativeRel.ValueGroupWithZero.lift_zero
-- 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
⊢ ValueGroupWithZero.lift
      (fun (r : R) (s : ↥(posSubmonoid R)) ↦
        HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) r : ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
            ValueGroup₀ v))
      ⋯ 1 =
    1

Tactic:
simp [ValueGroup₀.restrict₀]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀
-- 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 x_1 : ValueGroupWithZero R
hdist :
  ∀ (a b : R) (r s : ↥(posSubmonoid R)),
    HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (a * b) :
          ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑(r * s) : R) :
          ValueGroup₀ v) =
      HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a : ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑r : R) :
            ValueGroup₀ v) *
        HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) b : ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
            ValueGroup₀ v)
⊢ ValueGroupWithZero.lift
      (fun (r : R) (s : ↥(posSubmonoid R)) ↦
        HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) r : ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
            ValueGroup₀ v))
      ⋯ (x * x_1) =
    ValueGroupWithZero.lift
        (fun (r : R) (s : ↥(posSubmonoid R)) ↦
          HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
            (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) r :
              ValueGroup₀ v)
            (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
              ValueGroup₀ v))
        ⋯ x *
      ValueGroupWithZero.lift
        (fun (r : R) (s : ↥(posSubmonoid R)) ↦
          HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
            (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) r :
              ValueGroup₀ v)
            (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
              ValueGroup₀ v))
        ⋯ x_1

Tactic:
apply lift_mul

Premises used: ValuativeRel.ValueGroupWithZero.lift_mul
-- 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) (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:
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) (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)
        ((↑(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:
simp_all