-- 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)
pos :
  Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ) →
    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
neg :
  Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ) →
    ∀ (h : ¬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))
pos₁ :
  ∀ (h : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ)),
    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
neg₁ :
  ∀ (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))
⊢ 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)))

Tactic:
split_ifs