-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finprod_heightOneSpectrum_factorization' {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) :
    ∏ᶠ v : HeightOneSpectrum R, (v.asIdeal : FractionalIdeal R⁰ K) ^ (count K v I) = 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
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I =
    ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors))

Tactic:
apply finprod_congr

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
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
⊢ ∀ (x : HeightOneSpectrum R),
    ↑x.asIdeal ^ count K x I =
      ↑x.asIdeal ^
        (↑((Associates.mk x.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
          ↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).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
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = I

Tactic:
conv_rhs => rw [← finprod_heightOneSpectrum_factorization hI h]

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
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I =
    ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors))

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
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
⊢ ∀ (x : HeightOneSpectrum R),
    ↑x.asIdeal ^ count K x I =
      ↑x.asIdeal ^
        (↑((Associates.mk x.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
          ↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors))

Tactic:
intro w

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
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
w : HeightOneSpectrum R
⊢ ↑w.asIdeal ^ count K w I =
    ↑w.asIdeal ^
      (↑((Associates.mk w.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
        ↑((Associates.mk w.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors))

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
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
w : HeightOneSpectrum R
⊢ ↑w.asIdeal ^ count K w I =
    ↑w.asIdeal ^
      (↑((Associates.mk w.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
        ↑((Associates.mk w.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors))

Tactic:
apply congr_arg

Result:
case h.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
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
w : HeightOneSpectrum R
⊢ count K w I =
    ↑((Associates.mk w.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
      ↑((Associates.mk w.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).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
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = I

Tactic:
have h := (Classical.choose_spec (Classical.choose_spec (exists_eq_spanSingleton_mul I))).2

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
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = I

Proof state:
case h.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
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
w : HeightOneSpectrum R
⊢ count K w I =
    ↑((Associates.mk w.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
      ↑((Associates.mk w.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors)

Tactic:
rw [count_ne_zero K w hI]

Result:
no goals