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
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
ha : Ne.{u_1 + 1} (α := Associates (Ideal R)) (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)) 0
hb : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
h :
  ∀ (p : Associates (Ideal R)),
    Irreducible p →
      p.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
        p.count (Associates.factors (Associates.mk I))
hb₁ : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
h₁ h₂ h₃ :
  ∀ (v : Associates (Ideal R)) (hv : Irreducible v),
    v.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
      v.count (Associates.factors (Associates.mk I))
h₄ :
  ∀ (v : Associates (Ideal R)) (hv : Irreducible v) (J : Ideal R) (hJv : Associates.mk J = v),
    v.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
      v.count (Associates.factors (Associates.mk I))
h₅ :
  ∀ (v : Associates (Ideal R)) (J : Ideal R) (hv : Irreducible J) (hJv : Associates.mk J = v),
    v.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
      v.count (Associates.factors (Associates.mk I))
⊢ Eq (α := Associates (Ideal R)) (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)) (Associates.mk I)
have h₆ : ∀ (v : Associates (Ideal R)) (J : Ideal R) (hv : Irreducible J) (hJv : Associates.mk J = v),
  Associates.count (Associates.mk J)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
    Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))
Tactic: classical
  apply Associates.eq_of_eq_counts
  · apply Associates.finprod_ne_zero I
  · apply Associates.mk_ne_zero.mpr hI
  intro v hv
  obtain ⟨J, hJv⟩ := Associates.exists_rep v
  rw [← hJv, Associates.irreducible_mk] at hv
  rw [← hJv]
  apply Ideal.finprod_count
    ⟨J, Ideal.isPrime_of_prime (irreducible_iff_prime.mp hv), Irreducible.ne_zero hv⟩ I hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ ⨅ (i : HeightOneSpectrum R), i.maxPowDividing I = I
have nth_rw : Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
  (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)
Tactic: nth_rw 2 [← Ideal.finprod_heightOneSpectrum_factorization h0]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)
have rw : Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
  (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) sorry,
    i.maxPowDividing I)
Tactic: rw [finprod_def, dif_pos (Ideal.hasFiniteMulSupport h0), Ideal.prod_eq_iInf_of_pairwise_isCoprime]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
rw :
  Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
      i.maxPowDividing I)
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)
have rw₁ : (↑(Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) sorry) :
      Set (HeightOneSpectrum R)).Pairwise
  (onFun (β := Ideal R) IsCoprime fun (i : HeightOneSpectrum R) ↦ i.maxPowDividing I)
Tactic: rw [finprod_def, dif_pos (Ideal.hasFiniteMulSupport h0), Ideal.prod_eq_iInf_of_pairwise_isCoprime]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
      i.maxPowDividing I)
have h : ∀ (x : R),
  Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x ↔
    Membership.mem (γ := Ideal R)
      (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) sorry,
        i.maxPowDividing I)
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
⊢ Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x ↔
    Membership.mem (γ := Ideal R)
      (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I)
      x
have h : Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x →
  Membership.mem (γ := Ideal R)
    (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) sorry,
      i.maxPowDividing I)
    x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h :
  Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x →
    Membership.mem (γ := Ideal R)
      (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I)
      x
⊢ Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x ↔
    Membership.mem (γ := Ideal R)
      (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I)
      x
have h₁ : Membership.mem (γ := Ideal R)
    (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) sorry,
      i.maxPowDividing I)
    x →
  Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
⊢ Membership.mem (γ := Ideal R)
      (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I)
      x →
    Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x
have h : (∀ (i : HeightOneSpectrum R) (i_1 : ¬i.maxPowDividing I = ⊤), x ∈ i.maxPowDividing I) →
  ∀ (i : HeightOneSpectrum R), x ∈ i.maxPowDividing I
Tactic: simp only [Finite.mem_toFinset, mem_mulSupport, one_eq_top, ne_eq, Submodule.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R) (i_1 : ¬i.maxPowDividing I = ⊤), x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
⊢ x ∈ i.maxPowDividing I
have pos : i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
Tactic: by_cases i.maxPowDividing I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R) (i_1 : ¬i.maxPowDividing I = ⊤), x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
pos : i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
⊢ x ∈ i.maxPowDividing I
have neg : ¬i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
Tactic: by_cases i.maxPowDividing I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)
have rw : Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
  (if h : HasFiniteMulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I then
    ∏ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) h,
      i.maxPowDividing I
  else 1)
Tactic: classical
  rw [finprod_def, dif_pos (Ideal.hasFiniteMulSupport h0), Ideal.prod_eq_iInf_of_pairwise_isCoprime]
  · ext x
    constructor
    · aesop
    · simp only [Finite.mem_toFinset, mem_mulSupport, one_eq_top, ne_eq, Submodule.mem_iInf]
      intro h i
      by_cases i.maxPowDividing I = ⊤ <;> simp_all
  · intro x hx y hy hxy
    apply IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne _ _ hxy
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
rw :
  Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (if h : HasFiniteMulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I then
      ∏ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) h,
        i.maxPowDividing I
    else 1)
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)
have rw₁ : Eq (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
  (∏ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) sorry,
    i.maxPowDividing I)
