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 : HeightOneSpectrum R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
n : ℕ
h : count K v (I ^ n) = (↑n : ℤ) * count K v I
hI : ¬I = 0
neg : (↑n : ℤ) * count K v I + count K v I = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * count K v I
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = (↑(n + 1) : ℤ) * count K v I

Tactic:
rw [if_pos (And.intro (pow_ne_zero n hI) hI), h, Nat.cast_add,
        Nat.cast_one]

Premises used: pow_ne_zero, if_pos, Nat.cast_add, And.intro, Nat.cast_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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
n : ℕ
h : count K v (I ^ n) = (↑n : ℤ) * count K v I
hI : ¬I = 0
⊢ (↑n : ℤ) * count K v I + count K v I = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * count K v I

Tactic:
ring
-- 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
n : ℕ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
zero : count K v (HPow.hPow (β := ℕ) I 0) = (↑0 : ℤ) * count K v I
succ :
  ∀ (n : ℕ) (h : count K v (I ^ n) = (↑n : ℤ) * count K v I), count K v (I ^ (n + 1)) = (↑(n + 1) : ℤ) * count K v I
⊢ count K v (I ^ n) = (↑n : ℤ) * count K v I

Tactic:
induction n with
  | zero => rw [pow_zero, ofNat_zero, zero_mul, count_one]
  | succ n h =>
    classical rw [pow_succ, count_mul']
    by_cases hI : I = 0
    · have h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0) := by order
      rw [if_neg h_neg, hI, count_zero, mul_zero]
    · rw [if_pos (And.intro (pow_ne_zero n hI) hI), h, Nat.cast_add,
        Nat.cast_one]
      ring

Premises used: pow_succ, MulZeroClass.zero_mul, pow_zero, MulZeroClass.mul_zero, Int.ofNat_zero, Nat.cast_add, FractionalIdeal.count_zero, FractionalIdeal.count_one, Int.succ, FractionalIdeal.count_mul', Nat.cast_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
⊢ Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) 0

Tactic:
have hv : (v.asIdeal : FractionalIdeal R⁰ K) ≠ 0 := coeIdeal_ne_zero.mpr v.ne_bot
-- 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
hv : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) 0
rw :
  (↑v.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ 1⁻¹) (↑v.asIdeal : FractionalIdeal R⁰ K)
rw₁ :
  (↑v.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ 1) (↑v.asIdeal : FractionalIdeal R⁰ K)
rw₂ :
  (↑v.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 (↑v.asIdeal : FractionalIdeal R⁰ K)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
    (↑v.asIdeal : FractionalIdeal R⁰ K)
⊢ (↑v.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)
      ((↑v.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]

Premises used: Algebra.algebraMap, inv_one, RingHom.map_one, FractionalIdeal.spanSingleton_one, one_mul
-- 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
hv : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) 0
⊢ (↑v.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)
      ((↑v.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
have h_self : (v.asIdeal : FractionalIdeal R⁰ K) =
      spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal := by
    rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]
-- 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
hv : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) 0
h_self :
  (↑v.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)
      ((↑v.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
⊢ Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)

Tactic:
apply v.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 : HeightOneSpectrum R
hv : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) 0
h_self :
  (↑v.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)
      ((↑v.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
⊢ Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)

Tactic:
have hv_irred : 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 : HeightOneSpectrum R
hv : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) 0
h_self :
  (↑v.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)
      ((↑v.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hv_irred : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
rw :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk v.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ) =
    1
rw₁ :
  HSub.hSub (α := ℤ) (↑1 : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ) =
    1
rw₂ :
  HSub.hSub (α := ℤ) (↑1 : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ) =
    1
rw₃ :
  HSub.hSub (α := ℤ) (↑1 : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ) =
    1
rw₄ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ) = 1
rw₅ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ) = 1
rw₆ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑0 : ℤ) = 1
rw₇ : HSub.hSub (α := ℤ) (↑1 : ℤ) 0 = 1
rw₈ : Eq (α := ℤ) (↑1 : ℤ) 1
rw₉ rw₁₀ : Eq (α := ℤ) 1 1
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1

Tactic:
rw [count_well_defined K v hv h_self, Associates.count_self hv_irred,
    Ideal.span_singleton_one, ← Ideal.one_eq_top, Associates.mk_one, Associates.factors_one,
    Associates.count_zero hv_irred, ofNat_zero, sub_zero, ofNat_one]

