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
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)
ha_ne_zero : Ne (α := Ideal R) (Ideal.span {a}) 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  Membership.mem (γ := Set (HeightOneSpectrum R))
    {v : HeightOneSpectrum R |
      ¬HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
            (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a})))) : ℤ) =
          0}
    v
hv_irred : Irreducible v.asIdeal
⊢ Membership.mem (γ := Set (HeightOneSpectrum R))
    ({v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪ {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {a}}) v
have by_contra : ∀
  (h_notMem :
    ¬Membership.mem (γ := Set (HeightOneSpectrum R))
        ({v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪ {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {a}}) v),
  False
Tactic: by_contra h_notMem
-- 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)
ha_ne_zero : Ne (α := Ideal R) (Ideal.span {a}) 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  Membership.mem (γ := Set (HeightOneSpectrum R))
    {v : HeightOneSpectrum R |
      ¬HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
            (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a})))) : ℤ) =
          0}
    v
hv_irred : Irreducible v.asIdeal
h_notMem :
  ¬Membership.mem (γ := Set (HeightOneSpectrum R))
      ({v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪ {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {a}}) v
⊢ False
have h_notMem₁ : ¬(v.asIdeal ∣ J ∨ v.asIdeal ∣ Ideal.span {a})
Tactic: rw [mem_union, mem_setOf_eq, mem_setOf_eq] at h_notMem
Cleared hypotheses: h_notMem
-- 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)
ha_ne_zero : Ne (α := Ideal R) (Ideal.span {a}) 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  Membership.mem (γ := Set (HeightOneSpectrum R))
    {v : HeightOneSpectrum R |
      ¬HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
            (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a})))) : ℤ) =
          0}
    v
hv_irred : Irreducible v.asIdeal
h_notMem : ¬(v.asIdeal ∣ J ∨ v.asIdeal ∣ Ideal.span {a})
⊢ False
have h_notMem₁ : ¬v.asIdeal ∣ J ∧ ¬v.asIdeal ∣ Ideal.span {a}
Tactic: push Not at h_notMem
Cleared hypotheses: h_notMem
-- 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)
ha_ne_zero : Ne (α := Ideal R) (Ideal.span {a}) 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  Membership.mem (γ := Set (HeightOneSpectrum R))
    {v : HeightOneSpectrum R |
      ¬HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
            (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a})))) : ℤ) =
          0}
    v
hv_irred : Irreducible v.asIdeal
h_notMem : ¬v.asIdeal ∣ J ∧ ¬v.asIdeal ∣ Ideal.span {a}
⊢ False
have h_notMem₁ : Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J)) = 0 ∧
  Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a}))) = 0
Tactic: rw [← Associates.count_ne_zero_iff_dvd ha_ne_zero hv_irred, not_not,
      ← Associates.count_ne_zero_iff_dvd hJ_ne_zero hv_irred, not_not] at h_notMem
Cleared hypotheses: h_notMem
-- 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)
ha_ne_zero : Ne (α := Ideal R) (Ideal.span {a}) 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  Membership.mem (γ := Set (HeightOneSpectrum R))
    {v : HeightOneSpectrum R |
      ¬HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
            (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a})))) : ℤ) =
          0}
    v
hv_irred : Irreducible v.asIdeal
h_notMem :
  Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J)) = 0 ∧
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a}))) = 0
⊢ False
have hv₁ : ¬Eq (α := ℤ) 0 0
Tactic: rw [mem_setOf_eq, h_notMem.1, h_notMem.2, sub_self] at hv
Cleared hypotheses: hv, hv_irred, h_notMem
-- 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)
ha_ne_zero : Ne (α := Ideal R) (Ideal.span {a}) 0
hJ_ne_zero : J ≠ 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a})))) : ℤ) =
      0
