awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Operations
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
pos : I ≤ f a ∨ ∃ x ∈ insert b u, I ≤ f x
pos₁ pos₂ pos₃ pos₄ : I ≤ f a ∨ I ≤ f b ∨ ∃ x ∈ u, I ≤ f x
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i

Tactic:
rwa [Finset.exists_mem_insert, Finset.exists_mem_insert]

Premises used: Finset.exists_mem_insert
-- Module: Mathlib.RingTheory.Ideal.Operations
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

Tactic:
hp j (Finset.mem_insert_of_mem hj) ?_ ?_

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
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
refine_2 : j ≠ b
⊢ (f j).IsPrime

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
j : ι
hj : j ∈ t
hat : j ∉ t
hp : ∀ i ∈ insert j t, i ≠ j → i ≠ b → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert j t) : Set ι), (↑(f i) : Set R)
has : j ∈ insert j t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert a t) : Set ι), (↑(f i) : Set R)
has : a ∈ insert a t
j : ι
hj : j ∈ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ j → (f i).IsPrime
hbt : j ∉ t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
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 ∈ 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, *]
-- Module: Mathlib.RingTheory.Ideal.Operations
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 ≤ 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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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
h₁ : I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
⊢ a ∈ insert a t

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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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
h₁ : I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
has₁ : a ∈ insert a t
⊢ b ∉ t

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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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
h₁ : I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
has₁ : a ∈ insert a t
hbt₁ : b ∉ t
⊢ ∀ j ∈ t, (f j).IsPrime

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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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 ≤ f a ∨ ∃ i ∈ t, I ≤ f i
has : a ∈ insert a t
hbt : b ∉ t
hp' : ∀ j ∈ t, (f j).IsPrime
neg neg₁ neg₂ neg₃ : I ≤ f a ∨ ∃ x ∈ t, I ≤ f x
⊢ ∃ i ∈ insert a t, I ≤ f i

Tactic:
rwa [Finset.exists_mem_insert]

Premises used: Finset.exists_mem_insert
-- Module: Mathlib.RingTheory.Ideal.Operations
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
neg : ∀ (hbs : b ∉ s), ∃ i ∈ s, I ≤ f i
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
by_cases hbs : b ∈ s
-- Module: Mathlib.RingTheory.Ideal.Operations
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
⊢ ∃ (t : Finset ι), b ∉ t ∧ insert b t = s

Tactic:
⟨s.erase b, Finset.notMem_erase b s, Finset.insert_erase hbs⟩

Premises used: And.intro, Exists.intro, Finset.notMem_erase, Finset.erase, Finset.insert_erase
-- Module: Mathlib.RingTheory.Ideal.Operations
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
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
⊢ ∃ i ∈ s, 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⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
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

Tactic:
hp j (Finset.mem_insert_of_mem hj) ?_ ?_

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
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
refine_2 : j ≠ b
⊢ (f j).IsPrime

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert b t) : Set ι), (↑(f i) : Set R)
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
hp : ∀ i ∈ insert b t, i ≠ j → i ≠ b → (f i).IsPrime
has : j ∉ insert b t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
t : Finset ι
j : ι
hj : j ∈ t
hbt : j ∉ t
hp : ∀ i ∈ insert j t, i ≠ a → i ≠ j → (f i).IsPrime
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑(insert j t) : Set ι), (↑(f i) : Set R)
has : a ∉ insert j t
hbs : j ∈ insert j t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
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 ∈ 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, *]
-- Module: Mathlib.RingTheory.Ideal.Operations
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 ≤ 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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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
h₁ : I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
⊢ a ∉ insert b t

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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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
h₁ : I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
has₁ : a ∉ insert b t
⊢ b ∈ insert b t

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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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
h₁ : I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
has₁ : a ∉ insert b t
hbs₁ : b ∈ insert b t
⊢ ∀ j ∈ t, (f j).IsPrime

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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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 ≤ f b ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert b t
hbs : b ∈ insert b t
hp' : ∀ j ∈ t, (f j).IsPrime
pos pos₁ pos₂ pos₃ : I ≤ f b ∨ ∃ x ∈ t, I ≤ f x
⊢ ∃ i ∈ insert b t, I ≤ f i

Tactic:
rwa [Finset.exists_mem_insert]

Premises used: Finset.exists_mem_insert
-- Module: Mathlib.RingTheory.Ideal.Operations
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
neg₁ : ∀ (hsne : s.Nonempty), ∃ i ∈ s, I ≤ f i
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hsne

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.RingTheory.Ideal.Operations
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 : Set R) ⊆ ∅

