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 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
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
⊢ 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 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
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
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
rw₃ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 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) 0) : ℤ) =
  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
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
rw₃ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ) =
    0
rw₄ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ) =
    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))) : ℤ)
    (↑0 : ℤ) =
  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
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
rw₃ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ) =
    0
rw₄ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ) =
    0
rw₅ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑0 : ℤ) =
    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))) : ℤ)
    0 =
  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
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
rw₃ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ) =
    0
rw₄ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ) =
    0
rw₅ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑0 : ℤ) =
    0
rw₆ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      0 =
    0
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
have rw₇ : Eq (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ) 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
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
rw₃ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ) =
    0
rw₄ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ) =
    0
rw₅ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      (↑0 : ℤ) =
    0
rw₆ :
  HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ)
      0 =
    0
rw₇ : Eq (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal))) : ℤ) 0
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
have rw₈ : Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk w.asIdeal)) = 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
inst_5 : Decidable (w = v)
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = if w = v then 1 else 0
have pos : ∀ (h : w = v), count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 1
Tactic: split_ifs with h
-- 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
inst_5 : Decidable (w = v)
pos : ∀ (h : w = v), count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 1
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = if w = v then 1 else 0
have neg : ∀ (h : ¬w = v), count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
Tactic: split_ifs with h
-- 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
inst_5 : Decidable (w = v)
h : w = v
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 1
have pos : count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
Tactic: rw [h, count_self]
-- 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
inst_5 : Decidable (w = v)
h : w = v
pos : count K v (↑v.asIdeal : FractionalIdeal R⁰ K) = 1
⊢ count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 1
have pos₁ : Eq (α := ℤ) 1 1
Tactic: rw [h, count_self]
-- 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
exps : HeightOneSpectrum R → ℤ
⊢ count K v
      (∏ᶠ (w : HeightOneSpectrum R) (_ : w ≠ v),
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) (exps w)) =
    0
have hp₀ : count K v 1 = 0
Tactic: apply finprod_mem_induction fun I => count K v 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
exps : HeightOneSpectrum R → ℤ
hp₀ : count K v 1 = 0
⊢ count K v
      (∏ᶠ (w : HeightOneSpectrum R) (_ : w ≠ v),
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) (exps w)) =
    0
have hp₁ : ∀ (x y : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0
Tactic: apply finprod_mem_induction fun I => count K v 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
exps : HeightOneSpectrum R → ℤ
hp₀ : count K v 1 = 0
hp₁ : ∀ (x y : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0
⊢ count K v
      (∏ᶠ (w : HeightOneSpectrum R) (_ : w ≠ v),
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) (exps w)) =
    0
have hp₂ : ∀ (x : HeightOneSpectrum R),
  Membership.mem (γ := Set (HeightOneSpectrum R)) (fun (i : HeightOneSpectrum R) ↦ i = v → False) x →
    count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x.asIdeal : FractionalIdeal R⁰ K) (exps x)) =
      0
Tactic: apply finprod_mem_induction fun I => count K v 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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
⊢ count K v (I * I') = 0
have pos : ∀ (h : I ≠ 0 ∧ I' ≠ 0), count K v (I * I') = 0
Tactic: by_cases h : I ≠ 0 ∧ 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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
pos : ∀ (h : I ≠ 0 ∧ I' ≠ 0), count K v (I * I') = 0
⊢ count K v (I * I') = 0
have neg : ∀ (h : ¬(I ≠ 0 ∧ I' ≠ 0)), count K v (I * I') = 0
Tactic: by_cases h : I ≠ 0 ∧ 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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
⊢ count K v (I * I') = 0
have pos : (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0
Tactic: rw [count_mul' K v, if_pos h, hI, hI', add_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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
pos : (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0
⊢ count K v (I * I') = 0
have pos₁ : count K v I + count K v I' = 0
Tactic: rw [count_mul' K v, if_pos h, hI, hI', add_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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
pos : (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0
pos₁ : count K v I + count K v I' = 0
⊢ count K v (I * I') = 0
have pos₂ : 0 + count K v I' = 0
Tactic: rw [count_mul' K v, if_pos h, hI, hI', add_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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
pos : (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0
pos₁ : count K v I + count K v I' = 0
pos₂ : 0 + count K v I' = 0
⊢ count K v (I * I') = 0
have pos₃ : HAdd.hAdd (α := ℤ) 0 0 = 0
Tactic: rw [count_mul' K v, if_pos h, hI, hI', add_zero]