-- 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 a_1 : R) (b_1 : 0 <ᵥ a_1) (a_2 : R) (b_2 : 0 <ᵥ a_2),
    (if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) b : Γ) (0 : Γ) then 0
        else
          if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) a : Γ) (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) → Γ) a) ⋯) ⋯) :
                  WithZero ↥(valueGroup v)) :
                WithZero ↥(valueGroup v))
              ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                      (Units.mk0 ((v : (a : R) → Γ) b) ⋯) ⋯) :
                  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) → Γ) a_1) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v))
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) a_2) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v)) =
      HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          (if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) a : Γ) (0 : Γ) then 0
            else
              (↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                    (Units.mk0 ((v : (a : R) → Γ) a) h) ⋯) :
                WithZero ↥(valueGroup v)) :
            ValueGroup₀ v)
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) a_1) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v)) *
        HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          (if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) b : Γ) (0 : Γ) then 0
            else
              (↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                    (Units.mk0 ((v : (a : R) → Γ) b) h) ⋯) :
                WithZero ↥(valueGroup v)) :
            ValueGroup₀ v)
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) a_2) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v))
⊢ ∀ (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)

Tactic:
simp only [map_mul, ValueGroup₀.restrict₀_apply, mul_dite, mul_zero, dite_mul, zero_mul,
      Submonoid.coe_mul, Valuation.apply_posSubmonoid_ne_zero, ↓reduceDIte, Subtype.forall,
      posSubmonoid_def]

Premises used: MulZeroClass.zero_mul, reduceDIte, Subtype.forall, MulZeroClass.mul_zero, map_mul, dite_mul, ValuativeRel.posSubmonoid_def, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply, Valuation.apply_posSubmonoid_ne_zero, Submonoid.coe_mul, mul_dite