Tactic: classical
  rw [finprod_def, dif_pos (Ideal.hasFiniteMulSupport h0), Ideal.prod_eq_iInf_of_pairwise_isCoprime]
  · ext x
    constructor
    · aesop
    · simp only [Finite.mem_toFinset, mem_mulSupport, one_eq_top, ne_eq, Submodule.mem_iInf]
      intro h i
      by_cases i.maxPowDividing I = ⊤ <;> simp_all
  · intro x hx y hy hxy
    apply IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne _ _ hxy
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
rw :
  Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (if h : HasFiniteMulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I then
      ∏ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) h,
        i.maxPowDividing I
    else 1)
rw₁ :
  Eq (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
      i.maxPowDividing I)
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)
have rw₂ : Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
  (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) sorry,
    i.maxPowDividing I)
Tactic: classical
  rw [finprod_def, dif_pos (Ideal.hasFiniteMulSupport h0), Ideal.prod_eq_iInf_of_pairwise_isCoprime]
  · ext x
    constructor
    · aesop
    · simp only [Finite.mem_toFinset, mem_mulSupport, one_eq_top, ne_eq, Submodule.mem_iInf]
      intro h i
      by_cases i.maxPowDividing I = ⊤ <;> simp_all
  · intro x hx y hy hxy
    apply IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne _ _ hxy
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
rw :
  Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (if h : HasFiniteMulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I then
      ∏ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) h,
        i.maxPowDividing I
    else 1)
rw₁ :
  Eq (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
      i.maxPowDividing I)
rw₂ :
  Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
      i.maxPowDividing I)
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)
have rw₃ : (↑(Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) sorry) :
      Set (HeightOneSpectrum R)).Pairwise
  (onFun (β := Ideal R) IsCoprime fun (i : HeightOneSpectrum R) ↦ i.maxPowDividing I)
Tactic: classical
  rw [finprod_def, dif_pos (Ideal.hasFiniteMulSupport h0), Ideal.prod_eq_iInf_of_pairwise_isCoprime]
  · ext x
    constructor
    · aesop
    · simp only [Finite.mem_toFinset, mem_mulSupport, one_eq_top, ne_eq, Submodule.mem_iInf]
      intro h i
      by_cases i.maxPowDividing I = ⊤ <;> simp_all
  · intro x hx y hy hxy
    apply IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne _ _ hxy
-- 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 : Ideal R
hI : I ≠ 0
| (↑I : FractionalIdeal R⁰ K)
have rw : (↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) : FractionalIdeal R⁰ K)
Tactic: rw [← Ideal.finprod_heightOneSpectrum_factorization hI]
-- 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 : Ideal R
hI : I ≠ 0
⊢ 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 I))) : ℤ))
    (↑I : FractionalIdeal R⁰ K)
have conv_rhs : 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 I))) : ℤ))
  (↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) : FractionalIdeal R⁰ K)
Tactic: conv_rhs => rw [← Ideal.finprod_heightOneSpectrum_factorization hI]
-- 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 : Ideal R
hI : I ≠ 0
⊢ 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 I))) : ℤ))
    (↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) : FractionalIdeal R⁰ K)
have rw : 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 I))) : ℤ))
  (∏ᶠ (a : HeightOneSpectrum R), (↑(a.maxPowDividing I) : FractionalIdeal R⁰ K))
Tactic: rw [FractionalIdeal.coeIdeal_finprod R⁰ K (le_refl _)]
-- 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 : Ideal R
hI : I ≠ 0
⊢ 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 I))) : ℤ))
    (∏ᶠ (a : HeightOneSpectrum R), (↑(a.maxPowDividing I) : FractionalIdeal R⁰ K))
have simp_rw : 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 I))) : ℤ))
  (∏ᶠ (a : HeightOneSpectrum R),
    (↑(a.asIdeal ^ Associates.count (Associates.mk a.asIdeal) (Associates.factors (Associates.mk I))) :
      FractionalIdeal R⁰ K))
Tactic: simp_rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, FractionalIdeal.coeIdeal_pow,
    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
I : Ideal R
hI : I ≠ 0
simp_rw :
  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 I))) : ℤ))
    (∏ᶠ (a : HeightOneSpectrum R),
      (↑(a.asIdeal ^ Associates.count (Associates.mk a.asIdeal) (Associates.factors (Associates.mk I))) :
        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)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) : ℤ))
    (∏ᶠ (a : HeightOneSpectrum R), (↑(a.maxPowDividing I) : FractionalIdeal R⁰ K))
have simp_rw₁ : 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 I))) : ℤ))
  (∏ᶠ (a : HeightOneSpectrum R),
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑a.asIdeal : FractionalIdeal R⁰ K)
      (Associates.count (Associates.mk a.asIdeal) (Associates.factors (Associates.mk I))))
Tactic: simp_rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, FractionalIdeal.coeIdeal_pow,
    zpow_natCast]
-- 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)
⊢ ∏ᶠ (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 hJ_ne_zero : J ≠ 0
Tactic: have hJ_ne_zero : J ≠ 0 := ideal_factor_ne_zero hI haJ
-- 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
⊢ ∏ᶠ (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 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)
Tactic: have hJ := Ideal.finprod_heightOneSpectrum_factorization_coe K hJ_ne_zero
-- 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)
⊢ ∏ᶠ (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_ne_zero : Ne (α := Ideal R) (span {a}) 0
Tactic: have ha_ne_zero : Ideal.span {a} ≠ 0 := constant_factor_ne_zero hI haJ