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
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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
⊢ False
have hp's : p' ∈ s
Tactic: have hp's : p' ∈ s := by simpa [p', s, Ideal.dvd_iff_le] using le_sup_left.trans h
-- 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})
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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
⊢ False
have H₁ : J * K ≤ J * p
Tactic: have H₁ : J * K ≤ J * p := Ideal.mul_mono_right (le_sup_right.trans h)
-- 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})
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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : J * K ≤ J * p
⊢ False
have H₂ : ∑ p ∈ s, a p ∈ J * p
Tactic: replace H₁ := hK.trans_le H₁ (Ideal.mem_span_singleton_self _)
Cleared hypotheses: 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
⊢ ∑ q ∈ s \ {p'}, a q ∈ J * p
have refine : ∀ (q : HeightOneSpectrum R) (hq : q ∈ s \ {p'}), a q ∈ J * p
Tactic: refine sum_mem fun q hq ↦ ?_
-- 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})
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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
q : HeightOneSpectrum R
hq : q ∈ s \ {p'}
⊢ a q ∈ J * p
have hq₁ : q ∈ s ∧ ¬q = p'
Tactic: rw [Finset.mem_sdiff, Finset.mem_singleton] at hq
Cleared hypotheses: hq
-- 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
q : HeightOneSpectrum R
hq : q ∈ s ∧ ¬q = p'
⊢ a q ∈ J * p
have refine : ∏ q ∈ s \ {q}, q.asIdeal ≤ p
Tactic: refine Ideal.mul_mono_right ?_ (ha q hq.1)
-- 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})
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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
⊢ False
have H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
Tactic: have H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p := by
    refine sum_mem fun q hq ↦ ?_
    rw [Finset.mem_sdiff, Finset.mem_singleton] at hq
    refine Ideal.mul_mono_right ?_ (ha q hq.1)
    exact Ideal.prod_le_inf.trans (Finset.inf_le (b := p') (by simpa [hp's] using Ne.symm hq.2))
-- 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
⊢ False
have apply : a p' ∈ J * ∏ q ∈ s, q.asIdeal
Tactic: apply ha' _ hp's
-- 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})
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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal
have this₁ : Eq (α := Ideal R)
  (s.inf fun (i : HeightOneSpectrum R) ↦
    HPow.hPow (α := Ideal R) (β := ℕ) ((fun (i : HeightOneSpectrum R) ↦ i.asIdeal) i)
      ((fun (x : HeightOneSpectrum R) ↦ (1 : ℕ)) i))
  (∏ i ∈ s,
    HPow.hPow (α := Ideal R) (β := ℕ) ((fun (i : HeightOneSpectrum R) ↦ i.asIdeal) i)
      ((fun (x : HeightOneSpectrum R) ↦ (1 : ℕ)) i))
Tactic: have := IsDedekindDomain.inf_pow_eq_prod_of_prime s (fun i ↦ i.asIdeal) (fun _ ↦ 1)
    (fun i _ ↦ i.prime) (fun i _ j _ e ↦ mt HeightOneSpectrum.ext e)
