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
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
⊢ 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))) : ℤ) =
  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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have classical₄ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have classical₅ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ) = 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have classical₆ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑0 : ℤ) = 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have classical₇ : HSub.hSub (α := ℤ) (↑1 : ℤ) 0 = 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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have classical₈ : Eq (α := ℤ) (↑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
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
⊢ count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
have classical₉ : Eq (α := ℤ) 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
n : ℕ
⊢ count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) n) = (↑n : ℤ)
have rw : (↑n : ℤ) * count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = (↑n : ℤ)
Tactic: rw [count_pow, count_self, mul_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 : ℕ
rw : (↑n : ℤ) * count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = (↑n : ℤ)
⊢ count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) n) = (↑n : ℤ)
have rw₁ : HMul.hMul (α := ℤ) (↑n : ℤ) 1 = (↑n : ℤ)
Tactic: rw [count_pow, count_self, mul_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 : ℕ
rw : (↑n : ℤ) * count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = (↑n : ℤ)
rw₁ : HMul.hMul (α := ℤ) (↑n : ℤ) 1 = (↑n : ℤ)
⊢ count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) n) = (↑n : ℤ)
have rw₂ : Eq (α := ℤ) (↑n : ℤ) (↑n : ℤ)
Tactic: rw [count_pow, count_self, mul_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)) = -count K v (I ^ n)
have pos : ∀ (hI : I = 0), count K v (I ^ (-n)) = -count K v (I ^ n)
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
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)
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have neg : ∀ (hI : ¬I = 0), count K v (I ^ (-n)) = -count K v (I ^ n)
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
n : ℤ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I = 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have pos : ∀ (hn : n = 0), count K v (I ^ (-n)) = -count K v (I ^ n)
Tactic: by_cases hn : n = 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
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)
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have neg : ∀ (hn : ¬n = 0), count K v (I ^ (-n)) = -count K v (I ^ n)
Tactic: by_cases hn : n = 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
n : ℤ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I = 0
hn : n = 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have pos : count K v (HPow.hPow (β := ℤ) I (-0)) = -count K v (HPow.hPow (β := ℤ) I 0)
Tactic: rw [hn, neg_zero, zpow_zero, count_one, neg_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
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)
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have pos₁ : count K v (HPow.hPow (β := ℤ) I 0) = -count K v (HPow.hPow (β := ℤ) I 0)
Tactic: rw [hn, neg_zero, zpow_zero, count_one, neg_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
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)
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have pos₂ : count K v 1 = -count K v 1
Tactic: rw [hn, neg_zero, zpow_zero, count_one, neg_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
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
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have pos₃ : Eq (α := ℤ) 0 (-0)
Tactic: rw [hn, neg_zero, zpow_zero, count_one, neg_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
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)
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have pos₄ : Eq (α := ℤ) 0 0
Tactic: rw [hn, neg_zero, zpow_zero, count_one, neg_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
n : ℤ
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I = 0
hn : ¬n = 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have 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)
Tactic: rw [hI, zero_zpow n hn, zero_zpow (-n) (neg_ne_zero.mpr hn), count_zero, neg_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
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)
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have neg₁ : count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 0 (-n)) = -count K v 0
Tactic: rw [hI, zero_zpow n hn, zero_zpow (-n) (neg_ne_zero.mpr hn), count_zero, neg_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
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
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have neg₂ : count K v 0 = -count K v 0
Tactic: rw [hI, zero_zpow n hn, zero_zpow (-n) (neg_ne_zero.mpr hn), count_zero, neg_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
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
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)
have neg₃ : Eq (α := ℤ) 0 (-0)
Tactic: rw [hI, zero_zpow n hn, zero_zpow (-n) (neg_ne_zero.mpr hn), count_zero, neg_zero]