awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι} (hp : ∀ i ∈ s, (f i).IsPrime) (hn : s.card = n)
    (h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)),
    I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ((↑(f i) : Set R) ∪ ⋃ x ∈ (↑t : Set ι), (↑(f x) : Set R))
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : ¬f b ≤ f i
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ (↑(f i) : Set R)
hr : r ∈ (↑(t.inf f) : Set R)
hrb : r ∈ (↑(f b) : Set R)
hrI : r ∈ (↑I : Set R)
hra : r ∈ (↑(f a) : Set R)
HI : ¬(↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
s : R
hsI : s ∈ (↑I : Set R)
hs : s ∉ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
hsi : s ∈ f i
j : ι
hjt : j ∈ (↑t : Set ι)
hj : r + s ∈ (↑(f j) : Set R)
⊢ False
have hr₁ : ∀ (i : ι) (i_1 : i ∈ t), r ∈ f i
Tactic: simp only [Finset.inf_eq_iInf, SetLike.mem_coe, Submodule.mem_iInf] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
⊢ ∃ i ∈ s, I ≤ f i
have pos : ∀ (has : a ∈ s), ∃ i ∈ s, I ≤ f i
Tactic: by_cases has : a ∈ s
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
pos : ∀ (has : a ∈ s), ∃ i ∈ s, I ≤ f i
⊢ ∃ i ∈ s, I ≤ f i
have neg : ∀ (has : a ∉ s), ∃ i ∈ s, I ≤ f i
Tactic: by_cases has : a ∈ s
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
has : a ∈ s
⊢ ∃ i ∈ s, I ≤ f i
have pos : ∀ (t : Finset ι) (hat : a ∉ t) (hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime)
  (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a t) : Set ι), (↑(f i) : Set R)) (has : a ∈ insert a t), ∃ i ∈ insert a t, I ≤ f i
Tactic: obtain ⟨t, hat, rfl⟩ : ∃ t, a ∉ t ∧ insert a t = s :=
        ⟨s.erase a, Finset.notMem_erase a s, Finset.insert_erase has⟩
Cleared hypotheses: s, hp, h, has
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a t) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a t
⊢ ∃ i ∈ insert a t, I ≤ f i
have pos : ∀ (hbt : b ∈ t), ∃ i ∈ insert a t, I ≤ f i
Tactic: by_cases hbt : b ∈ t
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a t) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a t
pos : ∀ (hbt : b ∈ t), ∃ i ∈ insert a t, I ≤ f i
⊢ ∃ i ∈ insert a t, I ≤ f i
have neg : ∀ (hbt : b ∉ t), ∃ i ∈ insert a t, I ≤ f i
Tactic: by_cases hbt : b ∈ t
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a t) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a t
hbt : b ∈ t
⊢ ∃ i ∈ insert a t, I ≤ f i
have pos : ∀ (u : Finset ι) (hbu : b ∉ u) (hat : a ∉ insert b u) (hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime)
  (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a (insert b u)) : Set ι), (↑(f i) : Set R)) (has : a ∈ insert a (insert b u))
  (hbt : b ∈ insert b u), ∃ i ∈ insert a (insert b u), I ≤ f i
Tactic: obtain ⟨u, hbu, rfl⟩ : ∃ u, b ∉ u ∧ insert b u = t :=
          ⟨t.erase b, Finset.notMem_erase b t, Finset.insert_erase hbt⟩
Cleared hypotheses: t, hat, hp, h, has, hbt
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a (insert b u)) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
⊢ (f i).IsPrime
have refine_1 : i ≠ a
Tactic: refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a (insert b u)) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
refine_1 : i ≠ a
⊢ (f i).IsPrime
have refine_2 : i ≠ b
Tactic: refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a (insert b u)) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i
have hp' : ∀ i ∈ u, (f i).IsPrime
Tactic: have hp' : ∀ i ∈ u, IsPrime (f i) := by
          intro i hiu
          refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_ <;>
              rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a (insert b u)) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i
have h₁ : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
Tactic: rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ←
          Set.union_assoc, subset_union_prime' hp'] at h
