-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ :
  I =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hJ_ne_zero : J ≠ 0
hJ :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ))
    (↑J : FractionalIdeal R⁰ K)
ha_ne_zero : Ne (α := Ideal R) (span {a}) 0
ha :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ))
    (↑(span {a}) : FractionalIdeal R⁰ K)
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (∏ᶠ (v : HeightOneSpectrum R),
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ))
      (∏ᶠ (x : HeightOneSpectrum R),
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑x.asIdeal : FractionalIdeal R⁰ K)
          (-(↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)))
have rw : Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (∏ᶠ (v : HeightOneSpectrum R),
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
      (HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)))
  (∏ᶠ (i : HeightOneSpectrum R),
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk i.asIdeal) (Associates.factors (Associates.mk J))) : ℤ) *
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
        (-(↑(Associates.count (Associates.mk i.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)))
Tactic: rw [← finprod_mul_distrib (by fun_prop) (by fun_prop)]