Premises used: Ideal.one_eq_top, FractionalIdeal.count_well_defined, sub_zero, Associates.count_self, Ideal.span_singleton_one, Associates.count_zero, Associates.mk_one, Int.ofNat_zero, Int.ofNat_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 : HeightOneSpectrum R
hv : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) 0
h_self :
  (↑v.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)
      ((↑v.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hv_irred : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
classical :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk v.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ) =
    1
classical₁ :
  HSub.hSub (α := ℤ) (↑1 : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ) =
    1
classical₂ :
  HSub.hSub (α := ℤ) (↑1 : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ) =
    1
classical₃ :
  HSub.hSub (α := ℤ) (↑1 : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ) =
    1
classical₄ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ) = 1
classical₅ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ) = 1
classical₆ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑0 : ℤ) = 1
classical₇ : HSub.hSub (α := ℤ) (↑1 : ℤ) 0 = 1
classical₈ : Eq (α := ℤ) (↑1 : ℤ) 1
classical₉ classical₁₀ : Eq (α := ℤ) 1 1
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1

Tactic:
classical rw [count_well_defined K v hv h_self, Associates.count_self hv_irred,
    Ideal.span_singleton_one, ← Ideal.one_eq_top, Associates.mk_one, Associates.factors_one,
    Associates.count_zero hv_irred, ofNat_zero, sub_zero, ofNat_one]

Premises used: Ideal.one_eq_top, FractionalIdeal.count_well_defined, sub_zero, Associates.count_self, Ideal.span_singleton_one, Associates.count_zero, Associates.mk_one, Int.ofNat_zero, Int.ofNat_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 : HeightOneSpectrum R
n : ℕ
rw : (↑n : ℤ) * count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = (↑n : ℤ)
rw₁ : HMul.hMul (α := ℤ) (↑n : ℤ) 1 = (↑n : ℤ)
rw₂ rw₃ : Eq (α := ℤ) (↑n : ℤ) (↑n : ℤ)
⊢ count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) n) = (↑n : ℤ)

Tactic:
rw [count_pow, count_self, mul_one]

Premises used: FractionalIdeal.count_pow, mul_one, 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 : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
pos : ∀ (hI : I = 0), count K v (I ^ (-n)) = -count K v (I ^ n)
neg : ∀ (hI : ¬I = 0), count K v (I ^ (-n)) = -count K v (I ^ n)
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

Tactic:
by_cases hI : 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
n : ℤ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I = 0
pos : ∀ (hn : n = 0), count K v (I ^ (-n)) = -count K v (I ^ n)
neg : ∀ (hn : ¬n = 0), count K v (I ^ (-n)) = -count K v (I ^ n)
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

Tactic:
by_cases hn : n = 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
n : ℤ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I = 0
hn : n = 0
pos : count K v (HPow.hPow (β := ℤ) I (-0)) = -count K v (HPow.hPow (β := ℤ) I 0)
pos₁ : count K v (HPow.hPow (β := ℤ) I 0) = -count K v (HPow.hPow (β := ℤ) I 0)
pos₂ : count K v 1 = -count K v 1
pos₃ : Eq (α := ℤ) 0 (-0)
pos₄ pos₅ : Eq (α := ℤ) 0 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

Tactic:
rw [hn, neg_zero, zpow_zero, count_one, neg_zero]

Premises used: zpow_zero, FractionalIdeal.count_one, neg_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
n : ℤ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I = 0
hn : ¬n = 0
neg :
  count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 0 (-n)) =
    -count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 0 n)
neg₁ : count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 0 (-n)) = -count K v 0
neg₂ : count K v 0 = -count K v 0
neg₃ : Eq (α := ℤ) 0 (-0)
neg₄ neg₅ : Eq (α := ℤ) 0 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

Tactic:
rw [hI, zero_zpow n hn, zero_zpow (-n) (neg_ne_zero.mpr hn), count_zero, neg_zero]

Premises used: Iff.mpr, zero_zpow, FractionalIdeal.count_zero, neg_ne_zero, neg_zero, Neg.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
n : ℤ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : ¬I = 0
neg : count K v 1 = 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

