-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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})))) : ℤ)))
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})))) : ℤ)))
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})))) : ℤ))
neg₇ :
  exp
      (-(↑(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})))) :
          ℤ)) =
    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₈ neg₉ :
  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})))) : ℤ)) =
    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})))) : ℤ)))

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]

Premises used: WithZero.exp_add, Iff.mpr, neg_add, Associates.mk_ne_zero', Nat.cast_add, Ideal.span_singleton_mul_span_singleton, Associates.mk_mul_mk, Associates.count_mul, mul_ne_zero, if_neg, IsDedekindDomain.HeightOneSpectrum.associates_irreducible