-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
neg :
  (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
neg₁ :
  (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
neg₂ :
  exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) : ℤ)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
neg₃ :
  exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) : ℤ)) =
    exp
      (HAdd.hAdd (α := ℤ)
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ))
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
neg₄ :
  exp
      (-(↑(Associates.count (Associates.mk v.asIdeal)
              (Associates.factors (Associates.mk (HMul.hMul (α := Ideal R) (Ideal.span {x}) (Ideal.span {y}))))) :
          ℤ)) =
    exp
      (HAdd.hAdd (α := ℤ)
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ))
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
⊢ (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
have neg₅ : exp
    (-(↑(Associates.count (Associates.mk v.asIdeal)
            (HMul.hMul (α := Associates (Ideal R)) (Associates.mk (Ideal.span {x}))
                (Associates.mk (Ideal.span {y}))).factors) :
        ℤ)) =
  exp
    (HAdd.hAdd (α := ℤ)
      (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ))
      (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
Tactic: rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← exp_add,
        ← Ideal.span_singleton_mul_span_singleton, ← Associates.mk_mul_mk, ← neg_add,
        Associates.count_mul (Associates.mk_ne_zero'.mpr hx) (Associates.mk_ne_zero'.mpr hy)
          v.associates_irreducible,
        Nat.cast_add]