-- 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})
this_1 : ∀ 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this :
  Eq (α := Ideal R)
    (s.inf fun (i : HeightOneSpectrum R) ↦
      HPow.hPow (α := Ideal R) (β := ℕ) ((fun (i : HeightOneSpectrum R) ↦ i.asIdeal) i)
        ((fun (x : HeightOneSpectrum R) ↦ (1 : ℕ)) i))
    (∏ i ∈ s,
      HPow.hPow (α := Ideal R) (β := ℕ) ((fun (i : HeightOneSpectrum R) ↦ i.asIdeal) i)
        ((fun (x : HeightOneSpectrum R) ↦ (1 : ℕ)) i))
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal
have this₁ : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
Tactic: simp only [pow_one] at this
Cleared hypotheses: this
-- 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})
this_1 : ∀ 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal
have inst : Nonempty.{max 1 (u_1 + 1)} ↥s
Tactic: have inst : Nonempty {x // x ∈ s} := ⟨_, hp's⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : 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_1 : ∀ 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal
have rw : ∀ (i : Subtype (Membership.mem s)), a p' ∈ J * (↑i : HeightOneSpectrum R).asIdeal
Tactic: rw [← this, Finset.inf_eq_iInf, iInf_subtype', Ideal.mul_iInf, Ideal.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : 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_1 : ∀ 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
q : HeightOneSpectrum R
hq : q ∈ s
⊢ a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal
have pos : ∀ (hqp : q = p'), a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal
Tactic: by_cases hqp : q = p'
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : 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_1 : ∀ 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
q : HeightOneSpectrum R
hq : q ∈ s
pos : ∀ (hqp : q = p'), a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal
⊢ a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal
have neg : ∀ (hqp : ¬q = p'), a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal
Tactic: by_cases hqp : q = p'
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : 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_1 : ∀ 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : q = p'
⊢ a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal
have pos : ∀ (hq : p' ∈ s), a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) p' hq) : HeightOneSpectrum R).asIdeal
Tactic: subst hqp
Cleared hypotheses: q, hq, hqp
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : 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_1 : ∀ 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
hq : p' ∈ s
⊢ a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) p' hq) : HeightOneSpectrum R).asIdeal
have h₁ : a p' = HSub.hSub (α := R) (∑ p ∈ s, a p) (∑ q ∈ s \ {p'}, a q)
Tactic: convert! sub_mem H₁ H₂
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : 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_1 : ∀ 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
hq : p' ∈ s
⊢ a p' = HSub.hSub (α := R) (∑ p ∈ s, a p) (∑ q ∈ s \ {p'}, a q)
have h₁ : a p' = a p' + ∑ x ∈ s \ {p'}, a x - ∑ q ∈ s \ {p'}, a q
Tactic: rw [Finset.sum_eq_add_sum_diff_singleton_of_mem hp's, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : 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_1 : ∀ 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
hq : p' ∈ s
h₁ : a p' = a p' + ∑ x ∈ s \ {p'}, a x - ∑ q ∈ s \ {p'}, a q
⊢ a p' = HSub.hSub (α := R) (∑ p ∈ s, a p) (∑ q ∈ s \ {p'}, a q)
have h₂ : a p' = a p'
Tactic: rw [Finset.sum_eq_add_sum_diff_singleton_of_mem hp's, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : 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_1 : ∀ 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 = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : ¬q = p'
⊢ a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal
have neg : ∏ q ∈ s \ {p'}, q.asIdeal ≤ (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal
Tactic: refine Ideal.mul_mono_right ?_ (ha p' hp's)
-- 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: classical
  obtain ⟨I, rfl⟩ := Ideal.dvd_iff_le.mpr hIJ
  simp only [ne_eq, mul_eq_zero, not_or] at hI
  obtain ⟨hJ, hI⟩ := hI
  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]⟩
  let s := (I.finite_factors hI).toFinset
  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⟩
  choose! a ha ha' using fun p hps ↦ SetLike.exists_of_lt (this p hps)
  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)
  refine ⟨_, _, hK.symm, ?_⟩
  by_contra H
  obtain ⟨p, hp, h⟩ := Ideal.exists_le_maximal _ H
  let p' : HeightOneSpectrum R := ⟨p, hp.isPrime, fun e ↦ hI (by simp_all)⟩
  have hp's : p' ∈ s := by simpa [p', s, Ideal.dvd_iff_le] using le_sup_left.trans h
  have H₁ : J * K ≤ J * p := Ideal.mul_mono_right (le_sup_right.trans h)
  replace H₁ := hK.trans_le H₁ (Ideal.mem_span_singleton_self _)
  have H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p := by
    refine sum_mem fun q hq ↦ ?_
    rw [Finset.mem_sdiff, Finset.mem_singleton] at hq
    refine Ideal.mul_mono_right ?_ (ha q hq.1)
    exact Ideal.prod_le_inf.trans (Finset.inf_le (b := p') (by simpa [hp's] using Ne.symm hq.2))
  apply ha' _ hp's
  have := IsDedekindDomain.inf_pow_eq_prod_of_prime s (fun i ↦ i.asIdeal) (fun _ ↦ 1)
    (fun i _ ↦ i.prime) (fun i _ j _ e ↦ mt HeightOneSpectrum.ext e)
  simp only [pow_one] at this
  have inst : Nonempty {x // x ∈ s} := ⟨_, hp's⟩
  rw [← this, Finset.inf_eq_iInf, iInf_subtype', Ideal.mul_iInf, Ideal.mem_iInf]
  rintro ⟨q, hq⟩
  by_cases hqp : q = p'
  · subst hqp
    convert! sub_mem H₁ H₂
    rw [Finset.sum_eq_add_sum_diff_singleton_of_mem hp's, add_sub_cancel_right]
  · refine Ideal.mul_mono_right ?_ (ha p' hp's)
    exact Ideal.prod_le_inf.trans (Finset.inf_le (b := q) (by simpa [hq] using hqp))
Cleared hypotheses: I, hIJ, hI