have h_subset : Subset.{u_1} (α := Set (HeightOneSpectrum R))
  {v : HeightOneSpectrum R |
    ¬HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a})))) : ℤ) =
        0}
  ({v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪ {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {a}})
Tactic: have h_subset :
    {v : HeightOneSpectrum R | ¬((Associates.mk v.asIdeal).count (Associates.mk J).factors : ℤ) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = 0} ⊆
    {v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪
      {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {a}} := by
    intro v hv
    have hv_irred : Irreducible v.asIdeal := v.irreducible
    by_contra h_notMem
    rw [mem_union, mem_setOf_eq, mem_setOf_eq] at h_notMem
    push Not at h_notMem
    rw [← Associates.count_ne_zero_iff_dvd ha_ne_zero hv_irred, not_not,
      ← Associates.count_ne_zero_iff_dvd hJ_ne_zero hv_irred, not_not] at h_notMem
    rw [mem_setOf_eq, h_notMem.1, h_notMem.2, sub_self] at hv
    exact hv (Eq.refl 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0
have pos : ∀ (hI : I = 0), ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
pos : ∀ (hI : I = 0), ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0
have neg : ∀ (hI : ¬I = 0), ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J : Ideal R
hIJ : I ≤ J
hI : I ≠ 0
⊢ ∃ (a : R), I ⊔ Ideal.span {a} = J
have obtain : ∀ (I : Ideal R) (hIJ : J * I ≤ J) (hI : J * I ≠ 0), ∃ (a : R), J * I ⊔ Ideal.span {a} = J
Tactic: obtain ⟨I, rfl⟩ := Ideal.dvd_iff_le.mpr hIJ
Cleared hypotheses: I, hIJ, hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hI : J * I ≠ 0
⊢ ∃ (a : R), J * I ⊔ Ideal.span {a} = J
have hI₁ : ¬J = 0 ∧ ¬I = 0
Tactic: simp only [ne_eq, mul_eq_zero, not_or] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hI : ¬J = 0 ∧ ¬I = 0
⊢ ∃ (a : R), J * I ⊔ Ideal.span {a} = J
have hJ : ¬J = 0
Tactic: obtain ⟨hJ, hI⟩ := hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hI : ¬J = 0 ∧ ¬I = 0
hJ : ¬J = 0
⊢ ∃ (a : R), J * I ⊔ Ideal.span {a} = J
have hI₁ : ¬I = 0
Tactic: obtain ⟨hJ, hI⟩ := hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
this : ∃ (a : R) (K : Ideal R), J * K = Ideal.span {a} ∧ I + K = ⊤
⊢ ∃ (a : R), J * I ⊔ Ideal.span {a} = J
have obtain : ∀ (a : R) (K : Ideal R) (e : J * K = Ideal.span {a}) (e' : I + K = ⊤), ∃ (a : R), J * I ⊔ Ideal.span {a} = J
Tactic: obtain ⟨a, K, e, e'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
a : R
K : Ideal R
e : J * K = Ideal.span {a}
e' : I + K = ⊤
⊢ J * I ⊔ Ideal.span {a} = J
have rw : J * I ⊔ J * K = J
Tactic: rw [← e, ← Ideal.add_eq_sup, ← mul_add, e', Ideal.mul_top]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
a : R
K : Ideal R
e : J * K = Ideal.span {a}
e' : I + K = ⊤
rw : J * I ⊔ J * K = J
⊢ J * I ⊔ Ideal.span {a} = J
have rw₁ : J * I + J * K = J
Tactic: rw [← e, ← Ideal.add_eq_sup, ← mul_add, e', Ideal.mul_top]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
a : R
K : Ideal R
e : J * K = Ideal.span {a}
e' : I + K = ⊤
rw : J * I ⊔ J * K = J
rw₁ : J * I + J * K = J
⊢ J * I ⊔ Ideal.span {a} = J
have rw₂ : J * (I + K) = J
Tactic: rw [← e, ← Ideal.add_eq_sup, ← mul_add, e', Ideal.mul_top]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
a : R
K : Ideal R
e : J * K = Ideal.span {a}
e' : I + K = ⊤
rw : J * I ⊔ J * K = J
rw₁ : J * I + J * K = J
rw₂ : J * (I + K) = J
⊢ J * I ⊔ Ideal.span {a} = J
have rw₃ : J * ⊤ = J
Tactic: rw [← e, ← Ideal.add_eq_sup, ← mul_add, e', Ideal.mul_top]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
a : R
K : Ideal R
e : J * K = Ideal.span {a}
e' : I + K = ⊤
rw : J * I ⊔ J * K = J
rw₁ : J * I + J * K = J
rw₂ : J * (I + K) = J
rw₃ : J * ⊤ = J
⊢ J * I ⊔ Ideal.span {a} = J
have rw₄ : J = J
Tactic: rw [← e, ← Ideal.add_eq_sup, ← mul_add, e', Ideal.mul_top]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
⊢ ∃ (a : R), J * I ⊔ Ideal.span {a} = J
have suffices : ∃ (a : R) (K : Ideal R), J * K = Ideal.span {a} ∧ I + K = ⊤
Tactic: suffices ∃ a, ∃ K, J * K = Ideal.span {a} ∧ I + K = ⊤ by
    obtain ⟨a, K, e, e'⟩ := this
    exact ⟨a, by rw [← e, ← Ideal.add_eq_sup, ← mul_add, e', Ideal.mul_top]⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
p : HeightOneSpectrum R
hps : p ∈ s
| J * ∏ q ∈ s \ {p}, q.asIdeal
have rw : (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1
Tactic: rw [← mul_one (J * _)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
p : HeightOneSpectrum R
hps : p ∈ s
⊢ J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
have conv_rhs : J * ∏ q ∈ s, q.asIdeal < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1
Tactic: conv_rhs => rw [← mul_one (J * _)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
p : HeightOneSpectrum R
hps : p ∈ s
⊢ J * ∏ q ∈ s, q.asIdeal < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1
have rw : (J * ∏ x ∈ s \ {p}, x.asIdeal) * p.asIdeal < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1
Tactic: rw [Finset.prod_eq_mul_prod_diff_singleton_of_mem hps, ← mul_assoc,
      mul_right_comm _ p.asIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
p : HeightOneSpectrum R
hps : p ∈ s
⊢ (J * ∏ x ∈ s \ {p}, x.asIdeal) * p.asIdeal < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1
have refine_1 : p.asIdeal < 1
Tactic: refine mul_lt_mul_of_pos_left ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
p : HeightOneSpectrum R
hps : p ∈ s
refine_1 : p.asIdeal < 1
⊢ (J * ∏ x ∈ s \ {p}, x.asIdeal) * p.asIdeal < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1
have refine_2 : 0 < J * ∏ x ∈ s \ {p}, x.asIdeal
Tactic: refine mul_lt_mul_of_pos_left ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
p : HeightOneSpectrum R
hps : p ∈ s
⊢ p.asIdeal < 1
have refine_1 : p.asIdeal ≠ ⊤
Tactic: rw [Ideal.one_eq_top, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
p : HeightOneSpectrum R
hps : p ∈ s
⊢ 0 < J * ∏ x ∈ s \ {p}, x.asIdeal
have refine_2 : J ≠ 0 ∧ ∀ a ∈ s \ {p}, a.asIdeal ≠ 0
Tactic: rw [Ideal.zero_eq_bot, bot_lt_iff_ne_bot, ← Ideal.zero_eq_bot,
        mul_ne_zero_iff, Finset.prod_ne_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
⊢ ∃ (a : R) (K : Ideal R), J * K = Ideal.span {a} ∧ I + K = ⊤
have this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
Tactic: have : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal := by
    intro p hps
    conv_rhs => rw [← mul_one (J * _)]
    rw [Finset.prod_eq_mul_prod_diff_singleton_of_mem hps, ← mul_assoc,
      mul_right_comm _ p.asIdeal]
    refine mul_lt_mul_of_pos_left ?_ ?_
    · rw [Ideal.one_eq_top, lt_top_iff_ne_top]
      exact p.2.ne_top
    · rw [Ideal.zero_eq_bot, bot_lt_iff_ne_bot, ← Ideal.zero_eq_bot,
        mul_ne_zero_iff, Finset.prod_ne_zero_iff]
      exact ⟨hJ, fun x _ ↦ x.3⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
⊢ ∃ (a : R) (K : Ideal R), J * K = Ideal.span {a} ∧ I + K = ⊤
have choose! : ∀ (a : (p : HeightOneSpectrum R) → R)
  (ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal)
  (ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal),
  ∃ (a : R) (K : Ideal R), J * K = Ideal.span {a} ∧ I + K = ⊤
Tactic: choose! a ha ha' using fun p hps ↦ SetLike.exists_of_lt (this p hps)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
⊢ J ∣ Ideal.span {∑ p ∈ s, a p}
have rw : ∑ p ∈ s, a p ∈ J
Tactic: rw [Ideal.dvd_iff_le, Ideal.span_singleton_le_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
⊢ ∃ (a : R) (K : Ideal R), J * K = Ideal.span {a} ∧ I + K = ⊤
have obtain : ∀ (K : Ideal R) (hK : Ideal.span {∑ p ∈ s, a p} = J * K), ∃ (a : R) (K : Ideal R), J * K = Ideal.span {a} ∧ I + K = ⊤
Tactic: obtain ⟨K, hK⟩ : J ∣ Ideal.span {∑ p ∈ s, a p} := by
    rw [Ideal.dvd_iff_le, Ideal.span_singleton_le_iff_mem]
    exact sum_mem fun p hp ↦ Ideal.mul_le_right (ha p hp)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
⊢ ∃ (a : R) (K : Ideal R), J * K = Ideal.span {a} ∧ I + K = ⊤
have refine : I + K = ⊤
Tactic: refine ⟨_, _, hK.symm, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
⊢ I + K = ⊤
have by_contra : ∀ (H : ¬I + K = ⊤), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
⊢ False
have obtain : ∀ (p : Ideal R) (hp : p.IsMaximal) (h : I + K ≤ p), False
Tactic: obtain ⟨p, hp, h⟩ := Ideal.exists_le_maximal _ H