Tactic:
rw [eq_neg_iff_add_eq_zero, ← count_mul K v (zpow_ne_zero _ hI) (zpow_ne_zero _ hI),
      ← zpow_add₀ hI, neg_add_cancel, zpow_zero]

Premises used: zpow_zero, FractionalIdeal.count_mul, zpow_add₀, neg_add_cancel, zpow_ne_zero, eq_neg_iff_add_eq_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
n : ℤ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : ¬I = 0
⊢ 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
n : ℤ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : ¬I = 0
⊢ 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
rw : count K v (HPow.hPow (β := ℤ) I (-1)) = -count K v I
rw₁ : -count K v (HPow.hPow (β := ℤ) I 1) = -count K v I
rw₂ rw₃ : -count K v I = -count K v I
⊢ count K v I⁻¹ = -count K v I

Tactic:
rw [← zpow_neg_one, count_neg_zpow K v (1 : ℤ) I, zpow_one]

Premises used: zpow_neg_one, zpow_one, FractionalIdeal.count_neg_zpow, OfNat.ofNat
-- 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
n : ℤ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
ofNat : ∀ (n : ℕ), count K v (I ^ Int.ofNat n) = Int.ofNat n * count K v I
negSucc : ∀ (n : ℕ), count K v (I ^ -[n+1]) = -[n+1] * count K v I
⊢ count K v (I ^ n) = n * count K v I

Tactic:
obtain n | n := n
-- 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
n : ℕ
ofNat : count K v (I ^ n) = (↑n : ℤ) * count K v I
⊢ count K v (I ^ Int.ofNat n) = Int.ofNat n * count K v I

Tactic:
rw [ofNat_eq_natCast, zpow_natCast]

Premises used: zpow_natCast, Int.ofNat_eq_natCast
-- 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
n : ℕ
⊢ count K v (I ^ n) = (↑n : ℤ) * count K v I

Tactic:
count_pow K v n I

Premises used: FractionalIdeal.count_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
v : HeightOneSpectrum R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
n : ℕ
⊢ count K v (I ^ n) = (↑n : ℤ) * count K v I

Tactic:
exact count_pow K v n I

Premises used: FractionalIdeal.count_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
v : HeightOneSpectrum R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
n : ℕ
negSucc : -((↑n.succ : ℤ) * count K v I) = -(↑n.succ : ℤ) * count K v I
⊢ count K v (I ^ -[n+1]) = -[n+1] * count K v I

Tactic:
rw [negSucc_eq, count_neg_zpow, ← Int.natCast_succ, zpow_natCast, count_pow]

Premises used: zpow_natCast, FractionalIdeal.count_pow, Int.natCast_succ, FractionalIdeal.count_neg_zpow, Int.negSucc_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 : HeightOneSpectrum R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
n : ℕ
⊢ -((↑n.succ : ℤ) * count K v I) = -(↑n.succ : ℤ) * count K v I

Tactic:
ring
-- 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
n : ℤ
rw : n * count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = n
rw₁ : n * 1 = n
rw₂ rw₃ : n = n
⊢ count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) n) = n

Tactic:
rw [count_zpow, count_self, mul_one]

Premises used: FractionalIdeal.count_zpow, mul_one, 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
hw : w ≠ v
rw :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ 1⁻¹) (↑w.asIdeal : FractionalIdeal R⁰ K)
rw₁ :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ 1) (↑w.asIdeal : FractionalIdeal R⁰ K)
rw₂ :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 (↑w.asIdeal : FractionalIdeal R⁰ K)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K)
    (↑w.asIdeal : FractionalIdeal R⁰ K)
⊢ (↑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)

Tactic:
rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]

Premises used: Algebra.algebraMap, inv_one, RingHom.map_one, FractionalIdeal.spanSingleton_one, one_mul
-- 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
⊢ (↑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)

Tactic:
have hw_fact : (w.asIdeal : FractionalIdeal R⁰ K) =
      spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal := by
    rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]
-- 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)
⊢ Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0

Tactic:
have hw_ne_zero : (w.asIdeal : FractionalIdeal R⁰ K) ≠ 0 :=
    coeIdeal_ne_zero.mpr w.ne_bot
-- 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:
apply v.associates_irreducible

Premises used: IsDedekindDomain.HeightOneSpectrum.associates_irreducible