awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Ideal R
hI : I ≠ 0
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)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) : ℤ))
    (∏ᶠ (a : HeightOneSpectrum R), (↑(a.maxPowDividing I) : FractionalIdeal R⁰ K))
⊢ 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 I))) : ℤ))
    (↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) : FractionalIdeal R⁰ K)

Tactic:
rw [FractionalIdeal.coeIdeal_finprod R⁰ K (le_refl _)]

Premises used: le_refl, nonZeroDivisors, FractionalIdeal.coeIdeal_finprod
-- 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 : Ideal R
hI : I ≠ 0
simp_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)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) : ℤ))
    (∏ᶠ (a : HeightOneSpectrum R),
      (↑(a.asIdeal ^ Associates.count (Associates.mk a.asIdeal) (Associates.factors (Associates.mk I))) :
        FractionalIdeal R⁰ K))
simp_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)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) : ℤ))
    (∏ᶠ (a : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑a.asIdeal : FractionalIdeal R⁰ K)
        (Associates.count (Associates.mk a.asIdeal) (Associates.factors (Associates.mk I))))
⊢ 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 I))) : ℤ))
    (∏ᶠ (a : HeightOneSpectrum R), (↑(a.maxPowDividing I) : FractionalIdeal R⁰ K))

Tactic:
simp_rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, FractionalIdeal.coeIdeal_pow,
    zpow_natCast]

Premises used: zpow_natCast, IsDedekindDomain.HeightOneSpectrum.maxPowDividing, FractionalIdeal.coeIdeal_pow
-- 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)
⊢ J ≠ 0

Tactic:
have hJ_ne_zero : J ≠ 0 := ideal_factor_ne_zero hI haJ
-- 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
⊢ 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)

Tactic:
have hJ := Ideal.finprod_heightOneSpectrum_factorization_coe K hJ_ne_zero
-- 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)
⊢ Ne (α := Ideal R) (span {a}) 0

Tactic:
have ha_ne_zero : Ideal.span {a} ≠ 0 := constant_factor_ne_zero hI haJ
-- 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
⊢ 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)

Tactic:
have ha := Ideal.finprod_heightOneSpectrum_factorization_coe K ha_ne_zero
-- 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)
rw :
  ∏ᶠ (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})))) : ℤ))⁻¹)
⊢ ∏ᶠ (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

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

Premises used: FractionalIdeal.coeIdeal_span_singleton, div_eq_mul_inv, FractionalIdeal.div_spanSingleton, finprod_inv_distrib
-- 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)
funProp : J ≠ 0
⊢ HasFiniteMulSupport.{u_1, u_2} (M := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) fun (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))) : ℤ)

Tactic:
fun_prop
-- 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)
funProp : Ne (α := Ideal R) (span {a}) 0
⊢ HasFiniteMulSupport.{u_1, u_2} (M := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) fun (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})))) : ℤ))

Tactic:
fun_prop
-- 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)
h :
  ∀ (x : HeightOneSpectrum R),
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
          (↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)) =
      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 J))) : ℤ) *
        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})))) : ℤ))
⊢ 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:
apply finprod_congr

Premises used: finprod_congr
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)

Tactic:
have hd_ne_zero : (algebraMap R K) (d : R) ≠ 0 :=
    map_ne_zero_of_mem_nonZeroDivisors _ (IsFractionRing.injective R K) d.property
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
rw :
  ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) n : K) (0 : K) ∧
    ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
⊢ Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0

Tactic:
rw [spanSingleton_ne_zero_iff, IsFractionRing.mk'_eq_div, ne_eq, div_eq_zero_iff, not_or]

Premises used: IsFractionRing.mk'_eq_div, FractionalIdeal.spanSingleton_ne_zero_iff, ne_eq, not_or, div_eq_zero_iff
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
⊢ ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) n : K) (0 : K) ∧
    ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)

Tactic:
⟨(map_ne_zero_iff (algebraMap R K) (IsFractionRing.injective R K)).mpr hn, hd_ne_zero⟩

Premises used: Iff.mpr, Algebra.algebraMap, IsFractionRing.injective, And.intro, map_ne_zero_iff
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
⊢ ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) n : K) (0 : K) ∧
    ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)

Tactic:
exact ⟨(map_ne_zero_iff (algebraMap R K) (IsFractionRing.injective R K)).mpr hn, hd_ne_zero⟩
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
⊢ Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0

Tactic:
have h0 : spanSingleton R⁰ (mk' K n d) ≠ 0 := by
    rw [spanSingleton_ne_zero_iff, IsFractionRing.mk'_eq_div, ne_eq, div_eq_zero_iff, not_or]
    exact ⟨(map_ne_zero_iff (algebraMap R K) (IsFractionRing.injective R K)).mpr hn, hd_ne_zero⟩
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
rw :
  Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d))
    (spanSingleton R⁰
      (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K)
        ((algebraMap R K : (a : R) → K) n : K)))
⊢ spanSingleton R⁰ (mk' K n d) =
    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) (↑d : R))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(Ideal.span {n}) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
rw [coeIdeal_span_singleton, spanSingleton_mul_spanSingleton]

Premises used: FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.spanSingleton_mul_spanSingleton
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
h :
  mk' K n d =
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
⊢ Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d))
    (spanSingleton R⁰
      (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K)
        ((algebraMap R K : (a : R) → K) n : K)))

Tactic:
apply congr_arg

Premises used: congr_arg
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
h :
  HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) =
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
h₁ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) =
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
h₂ h₃ :
  HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K) =
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
⊢ mk' K n d =
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)

Tactic:
rw [IsFractionRing.mk'_eq_div, div_eq_mul_inv, mul_comm]

Premises used: IsFractionRing.mk'_eq_div, div_eq_mul_inv, mul_comm
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
⊢ spanSingleton R⁰ (mk' K n d) =
    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) (↑d : R))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(Ideal.span {n}) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
have hI : spanSingleton R⁰ (mk' K n d) =
      spanSingleton R⁰ ((algebraMap R K) d)⁻¹ * ↑(Ideal.span {n} : Ideal R) := by
    rw [coeIdeal_span_singleton, spanSingleton_mul_spanSingleton]
    apply congr_arg
    rw [IsFractionRing.mk'_eq_div, div_eq_mul_inv, mul_comm]