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
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)
⊢ 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]
-- 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 neg : count K v 1 = 0
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]
-- 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 I⁻¹ = -count K v I
have rw : count K v (HPow.hPow (β := ℤ) I (-1)) = -count K v I
Tactic: rw [← zpow_neg_one, count_neg_zpow K v (1 : ℤ) I, zpow_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
rw : count K v (HPow.hPow (β := ℤ) I (-1)) = -count K v I
⊢ count K v I⁻¹ = -count K v I
have rw₁ : -count K v (HPow.hPow (β := ℤ) I 1) = -count K v I
Tactic: rw [← zpow_neg_one, count_neg_zpow K v (1 : ℤ) I, zpow_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
rw : count K v (HPow.hPow (β := ℤ) I (-1)) = -count K v I
rw₁ : -count K v (HPow.hPow (β := ℤ) I 1) = -count K v I
⊢ count K v I⁻¹ = -count K v I
have rw₂ : -count K v I = -count K v I
Tactic: rw [← zpow_neg_one, count_neg_zpow K v (1 : ℤ) I, zpow_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 ofNat : ∀ (n : ℕ), count K v (I ^ ofNat n) = ofNat n * count K v I
Tactic: obtain n | n := n
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
ofNat : ∀ (n : ℕ), count K v (I ^ Int.ofNat n) = Int.ofNat n * count K v I
⊢ count K v (I ^ n) = n * count K v I
have negSucc : ∀ (n : ℕ), count K v (I ^ -[n+1]) = -[n+1] * count K v I
Tactic: obtain n | n := n
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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
n : ℕ
⊢ count K v (I ^ ofNat n) = ofNat n * count K v I
have ofNat : count K v (I ^ n) = (↑n : ℤ) * count K v I
Tactic: rw [ofNat_eq_natCast, zpow_natCast]
-- 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 : ℕ
⊢ count K v (I ^ -[n+1]) = -[n+1] * count K v I
have negSucc : -((↑n.succ : ℤ) * count K v I) = -(↑n.succ : ℤ) * count K v I
Tactic: rw [negSucc_eq, count_neg_zpow, ← Int.natCast_succ, zpow_natCast, count_pow]
-- 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_zpow, 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₁ : n * 1 = n
Tactic: rw [count_zpow, 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₁ : 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₂ : n = n
Tactic: rw [count_zpow, 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 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)
have 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)
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 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)
⊢ (↑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)
have 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)
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 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)
⊢ (↑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)
have rw₂ : (↑w.asIdeal : FractionalIdeal R⁰ K) =
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 (↑w.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 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)
⊢ (↑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)
have rw₃ : Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K)
  (↑w.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 w : HeightOneSpectrum R
hw : w ≠ v
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
have 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)
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]
-- 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 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)
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
have hw_ne_zero : 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
-- 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 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
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
have hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
Tactic: have hv : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible
-- 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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
have hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
Tactic: have hw' : Irreducible (Associates.mk w.asIdeal) := by apply w.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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
have rw : ¬Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v.asIdeal) hv =
    Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk w.asIdeal) hw'
Tactic: rw [count_well_defined K v hw_ne_zero hw_fact, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero hv, ofNat_zero, sub_zero,
    natCast_eq_zero, ← pow_one (Associates.mk w.asIdeal), Associates.factors_prime_pow hw',
    Associates.count_some hv, Multiset.replicate_one, Multiset.count_eq_zero,
    Multiset.mem_singleton]
-- 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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
⊢ ¬Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v.asIdeal) hv =
      Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk w.asIdeal) hw'
have simp : ¬Eq (α := Associates (Ideal R)) (Associates.mk v.asIdeal) (Associates.mk w.asIdeal)
Tactic: simp only [Subtype.mk.injEq]
-- 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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
⊢ ¬Eq (α := Associates (Ideal R)) (Associates.mk v.asIdeal) (Associates.mk w.asIdeal)
have rw : ¬v = w
Tactic: rw [Associates.mk_eq_mk_iff_associated, associated_iff_eq, ← HeightOneSpectrum.ext_iff]
-- 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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
have rw : HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
    (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ) =
  0
Tactic: classical
  rw [count_well_defined K v hw_ne_zero hw_fact, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero hv, ofNat_zero, sub_zero,
    natCast_eq_zero, ← pow_one (Associates.mk w.asIdeal), Associates.factors_prime_pow hw',
    Associates.count_some hv, Multiset.replicate_one, Multiset.count_eq_zero,
    Multiset.mem_singleton]
  simp only [Subtype.mk.injEq]
  rw [Associates.mk_eq_mk_iff_associated, associated_iff_eq, ← HeightOneSpectrum.ext_iff]
  exact Ne.symm hw
-- 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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
rw :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ) =
    0
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
have rw₁ : HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
    (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ) =
  0
Tactic: classical
  rw [count_well_defined K v hw_ne_zero hw_fact, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero hv, ofNat_zero, sub_zero,
    natCast_eq_zero, ← pow_one (Associates.mk w.asIdeal), Associates.factors_prime_pow hw',
    Associates.count_some hv, Multiset.replicate_one, Multiset.count_eq_zero,
    Multiset.mem_singleton]
  simp only [Subtype.mk.injEq]
  rw [Associates.mk_eq_mk_iff_associated, associated_iff_eq, ← HeightOneSpectrum.ext_iff]
  exact Ne.symm hw
-- 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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact :
  (↑w.asIdeal : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑w.asIdeal : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hw_ne_zero : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hw' : Irreducible (M := Associates (Ideal R)) (Associates.mk w.asIdeal)
rw :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ) =
    0
rw₁ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ) =
    0
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
have rw₂ : HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
    (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ) =
  0
Tactic: classical
  rw [count_well_defined K v hw_ne_zero hw_fact, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero hv, ofNat_zero, sub_zero,
    natCast_eq_zero, ← pow_one (Associates.mk w.asIdeal), Associates.factors_prime_pow hw',
    Associates.count_some hv, Multiset.replicate_one, Multiset.count_eq_zero,
    Multiset.mem_singleton]
  simp only [Subtype.mk.injEq]
  rw [Associates.mk_eq_mk_iff_associated, associated_iff_eq, ← HeightOneSpectrum.ext_iff]
  exact Ne.symm hw