-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Nontrivial R
x y : R
pos :
  ∀ (_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y))
    (_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x)
    (b : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y),
    ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        (ord R (x * y)) =
      HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
        (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦
              (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (ord R x) :
          WithZero (Multiplicative ℤ))
        (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦
              (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (ord R y) :
          WithZero (Multiplicative ℤ))
neg :
  ∀ (_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y))
    (_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x) (b : y ∉ nonZeroDivisors R),
    ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        (ord R (x * y)) =
      HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
        (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦
              (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (ord R x) :
          WithZero (Multiplicative ℤ))
        (0 : WithZero (Multiplicative ℤ))
pos₁ :
  ∀ (_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y)) (_ : x ∉ nonZeroDivisors R),
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y →
      ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (ord R (x * y)) =
        HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
          (0 : WithZero (Multiplicative ℤ))
          (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
              (fun (x : ℕ) ↦
                (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
              (ord R y) :
            WithZero (Multiplicative ℤ))
neg₁ :
  ∀ (_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y)) (_ : x ∉ nonZeroDivisors R),
    y ∉ nonZeroDivisors R →
      ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (ord R (x * y)) =
        HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
pos₂ :
  ∀ (_ : x * y ∉ nonZeroDivisors R),
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x →
      Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y →
        0 =
          HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
            (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
                (fun (x : ℕ) ↦
                  (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
                (ord R x) :
              WithZero (Multiplicative ℤ))
            (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
                (fun (x : ℕ) ↦
                  (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
                (ord R y) :
              WithZero (Multiplicative ℤ))
neg₂ :
  ∀ (_ : x * y ∉ nonZeroDivisors R),
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x →
      y ∉ nonZeroDivisors R →
        0 =
          HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
            (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
                (fun (x : ℕ) ↦
                  (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
                (ord R x) :
              WithZero (Multiplicative ℤ))
            (0 : WithZero (Multiplicative ℤ))
⊢ (if Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y) then
      ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        (ord R (x * y))
    else 0) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (if Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x then
          ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦
              (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (ord R x)
        else 0 :
        WithZero (Multiplicative ℤ))
      (if Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y then
          ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦
              (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (ord R y)
        else 0 :
        WithZero (Multiplicative ℤ))
have pos₃ : ∀ (_ : x * y ∉ nonZeroDivisors R),
  x ∉ nonZeroDivisors R →
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y →
      0 =
        HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
          (0 : WithZero (Multiplicative ℤ))
          (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
              (fun (x : ℕ) ↦
                (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
              (ord R y) :
            WithZero (Multiplicative ℤ))
Tactic: split_ifs with _ _ b