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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ :
  I =
    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) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hJ_ne_zero : J ≠ 0
hJ :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ))
    (↑J : FractionalIdeal R⁰ K)
ha_ne_zero : Ne (α := Ideal R) (span {a}) 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)) =
    I
have ha : Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (∏ᶠ (v : HeightOneSpectrum R),
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ))
  (↑(span {a}) : FractionalIdeal R⁰ K)
Tactic: have ha := Ideal.finprod_heightOneSpectrum_factorization_coe K ha_ne_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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ :
  I =
    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) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hJ_ne_zero : J ≠ 0
hJ :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ))
    (↑J : FractionalIdeal R⁰ K)
ha_ne_zero : Ne (α := Ideal R) (span {a}) 0
ha :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ))
    (↑(span {a}) : FractionalIdeal R⁰ K)
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)) =
    I
have rw : ∏ᶠ (v : HeightOneSpectrum R),
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
      (HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)) =
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ))
    (∏ᶠ (x : HeightOneSpectrum R),
      (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑x.asIdeal : FractionalIdeal R⁰ K)
          (↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ))⁻¹)
Tactic: rw [haJ, ← div_spanSingleton, div_eq_mul_inv, ← coeIdeal_span_singleton, ← hJ, ← ha,
    ← finprod_inv_distrib]
-- 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ :
  I =
    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) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hJ_ne_zero : J ≠ 0
hJ :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ))
    (↑J : FractionalIdeal R⁰ K)
ha_ne_zero : Ne (α := Ideal R) (span {a}) 0
ha :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ))
    (↑(span {a}) : FractionalIdeal R⁰ K)
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)))
    (∏ᶠ (i : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
          (↑(Associates.count (Associates.mk i.asIdeal) (Associates.factors (Associates.mk J))) : ℤ) *
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
          (-(↑(Associates.count (Associates.mk i.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)))
have h : ∀ (x : HeightOneSpectrum R),
  HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x.asIdeal : FractionalIdeal R⁰ K)
      (HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
        (↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)) =
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑x.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk J))) : ℤ) *
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑x.asIdeal : FractionalIdeal R⁰ K)
        (-(↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ))
Tactic: apply finprod_congr
-- 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ :
  I =
    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) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hJ_ne_zero : J ≠ 0
hJ :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ))
    (↑J : FractionalIdeal R⁰ K)
ha_ne_zero : Ne (α := Ideal R) (span {a}) 0
ha :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ))
    (↑(span {a}) : FractionalIdeal R⁰ K)
v : HeightOneSpectrum R
⊢ HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
      (HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)) =
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ) *
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ))
have h : HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
    (HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)) =
  HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
    (HAdd.hAdd (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
      (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {a})))) : ℤ)))
Tactic: rw [← zpow_add₀ ((@coeIdeal_ne_zero R _ K _ _ _ _).mpr v.ne_bot), sub_eq_add_neg]
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
⊢ Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {n})))) : ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {(↑d : R)})))) :
            ℤ)))
    (spanSingleton R⁰ (mk' K n d))
have hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
Tactic: have hd_ne_zero : (algebraMap R K) (d : R) ≠ 0 :=
    map_ne_zero_of_mem_nonZeroDivisors _ (IsFractionRing.injective R K) d.property
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
⊢ Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
have rw : ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) n : K) (0 : K) ∧
  ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
Tactic: rw [spanSingleton_ne_zero_iff, IsFractionRing.mk'_eq_div, ne_eq, div_eq_zero_iff, not_or]
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
⊢ Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {n})))) : ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {(↑d : R)})))) :
            ℤ)))
    (spanSingleton R⁰ (mk' K n d))
have h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
Tactic: have h0 : spanSingleton R⁰ (mk' K n d) ≠ 0 := by
    rw [spanSingleton_ne_zero_iff, IsFractionRing.mk'_eq_div, ne_eq, div_eq_zero_iff, not_or]
    exact ⟨(map_ne_zero_iff (algebraMap R K) (IsFractionRing.injective R K)).mpr hn, hd_ne_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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
⊢ spanSingleton R⁰ (mk' K n d) =
    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) (↑d : R))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(Ideal.span {n}) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
have rw : Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d))
  (spanSingleton R⁰
    (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K)
      ((algebraMap R K : (a : R) → K) n : K)))
Tactic: rw [coeIdeal_span_singleton, spanSingleton_mul_spanSingleton]
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
⊢ Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d))
    (spanSingleton R⁰
      (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K)
        ((algebraMap R K : (a : R) → K) n : K)))
have h : mk' K n d =
  HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
Tactic: apply congr_arg
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
⊢ mk' K n d =
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
have h : HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) =
  HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
Tactic: rw [IsFractionRing.mk'_eq_div, div_eq_mul_inv, mul_comm]
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
h :
  HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) =
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
⊢ mk' K n d =
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
have h₁ : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) =
  HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
Tactic: rw [IsFractionRing.mk'_eq_div, div_eq_mul_inv, mul_comm]
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
h :
  HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) =
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
h₁ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) =
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
⊢ mk' K n d =
    HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
have h₂ : HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K) =
  HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) (↑d : R))⁻¹ : K) ((algebraMap R K : (a : R) → K) n : K)
Tactic: rw [IsFractionRing.mk'_eq_div, div_eq_mul_inv, mul_comm]
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
⊢ Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {n})))) : ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {(↑d : R)})))) :
            ℤ)))
    (spanSingleton R⁰ (mk' K n d))
have hI : spanSingleton R⁰ (mk' K n d) =
  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) (↑d : R))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    ((↑(Ideal.span {n}) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
Tactic: have hI : spanSingleton R⁰ (mk' K n d) =
      spanSingleton R⁰ ((algebraMap R K) d)⁻¹ * ↑(Ideal.span {n} : Ideal R) := by
    rw [coeIdeal_span_singleton, spanSingleton_mul_spanSingleton]
    apply congr_arg
    rw [IsFractionRing.mk'_eq_div, div_eq_mul_inv, mul_comm]
-- 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
k : K
hk : I = spanSingleton R⁰ k
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors
                  (Associates.mk
                    (Ideal.span {choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯})))) :
            ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {(↑d : R)})))) :
            ℤ)) =
    I
have hnd : mk' K n d = k
Tactic: have hnd : mk' K n d = k := choose_spec (choose_spec (exists_mk'_eq R⁰ k))
-- 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
k : K
hk : I = spanSingleton R⁰ k
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
hnd : mk' K n d = k
h : n = 0
⊢ False
have hk₁ : I = 0
Tactic: rw [← hnd, h, IsFractionRing.mk'_eq_div, map_zero, zero_div, spanSingleton_zero] at hk
Cleared hypotheses: hk, hnd, h
-- 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
k : K
hk : I = spanSingleton R⁰ k
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
hnd : mk' K n d = k
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors
                  (Associates.mk
                    (Ideal.span {choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯})))) :
            ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {(↑d : R)})))) :
            ℤ)) =
    I
have hn0 : n ≠ 0
Tactic: have hn0 : n ≠ 0 := by
    by_contra h
    rw [← hnd, h, IsFractionRing.mk'_eq_div, map_zero, zero_div, spanSingleton_zero] at hk
    exact hI hk