awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
ι : Type u_3
I : ι → FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
i : ι
s : Finset ι
hi : i ∉ s
hrec : ∀ (hS : ∀ i ∈ s, I i ≠ 0), count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
hS : ∀ i_1 ∈ Insert.insert i s, I i_1 ≠ 0
hS' : ∀ i ∈ s, I i ≠ 0
hS0 : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (∏ i ∈ s, I i) 0
hi0 : I i ≠ 0
insert : count K v (I i * ∏ x ∈ s, I x) = ∑ i ∈ Insert.insert i s, count K v (I i)
⊢ count K v (∏ i ∈ Insert.insert i s, I i) = ∑ i ∈ Insert.insert i s, count K v (I i)
have insert₁ : count K v (I i * ∏ x ∈ s, I x) = count K v (I i) + ∑ x ∈ s, count K v (I x)
Tactic: rw [Finset.prod_insert hi, Finset.sum_insert hi, count_mul K v hi0 hS0, hrec hS']
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
ι : Type u_3
I : ι → FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
i : ι
s : Finset ι
hi : i ∉ s
hrec : ∀ (hS : ∀ i ∈ s, I i ≠ 0), count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
hS : ∀ i_1 ∈ Insert.insert i s, I i_1 ≠ 0
hS' : ∀ i ∈ s, I i ≠ 0
hS0 : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (∏ i ∈ s, I i) 0
hi0 : I i ≠ 0
insert : count K v (I i * ∏ x ∈ s, I x) = ∑ i ∈ Insert.insert i s, count K v (I i)
insert₁ : count K v (I i * ∏ x ∈ s, I x) = count K v (I i) + ∑ x ∈ s, count K v (I x)
⊢ count K v (∏ i ∈ Insert.insert i s, I i) = ∑ i ∈ Insert.insert i s, count K v (I i)
have insert₂ : count K v (I i) + count K v (∏ i ∈ s, I i) = count K v (I i) + ∑ x ∈ s, count K v (I x)
Tactic: rw [Finset.prod_insert hi, Finset.sum_insert hi, count_mul K v hi0 hS0, hrec hS']
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
ι : Type u_3
I : ι → FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
i : ι
s : Finset ι
hi : i ∉ s
hrec : ∀ (hS : ∀ i ∈ s, I i ≠ 0), count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
hS : ∀ i_1 ∈ Insert.insert i s, I i_1 ≠ 0
hS' : ∀ i ∈ s, I i ≠ 0
hS0 : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (∏ i ∈ s, I i) 0
hi0 : I i ≠ 0
insert : count K v (I i * ∏ x ∈ s, I x) = ∑ i ∈ Insert.insert i s, count K v (I i)
insert₁ : count K v (I i * ∏ x ∈ s, I x) = count K v (I i) + ∑ x ∈ s, count K v (I x)
insert₂ : count K v (I i) + count K v (∏ i ∈ s, I i) = count K v (I i) + ∑ x ∈ s, count K v (I x)
⊢ count K v (∏ i ∈ Insert.insert i s, I i) = ∑ i ∈ Insert.insert i s, count K v (I i)
have insert₃ : count K v (I i) + ∑ i ∈ s, count K v (I i) = count K v (I i) + ∑ x ∈ s, count K v (I x)
Tactic: rw [Finset.prod_insert hi, Finset.sum_insert hi, count_mul K v hi0 hS0, hrec hS']
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
ι : Type u_3
s : Finset ι
I : ι → FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hS : ∀ i ∈ s, I i ≠ 0
⊢ count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
have empty : ∀ (hS : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → I i ≠ 0), count K v (∏ i ∈ ∅, I i) = ∑ i ∈ ∅, count K v (I i)
Tactic: induction s using Finset.induction with
  | empty => rw [Finset.prod_empty, Finset.sum_empty, count_one]
  | insert i s hi hrec =>
    have hS' : ∀ i ∈ s, I i ≠ 0 := fun j hj => hS j (Finset.mem_insert_of_mem hj)
    have hS0 : ∏ i ∈ s, I i ≠ 0 := Finset.prod_ne_zero_iff.mpr hS'
    have hi0 : I i ≠ 0 := hS i (Finset.mem_insert_self i s)
    rw [Finset.prod_insert hi, Finset.sum_insert hi, count_mul K v hi0 hS0, hrec hS']
Cleared hypotheses: s, hS
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
ι : Type u_3
s : Finset ι
I : ι → FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hS : ∀ i ∈ s, I i ≠ 0
empty :
  ∀ (hS : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → I i ≠ 0), count K v (∏ i ∈ ∅, I i) = ∑ i ∈ ∅, count K v (I i)
⊢ count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (hrec : ∀ (hS : ∀ i ∈ s, I i ≠ 0), count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i))
  (hS : ∀ i_1 ∈ insert i s, I i_1 ≠ 0), count K v (∏ i ∈ insert i s, I i) = ∑ i ∈ insert i s, count K v (I i)
Tactic: induction s using Finset.induction with
  | empty => rw [Finset.prod_empty, Finset.sum_empty, count_one]
  | insert i s hi hrec =>
    have hS' : ∀ i ∈ s, I i ≠ 0 := fun j hj => hS j (Finset.mem_insert_of_mem hj)
    have hS0 : ∏ i ∈ s, I i ≠ 0 := Finset.prod_ne_zero_iff.mpr hS'
    have hi0 : I i ≠ 0 := hS i (Finset.mem_insert_self i s)
    rw [Finset.prod_insert hi, Finset.sum_insert hi, count_mul K v hi0 hS0, hrec hS']
Cleared hypotheses: s, hS
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
ι : Type u_3
s : Finset ι
I : ι → FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hS : ∀ i ∈ s, I i ≠ 0
⊢ count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
have empty : ∀ (hS : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → I i ≠ 0), count K v (∏ i ∈ ∅, I i) = ∑ i ∈ ∅, count K v (I i)
Tactic: classical
  induction s using Finset.induction with
  | empty => rw [Finset.prod_empty, Finset.sum_empty, count_one]
  | insert i s hi hrec =>
    have hS' : ∀ i ∈ s, I i ≠ 0 := fun j hj => hS j (Finset.mem_insert_of_mem hj)
    have hS0 : ∏ i ∈ s, I i ≠ 0 := Finset.prod_ne_zero_iff.mpr hS'
    have hi0 : I i ≠ 0 := hS i (Finset.mem_insert_self i s)
    rw [Finset.prod_insert hi, Finset.sum_insert hi, count_mul K v hi0 hS0, hrec hS']
Cleared hypotheses: s, hS
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
ι : Type u_3
s : Finset ι
I : ι → FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hS : ∀ i ∈ s, I i ≠ 0
empty :
  ∀ (hS : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → I i ≠ 0), count K v (∏ i ∈ ∅, I i) = ∑ i ∈ ∅, count K v (I i)
⊢ count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (hrec : ∀ (hS : ∀ i ∈ s, I i ≠ 0), count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i))
  (hS : ∀ i_1 ∈ insert i s, I i_1 ≠ 0), count K v (∏ i ∈ insert i s, I i) = ∑ i ∈ insert i s, count K v (I i)
Tactic: classical
  induction s using Finset.induction with
  | empty => rw [Finset.prod_empty, Finset.sum_empty, count_one]
  | insert i s hi hrec =>
    have hS' : ∀ i ∈ s, I i ≠ 0 := fun j hj => hS j (Finset.mem_insert_of_mem hj)
    have hS0 : ∏ i ∈ s, I i ≠ 0 := Finset.prod_ne_zero_iff.mpr hS'
    have hi0 : I i ≠ 0 := hS i (Finset.mem_insert_self i s)
    rw [Finset.prod_insert hi, Finset.sum_insert hi, count_mul K v hi0 hS0, hrec hS']
Cleared hypotheses: s, hS
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
⊢ count K v (HPow.hPow (β := ℕ) I 0) = (↑0 : ℤ) * count K v I
have zero : count K v 1 = (↑0 : ℤ) * count K v I
Tactic: rw [pow_zero, ofNat_zero, zero_mul, count_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
zero : count K v 1 = (↑0 : ℤ) * count K v I
⊢ count K v (HPow.hPow (β := ℕ) I 0) = (↑0 : ℤ) * count K v I
have zero₁ : count K v 1 = 0 * count K v I
Tactic: rw [pow_zero, ofNat_zero, zero_mul, count_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
zero : count K v 1 = (↑0 : ℤ) * count K v I
zero₁ : count K v 1 = 0 * count K v I
⊢ count K v (HPow.hPow (β := ℕ) I 0) = (↑0 : ℤ) * count K v I
have zero₂ : count K v 1 = 0
Tactic: rw [pow_zero, ofNat_zero, zero_mul, count_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
zero : count K v 1 = (↑0 : ℤ) * count K v I
zero₁ : count K v 1 = 0 * count K v I
zero₂ : count K v 1 = 0
⊢ count K v (HPow.hPow (β := ℕ) I 0) = (↑0 : ℤ) * count K v I
have zero₃ : Eq (α := ℤ) 0 0
Tactic: rw [pow_zero, ofNat_zero, zero_mul, count_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
⊢ count K v (I ^ (n + 1)) = (↑(n + 1) : ℤ) * count K v I
have succ : (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 [pow_succ, count_mul']
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
⊢ count K v (I ^ (n + 1)) = (↑(n + 1) : ℤ) * count K v I
have succ : (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: classical rw [pow_succ, count_mul']
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = (↑(n + 1) : ℤ) * count K v I
have pos : ∀ (hI : I = 0), (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: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
pos : ∀ (hI : I = 0), (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = (↑(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
have neg : ∀ (hI : ¬I = 0), (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: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
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
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = (↑(n + 1) : ℤ) * count K v I
have h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
Tactic: have h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0) := by order
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = (↑(n + 1) : ℤ) * count K v I
have pos : 0 = (↑(n + 1) : ℤ) * count K v I
Tactic: rw [if_neg h_neg, hI, count_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
pos : 0 = (↑(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
have pos₁ : 0 = (↑(n + 1) : ℤ) * count K v 0
Tactic: rw [if_neg h_neg, hI, count_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
pos : 0 = (↑(n + 1) : ℤ) * count K v I
pos₁ : 0 = (↑(n + 1) : ℤ) * count K v 0
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = (↑(n + 1) : ℤ) * count K v I
have pos₂ : 0 = HMul.hMul (α := ℤ) (↑(n + 1) : ℤ) 0
Tactic: rw [if_neg h_neg, hI, count_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
pos : 0 = (↑(n + 1) : ℤ) * count K v I
pos₁ : 0 = (↑(n + 1) : ℤ) * count K v 0
pos₂ : 0 = HMul.hMul (α := ℤ) (↑(n + 1) : ℤ) 0
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = (↑(n + 1) : ℤ) * count K v I
have pos₃ : Eq (α := ℤ) 0 0
Tactic: rw [if_neg h_neg, hI, count_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = (↑(n + 1) : ℤ) * count K v I
have neg : (↑n : ℤ) * count K v I + count K v I = HAdd.hAdd (α := ℤ) (↑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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
⊢ count K v (I ^ n) = (↑n : ℤ) * count K v I
have zero : count K v (HPow.hPow (β := ℕ) I 0) = (↑0 : ℤ) * 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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
⊢ count K v (I ^ n) = (↑n : ℤ) * count K v I
have 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
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have hv : 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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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)
have 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)
Tactic: rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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)
⊢ (↑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)
have 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)
Tactic: rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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)
⊢ (↑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)
have rw₂ : (↑v.asIdeal : FractionalIdeal R⁰ K) =
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 (↑v.asIdeal : FractionalIdeal R⁰ K)
Tactic: rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
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)
⊢ (↑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)
have rw₃ : Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
  (↑v.asIdeal : FractionalIdeal R⁰ K)
Tactic: rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have 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)
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]