Tactic:
rw [Finset.coe_empty, Set.biUnion_empty] at h

Premises used: Finset.coe_empty, Set.biUnion_empty
-- Module: Mathlib.RingTheory.Ideal.Operations
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 ∉ ∅
h₁ : (↑I : Set R) ⊆ ∅
⊢ a ∉ ∅

Tactic:
rw [Finset.coe_empty, Set.biUnion_empty] at h

Premises used: Finset.coe_empty, Set.biUnion_empty
-- Module: Mathlib.RingTheory.Ideal.Operations
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 ∉ ∅
h₁ : (↑I : Set R) ⊆ ∅
has₁ : a ∉ ∅
⊢ b ∉ ∅

Tactic:
rw [Finset.coe_empty, Set.biUnion_empty] at h

Premises used: Finset.coe_empty, Set.biUnion_empty
-- Module: Mathlib.RingTheory.Ideal.Operations
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) ⊆ ∅
has : a ∉ ∅
hbs : b ∉ ∅
⊢ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ I ≤ f i

Tactic:
(h I.zero_mem).elim

Premises used: False.elim, Ideal.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
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) ⊆ ∅
has : a ∉ ∅
hbs : b ∉ ∅
⊢ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ I ≤ f i

Tactic:
exact (h I.zero_mem).elim

Premises used: False.elim, Ideal.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
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
neg : ∀ (i : ι) (his : i ∈ s), ∃ i ∈ s, I ≤ f i
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
obtain ⟨i, his⟩ := hsne
-- Module: Mathlib.RingTheory.Ideal.Operations
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
⊢ ∃ (t : Finset ι), i ∉ t ∧ insert i t = s

Tactic:
⟨s.erase i, Finset.notMem_erase i s, Finset.insert_erase his⟩

Premises used: And.intro, Exists.intro, Finset.notMem_erase, Finset.erase, Finset.insert_erase
-- Module: Mathlib.RingTheory.Ideal.Operations
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
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
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
obtain ⟨t, _, rfl⟩ : ∃ t, i ∉ t ∧ insert i t = s :=
          ⟨s.erase i, Finset.notMem_erase i s, Finset.insert_erase his⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
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

Tactic:
hp j (Finset.mem_insert_of_mem hj) ?_ ?_

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
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
refine_2 : j ≠ b
⊢ (f j).IsPrime

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
i : ι
t : Finset ι
left : i ∉ t
h : (↑I : Set R) ⊆ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R)
hbs : b ∉ insert i t
his : i ∈ insert i t
j : ι
hj : j ∈ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ j → i_1 ≠ b → (f i_1).IsPrime
has : j ∉ insert i t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
i : ι
t : Finset ι
left : i ∉ t
h : (↑I : Set R) ⊆ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R)
has : a ∉ insert i t
his : i ∈ insert i t
j : ι
hj : j ∈ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ j → (f i_1).IsPrime
hbs : j ∉ insert i t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
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 ∈ 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, *]
-- Module: Mathlib.RingTheory.Ideal.Operations
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 ≤ 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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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
h₁ : I ≤ f i ∨ ∃ i ∈ t, I ≤ f i
⊢ a ∉ insert i t

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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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
h₁ : I ≤ f i ∨ ∃ i ∈ t, I ≤ f i
has₁ : a ∉ insert i t
⊢ b ∉ insert i t

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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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
h₁ : I ≤ f i ∨ ∃ i ∈ t, I ≤ f i
has₁ : a ∉ insert i t
hbs₁ : b ∉ insert i t
⊢ i ∈ insert i t

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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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
h₁ : I ≤ f i ∨ ∃ i ∈ t, I ≤ f i
has₁ : a ∉ insert i t
hbs₁ : b ∉ insert i t
his₁ : i ∈ insert i t
⊢ ∀ j ∈ t, (f j).IsPrime

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

Premises used: Ideal.subset_union_prime', or_self_iff, Set.biUnion_insert, SetLike.coe, Set.union_self, Finset.coe_insert, or_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
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 ≤ f i ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
hp' : ∀ j ∈ t, (f j).IsPrime
neg neg₁ neg₂ neg₃ : I ≤ f i ∨ ∃ x ∈ t, I ≤ f x
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
rwa [Finset.exists_mem_insert]

Premises used: Finset.exists_mem_insert