awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have hv_irred : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
Tactic: have hv_irred : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible
-- 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
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)
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have 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
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]
-- 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have rw₁ : HSub.hSub (α := ℤ) (↑1 : ℤ)
    (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ) =
  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]
-- 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have rw₂ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ) =
  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]
-- 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have rw₃ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ) =
  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]
-- 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have rw₄ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ) = 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]
-- 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have rw₅ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ) = 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]
-- 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have rw₆ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑0 : ℤ) = 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]
-- 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have rw₇ : HSub.hSub (α := ℤ) (↑1 : ℤ) 0 = 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]
-- 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have rw₈ : Eq (α := ℤ) (↑1 : ℤ) 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]
-- 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have rw₉ : Eq (α := ℤ) 1 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]
-- 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
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)
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have 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
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]
-- 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have classical₁ : HSub.hSub (α := ℤ) (↑1 : ℤ)
    (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ) =
  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]
-- 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have classical₂ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ) =
  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]