-- 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 ℤ))
⊢ (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₁ : ∀ (_ : 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 ℤ))
Tactic: split_ifs with _ _ b