-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finprod_heightOneSpectrum_factorization {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) {a : R}
    {J : Ideal R} (haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J) :
    ∏ᶠ v : HeightOneSpectrum R, (v.asIdeal : FractionalIdeal R⁰ K) ^
      ((Associates.mk v.asIdeal).count (Associates.mk J).factors -
        (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors : ℤ) = I

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑(Ideal.span {a})
⊢ ∀ (x : HeightOneSpectrum R),
    ↑x.asIdeal ^
        (↑((Associates.mk x.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
      ↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk J).factors) *
        ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {a})).factors))

Tactic:
intro v

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑(Ideal.span {a})
v : HeightOneSpectrum R
⊢ ↑v.asIdeal ^
      (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
    ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) *
      ↑v.asIdeal ^ (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors))

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑(Ideal.span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      ∏ᶠ (x : HeightOneSpectrum R),
        (↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {a})).factors))⁻¹

Tactic:
simp_rw [← zpow_neg]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑(Ideal.span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      ∏ᶠ (x : HeightOneSpectrum R),
        ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {a})).factors))

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
    I

Tactic:
have ha_ne_zero : Ideal.span {a} ≠ 0 := constant_factor_ne_zero hI haJ

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
    I

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑(Ideal.span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
    I

Tactic:
rw [haJ, ← div_spanSingleton, div_eq_mul_inv, ← coeIdeal_span_singleton, ← hJ, ← ha,
  ← finprod_inv_distrib]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑(Ideal.span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      ∏ᶠ (x : HeightOneSpectrum R),
        (↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {a})).factors))⁻¹