-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
h :
  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})))) : ℤ)) =
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
      (HAdd.hAdd (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)))
h₁ h₂ :
  HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
      (HAdd.hAdd (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ))) =
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
      (HAdd.hAdd (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)))
⊢ 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})))) : ℤ)) =
    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))) : ℤ) *
      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})))) : ℤ))

Tactic:
rw [← zpow_add₀ ((@coeIdeal_ne_zero R _ K _ _ _ _).mpr v.ne_bot), sub_eq_add_neg]

Premises used: Iff.mpr, sub_eq_add_neg, zpow_add₀, IsDedekindDomain.HeightOneSpectrum.ne_bot, FractionalIdeal.coeIdeal_ne_zero