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
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    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) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
⊢ Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)

Tactic:
have hv : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible
-- 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
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    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) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
⊢ Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)

Tactic:
apply w.associates_irreducible

Premises used: IsDedekindDomain.HeightOneSpectrum.associates_irreducible
-- 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
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    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) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
⊢ Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)

Tactic:
have hw' : Irreducible (Associates.mk w.asIdeal) := by apply w.associates_irreducible
-- 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
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    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) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
rw :
  ¬Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v.asIdeal) hv =
      Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk w.asIdeal) hw'
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0

Tactic:
rw [count_well_defined K v hw_ne_zero hw_fact, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero hv, ofNat_zero, sub_zero,
    natCast_eq_zero, ← pow_one (Associates.mk w.asIdeal), Associates.factors_prime_pow hw',
    Associates.count_some hv, Multiset.replicate_one, Multiset.count_eq_zero,
    Multiset.mem_singleton]

Premises used: Associates.mk, Ideal.one_eq_top, FractionalIdeal.count_well_defined, sub_zero, Ideal.span_singleton_one, Associates.count_some, Associates.count_zero, IsDedekindDomain.HeightOneSpectrum.asIdeal, Associates.mk_one, Associates.factors_prime_pow, Int.natCast_eq_zero, Int.ofNat_zero, Multiset.mem_singleton, pow_one, Multiset.count_eq_zero, Multiset.replicate_one, Associates.factors_one
-- 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
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    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) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
simp : ¬Eq (α := Associates (Ideal R)) (Associates.mk v.asIdeal) (Associates.mk w.asIdeal)
⊢ ¬Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v.asIdeal) hv =
      Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk w.asIdeal) hw'

Tactic:
simp only [Subtype.mk.injEq]

Premises used: Subtype.mk.injEq
-- 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
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    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) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
rw : ¬v = w
⊢ ¬Eq (α := Associates (Ideal R)) (Associates.mk v.asIdeal) (Associates.mk w.asIdeal)

Tactic:
rw [Associates.mk_eq_mk_iff_associated, associated_iff_eq, ← HeightOneSpectrum.ext_iff]

Premises used: Associates.mk_eq_mk_iff_associated, IsDedekindDomain.HeightOneSpectrum.ext_iff, associated_iff_eq
-- 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
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    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) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
⊢ ¬v = w

Tactic:
Ne.symm hw

Premises used: Ne.symm
-- 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
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    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) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
⊢ ¬v = w

Tactic:
exact Ne.symm hw

Premises used: Ne.symm
-- 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
v w : HeightOneSpectrum R
inst_5 : Decidable (w = v)
pos : ∀ (h : w = v), count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 1
neg : ∀ (h : ¬w = v), count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = if w = v then 1 else 0

Tactic:
split_ifs with h
-- 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
v w : HeightOneSpectrum R
inst_5 : Decidable (w = v)
h : w = v
pos : count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
pos₁ pos₂ : Eq (α := ℤ) 1 1
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 1

Tactic:
rw [h, count_self]

Premises used: FractionalIdeal.count_self
-- 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
v w : HeightOneSpectrum R
inst_5 : Decidable (w = v)
h : ¬w = v
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0

Tactic:
count_maximal_coprime K v h

Premises used: FractionalIdeal.count_maximal_coprime
-- 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
v w : HeightOneSpectrum R
inst_5 : Decidable (w = v)
h : ¬w = v
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0

Tactic:
exact count_maximal_coprime K v h

Premises used: FractionalIdeal.count_maximal_coprime
-- 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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
hp₀ : count K v 1 = 0
hp₁ : ∀ (x y : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0
hp₂ :
  ∀ (x : HeightOneSpectrum R),
    Membership.mem (γ := Set (HeightOneSpectrum R)) (fun (i : HeightOneSpectrum R) ↦ i = v → False) x →
      count K v
          (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x.asIdeal : FractionalIdeal R⁰ K) (exps x)) =
        0
