-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finprod_heightOneSpectrum_factorization_principal {I : FractionalIdeal R⁰ K} (hI : I ≠ 0)
    (k : K) (hk : I = spanSingleton R⁰ k) :
    ∏ᶠ v : HeightOneSpectrum R, (v.asIdeal : FractionalIdeal R⁰ K) ^
      ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose
          (mk'_surjective R⁰ k)} : Ideal R)).factors -
        (Associates.mk v.asIdeal).count (Associates.mk ((Ideal.span {(↑(choose
          (choose_spec (mk'_surjective R⁰ k)) : ↥R⁰) : R)}) : Ideal R)).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
k : K
hk : I = spanSingleton R⁰ k
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(choose ⋯)})).factors)) =
    I

Tactic:
set n : R := choose (mk'_surjective R⁰ k)

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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(choose ⋯)})).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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) =
    I

Tactic:
have hnd : mk' K n d = k := choose_spec (choose_spec (mk'_surjective R⁰ k))

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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) =
    I

Tactic:
have hn0 : n ≠ 0 := by
  by_contra h
  rw [← hnd, h, IsFractionRing.mk'_eq_div, _root_.map_zero,
    zero_div, spanSingleton_zero] at hk
  exact hI hk

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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
hn0 : n ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
⊢ n ≠ 0

Tactic:
by_contra 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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
h : n = 0
⊢ False

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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
h : n = 0
⊢ False

Tactic:
rw [← hnd, h, IsFractionRing.mk'_eq_div, _root_.map_zero,
  zero_div, spanSingleton_zero] at hk

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
k : K
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hk : I = 0
hnd : mk' K n d = k
h : n = 0
⊢ False

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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
hn0 : n ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) =
    I

Tactic:
rw [finprod_heightOneSpectrum_factorization_principal_fraction hn0 d, hk, hnd]

Result:
no goals

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

Tactic:
set d : ↥R⁰ := choose (choose_spec (mk'_surjective R⁰ k))

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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).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
k : K
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hk : I = 0
hnd : mk' K n d = k
h : n = 0
⊢ False

Tactic:
exact hI hk

Result:
no goals