Cleared hypotheses: h, has, hbt, hp'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i
have pos : I ≤ f a ∨ ∃ x ∈ insert b u, I ≤ f x
Tactic: rwa [Finset.exists_mem_insert, Finset.exists_mem_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a t) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a t
hbt : b ∉ t
j : ι
hj : j ∈ t
⊢ (f j).IsPrime
have refine_1 : j ≠ a
Tactic: refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a t) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a t
hbt : b ∉ t
j : ι
hj : j ∈ t
refine_1 : j ≠ a
⊢ (f j).IsPrime
have refine_2 : j ≠ b
Tactic: refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a t) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a t
hbt : b ∉ t
⊢ ∃ i ∈ insert a t, I ≤ f i
have hp' : ∀ j ∈ t, (f j).IsPrime
Tactic: have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a t) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a t
hbt : b ∉ t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert a t, I ≤ f i
have h₁ : I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
Tactic: rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f a : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
Cleared hypotheses: h, has, hbt, hp'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
has : a ∉ s
⊢ ∃ i ∈ s, I ≤ f i
have pos : ∀ (hbs : b ∈ s), ∃ i ∈ s, I ≤ f i
Tactic: by_cases hbs : b ∈ s
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
has : a ∉ s
pos : ∀ (hbs : b ∈ s), ∃ i ∈ s, I ≤ f i
⊢ ∃ i ∈ s, I ≤ f i
have neg : ∀ (hbs : b ∉ s), ∃ i ∈ s, I ≤ f i
Tactic: by_cases hbs : b ∈ s
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
has : a ∉ s
hbs : b ∈ s
⊢ ∃ i ∈ s, I ≤ f i
have pos : ∀ (t : Finset ι) (hbt : b ∉ t) (hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime)
  (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert b t) : Set ι), (↑(f i) : Set R)) (has : a ∉ insert b t) (hbs : b ∈ insert b t),
  ∃ i ∈ insert b t, I ≤ f i
Tactic: obtain ⟨t, hbt, rfl⟩ : ∃ t, b ∉ t ∧ insert b t = s :=
          ⟨s.erase b, Finset.notMem_erase b s, Finset.insert_erase hbs⟩
Cleared hypotheses: s, hp, h, has, hbs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert b t) : Set ι), (↑(f i) : Set R)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
⊢ (f j).IsPrime
have refine_1 : j ≠ a
Tactic: refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert b t) : Set ι), (↑(f i) : Set R)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
refine_1 : j ≠ a
⊢ (f j).IsPrime
have refine_2 : j ≠ b
Tactic: refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert b t) : Set ι), (↑(f i) : Set R)
has : a ∉ insert b t
hbs : b ∈ insert b t
⊢ ∃ i ∈ insert b t, I ≤ f i
have hp' : ∀ j ∈ t, (f j).IsPrime
Tactic: have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert b t) : Set ι), (↑(f i) : Set R)
has : a ∉ insert b t
hbs : b ∈ insert b t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert b t, I ≤ f i
have h₁ : I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
Tactic: rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f b : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
Cleared hypotheses: h, has, hbs, hp'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
has : a ∉ s
hbs : b ∉ s
⊢ ∃ i ∈ s, I ≤ f i
have neg : ∀ (hp : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → i ≠ a → i ≠ b → (f i).IsPrime)
  (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑∅ : Set ι), (↑(f i) : Set R)) (has : a ∉ ∅) (hbs : b ∉ ∅),
  ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ I ≤ f i
Tactic: rcases s.eq_empty_or_nonempty with rfl | hsne
Cleared hypotheses: s, hp, h, has, hbs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
has : a ∉ s
hbs : b ∉ s
neg :
  ∀ (hp : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → i ≠ a → i ≠ b → (f i).IsPrime)
    (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑∅ : Set ι), (↑(f i) : Set R)) (has : a ∉ ∅) (hbs : b ∉ ∅),
    ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ I ≤ f i
⊢ ∃ i ∈ s, I ≤ f i
have neg₁ : ∀ (hsne : s.Nonempty), ∃ i ∈ s, I ≤ f i
Tactic: rcases s.eq_empty_or_nonempty with rfl | hsne
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
hp : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → i ≠ a → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑∅ : Set ι), (↑(f i) : Set R)
has : a ∉ ∅
hbs : b ∉ ∅
⊢ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ I ≤ f i
have h₁ : (↑I : Set R) ⊆ ∅
Tactic: rw [Finset.coe_empty, Set.biUnion_empty] at h
Cleared hypotheses: h, has, hbs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
has : a ∉ s
hbs : b ∉ s
hsne : s.Nonempty
⊢ ∃ i ∈ s, I ≤ f i
have neg : ∀ (i : ι) (his : i ∈ s), ∃ i ∈ s, I ≤ f i
Tactic: obtain ⟨i, his⟩ := hsne
Cleared hypotheses: hsne
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
has : a ∉ s
hbs : b ∉ s
i : ι
his : i ∈ s
⊢ ∃ i ∈ s, I ≤ f i
have neg : ∀ (t : Finset ι),
  i ∉ t →
    ∀ (hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime)
      (h : (↑I : Set R) ⊆ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R)) (has : a ∉ insert i t)
      (hbs : b ∉ insert i t) (his : i ∈ insert i t), ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: obtain ⟨t, _, rfl⟩ : ∃ t, i ∉ t ∧ insert i t = s :=
          ⟨s.erase i, Finset.notMem_erase i s, Finset.insert_erase his⟩