⊢ count K v
      (∏ᶠ (w : HeightOneSpectrum R) (_ : w ≠ v),
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) (exps w)) =
    0

Tactic:
apply finprod_mem_induction fun I => count K v I = 0

Premises used: FractionalIdeal.count, OfNat.ofNat, Eq, finprod_mem_induction
-- 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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
⊢ count K v 1 = 0

Tactic:
count_one K v

Premises used: FractionalIdeal.count_one
-- 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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
⊢ count K v 1 = 0

Tactic:
exact count_one K v

Premises used: FractionalIdeal.count_one
-- 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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
pos : ∀ (h : I ≠ 0 ∧ I' ≠ 0), count K v (I * I') = 0
neg : ∀ (h : ¬(I ≠ 0 ∧ I' ≠ 0)), count K v (I * I') = 0
⊢ count K v (I * I') = 0

Tactic:
by_cases h : I ≠ 0 ∧ I' ≠ 0
-- 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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
pos : (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0
pos₁ : count K v I + count K v I' = 0
pos₂ : 0 + count K v I' = 0
pos₃ : HAdd.hAdd (α := ℤ) 0 0 = 0
pos₄ pos₅ : Eq (α := ℤ) 0 0
⊢ count K v (I * I') = 0

Tactic:
rw [count_mul' K v, if_pos h, hI, hI', add_zero]

Premises used: if_pos, FractionalIdeal.count_mul', add_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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : ¬(I ≠ 0 ∧ I' ≠ 0)
neg : (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0
neg₁ neg₂ : Eq (α := ℤ) 0 0
⊢ count K v (I * I') = 0

Tactic:
rw [count_mul' K v, if_neg h]

Premises used: FractionalIdeal.count_mul', if_neg
-- 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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
pos : ∀ (h : I ≠ 0 ∧ I' ≠ 0), count K v (I * I') = 0
neg neg₁ : ∀ (h : ¬(I ≠ 0 ∧ I' ≠ 0)), count K v (I * I') = 0
⊢ count K v (I * I') = 0

Tactic:
classical
    by_cases h : I ≠ 0 ∧ I' ≠ 0
    · rw [count_mul' K v, if_pos h, hI, hI', add_zero]
    · rw [count_mul' K v, if_neg h]

Premises used: FractionalIdeal.count_mul', add_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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
w : HeightOneSpectrum R
hw : Membership.mem (γ := Set (HeightOneSpectrum R)) (fun (i : HeightOneSpectrum R) ↦ i = v → False) w
hp₂ : exps w * count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
hp₃ : exps w * 0 = 0
hp₄ hp₅ : Eq (α := ℤ) 0 0
⊢ count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) (exps w)) = 0

Tactic:
rw [count_zpow, count_maximal_coprime K v hw, mul_zero]

Premises used: FractionalIdeal.count_maximal_coprime, MulZeroClass.mul_zero, FractionalIdeal.count_zpow
-- 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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
rw :
  Eq (α := ℤ)
    (∑ i ∈ exps.support,
        count K v
          (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
            ((exps : (a : HeightOneSpectrum R) → ℤ) i : ℤ)) :
      ℤ)
    ((exps : (a : HeightOneSpectrum R) → ℤ) v : ℤ)
hS :
  ∀ i ∈ exps.support,
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
        ((exps : (a : HeightOneSpectrum R) → ℤ) i : ℤ) ≠
      0
⊢ count K v
      (exps.prod fun (x1 : HeightOneSpectrum R) (x2 : ℤ) ↦
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x1.asIdeal : FractionalIdeal R⁰ K) x2) =
    (exps : (a : HeightOneSpectrum R) → ℤ) v

Tactic:
rw [Finsupp.prod, count_prod]

Premises used: FractionalIdeal.count_prod, Finsupp.prod
-- 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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ Eq (α := ℤ)
    (∑ i ∈ exps.support,
        count K v
          (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
            ((exps : (a : HeightOneSpectrum R) → ℤ) i : ℤ)) :
      ℤ)
    ((exps : (a : HeightOneSpectrum R) → ℤ) v : ℤ)

Tactic:
simp only [count_zpow, count_maximal, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq',
      exps.mem_support_iff, ne_eq, ite_not, ite_eq_right_iff, @eq_comm ℤ 0, imp_self]

Premises used: Finsupp.mem_support_iff, Finset.sum_ite_eq', mul_ite, eq_comm, ne_eq, MulZeroClass.mul_zero, ite_eq_right_iff, imp_self, ite_not, FractionalIdeal.count_zpow, mul_one, FractionalIdeal.count_maximal
-- 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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ Eq (α := ℤ)
    (∑ i ∈ exps.support,
        count K v
          (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
            ((exps : (a : HeightOneSpectrum R) → ℤ) i : ℤ)) :
      ℤ)
    ((exps : (a : HeightOneSpectrum R) → ℤ) v : ℤ)

Tactic:
classical simp only [count_zpow, count_maximal, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq',
      exps.mem_support_iff, ne_eq, ite_not, ite_eq_right_iff, @eq_comm ℤ 0, imp_self]

Premises used: Finsupp.mem_support_iff, Finset.sum_ite_eq', mul_ite, eq_comm, ne_eq, MulZeroClass.mul_zero, ite_eq_right_iff, imp_self, ite_not, FractionalIdeal.count_zpow, mul_one, FractionalIdeal.count_maximal
-- 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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ ∀ i ∈ exps.support,
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
        ((exps : (a : HeightOneSpectrum R) → ℤ) i : ℤ) ≠
      0

Tactic:
fun v hv ↦ zpow_ne_zero _ (coeIdeal_ne_zero.mpr v.ne_bot)

Premises used: Iff.mpr, IsDedekindDomain.HeightOneSpectrum.ne_bot, zpow_ne_zero, DFunLike.coe, FractionalIdeal.coeIdeal_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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ ∀ i ∈ exps.support,
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
        ((exps : (a : HeightOneSpectrum R) → ℤ) i : ℤ) ≠
      0

Tactic:
exact fun v hv ↦ zpow_ne_zero _ (coeIdeal_ne_zero.mpr v.ne_bot)

Premises used: zpow_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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ count K v
      (Finsupp.prod
        {
          support :=
            Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps,
          toFun := exps, mem_support_toFun := ⋯ : HeightOneSpectrum R →₀ ℤ }
        fun (x1 : HeightOneSpectrum R) (x2 : ℤ) ↦
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x1.asIdeal : FractionalIdeal R⁰ K) x2) =
    ({
          support :=
            Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps,
          toFun := exps, mem_support_toFun := ⋯ } :
        (a : HeightOneSpectrum R) → ℤ)
      v

Tactic:
count_finsuppProd K v (Finsupp.mk h_exps.toFinset exps (fun _ ↦ h_exps.mem_toFinset))

Premises used: FractionalIdeal.count_finsuppProd, Set.Finite.mem_toFinset, Finsupp.mk, Set.Finite.toFinset
-- 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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
h :
  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) (exps v))
    (Finsupp.prod
      {
        support :=
          Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps,
        toFun := exps, mem_support_toFun := ⋯ }
      fun (x1 : HeightOneSpectrum R) (x2 : ℤ) ↦
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x1.asIdeal : FractionalIdeal R⁰ K) x2)
⊢ count K v
      (∏ᶠ (v : HeightOneSpectrum R),
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) (exps v)) =
    exps v

Tactic:
convert! count_finsuppProd K v (Finsupp.mk h_exps.toFinset exps (fun _ ↦ h_exps.mem_toFinset))

Premises used: FractionalIdeal.count_finsuppProd, Set.Finite.mem_toFinset, Finsupp.mk, Set.Finite.toFinset