Cleared hypotheses: s, hp, h, has, hbs, his
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : (↑I : Set R) ⊆ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
j : ι
hj : j ∈ t
⊢ (f j).IsPrime
have refine_1 : j ≠ a
Tactic: refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : (↑I : Set R) ⊆ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
j : ι
hj : j ∈ t
refine_1 : j ≠ a
⊢ (f j).IsPrime
have refine_2 : j ≠ b
Tactic: refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : (↑I : Set R) ⊆ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1
have hp' : ∀ j ∈ t, (f j).IsPrime
Tactic: have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : (↑I : Set R) ⊆ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1
have h₁ : I ≤ f i ∨ ∃ i ∈ t, I ≤ f i
Tactic: rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f i : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
Cleared hypotheses: h, has, hbs, his, hp'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
⊢ ∃ i ∈ s, I ≤ f i
have pos : ∀ (has : a ∈ s), ∃ i ∈ s, I ≤ f i
Tactic: classical
    by_cases has : a ∈ s
    · obtain ⟨t, hat, rfl⟩ : ∃ t, a ∉ t ∧ insert a t = s :=
        ⟨s.erase a, Finset.notMem_erase a s, Finset.insert_erase has⟩
      by_cases hbt : b ∈ t
      · obtain ⟨u, hbu, rfl⟩ : ∃ u, b ∉ u ∧ insert b u = t :=
          ⟨t.erase b, Finset.notMem_erase b t, Finset.insert_erase hbt⟩
        have hp' : ∀ i ∈ u, IsPrime (f i) := by
          intro i hiu
          refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_ <;>
              rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ←
          Set.union_assoc, subset_union_prime' hp'] at h
        rwa [Finset.exists_mem_insert, Finset.exists_mem_insert]
      · have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f a : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]
    · by_cases hbs : b ∈ s
      · obtain ⟨t, hbt, rfl⟩ : ∃ t, b ∉ t ∧ insert b t = s :=
          ⟨s.erase b, Finset.notMem_erase b s, Finset.insert_erase hbs⟩
        have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f b : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]
      rcases s.eq_empty_or_nonempty with rfl | hsne
      · rw [Finset.coe_empty, Set.biUnion_empty] at h
        exact (h I.zero_mem).elim
      · obtain ⟨i, his⟩ := hsne
        obtain ⟨t, _, rfl⟩ : ∃ t, i ∉ t ∧ insert i t = s :=
          ⟨s.erase i, Finset.notMem_erase i s, Finset.insert_erase his⟩
        have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f i : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
pos : ∀ (has : a ∈ s), ∃ i ∈ s, I ≤ f i
⊢ ∃ i ∈ s, I ≤ f i
have neg : ∀ (has : a ∉ s), ∃ i ∈ s, I ≤ f i
Tactic: classical
    by_cases has : a ∈ s
    · obtain ⟨t, hat, rfl⟩ : ∃ t, a ∉ t ∧ insert a t = s :=
        ⟨s.erase a, Finset.notMem_erase a s, Finset.insert_erase has⟩
      by_cases hbt : b ∈ t
      · obtain ⟨u, hbu, rfl⟩ : ∃ u, b ∉ u ∧ insert b u = t :=
          ⟨t.erase b, Finset.notMem_erase b t, Finset.insert_erase hbt⟩
        have hp' : ∀ i ∈ u, IsPrime (f i) := by
          intro i hiu
          refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_ <;>
              rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ←
          Set.union_assoc, subset_union_prime' hp'] at h
        rwa [Finset.exists_mem_insert, Finset.exists_mem_insert]
      · have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f a : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]
    · by_cases hbs : b ∈ s
      · obtain ⟨t, hbt, rfl⟩ : ∃ t, b ∉ t ∧ insert b t = s :=
          ⟨s.erase b, Finset.notMem_erase b s, Finset.insert_erase hbs⟩
        have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f b : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]
      rcases s.eq_empty_or_nonempty with rfl | hsne
      · rw [Finset.coe_empty, Set.biUnion_empty] at h
        exact (h I.zero_mem).elim
      · obtain ⟨i, his⟩ := hsne
        obtain ⟨t, _, rfl⟩ : ∃ t, i ∉ t ∧ insert i t = s :=
          ⟨s.erase i, Finset.notMem_erase i s, Finset.insert_erase his⟩
        have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f i : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]