-- Mathlib/RingTheory/Ideal/Operations.lean
theorem subset_union_prime {R : Type u} [CommRing R] {s : Finset ι} {f : ι → Ideal R} (a b : ι)
    (hp : ∀ i ∈ s, i ≠ a → i ≠ b → IsPrime (f i)) {I : Ideal R} :
    ((I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), f i) ↔ ∃ i ∈ s, I ≤ f i :=
  suffices ((I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), f i) → ∃ i, i ∈ s ∧ I ≤ f i by
    have aux := fun h => (bex_def.2 <| this h)
    simp_rw [exists_prop] at aux
    refine ⟨aux, fun ⟨i, his, hi⟩ ↦ Set.Subset.trans hi ?_⟩
    apply Set.subset_biUnion_of_mem (show i ∈ (↑s : Set ι) from his)
  fun h : (I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), f i => by
  classical
    by_cases has : a ∈ s
    · obtain ⟨t, hat, rfl⟩ : ∃ t, a ∉ t ∧ insert a t = s :=
        ⟨s.erase a, Finset.not_mem_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.not_mem_erase b t, Finset.insert_erase hbt⟩
        have hp' : ∀ i ∈ u, IsPrime (f i)

Proof state:
case pos.intro.intro
ι : 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 ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert b 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

Result:
case pos.intro.intro
ι : 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
⊢ ∃ i ∈ insert b t, I ≤ f i

Proof state:
case neg.inl
ι : 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 ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
hbs : b ∉ s
hse : s = ∅
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
subst hse

Result:
case neg.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
hp : ∀ i ∈ ∅, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑∅, ↑(f i)
has : a ∉ ∅
hbs : b ∉ ∅
⊢ ∃ i ∈ ∅, I ≤ f i

Proof state:
case neg.inr.intro.intro.intro
ι : 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 ⊆ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
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

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

Result:
case neg.inr.intro.intro.intro
ι : 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
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1

Proof state:
case pos
ι : 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 ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∈ s
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
obtain ⟨t, hat, rfl⟩ : ∃ t, a ∉ t ∧ insert a t = s :=
  ⟨s.erase a, Finset.not_mem_erase a s, Finset.insert_erase has⟩

Result:
case pos.intro.intro
ι : 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 ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
⊢ ∃ i ∈ insert a t, I ≤ f i

Proof state:
ι : 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
this : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ i ∈ s, I ≤ f i
aux : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ x, ∃ (_ : x ∈ s), I ≤ f x
⊢ ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
simp_rw [exists_prop] at aux

Result:
ι : 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
this aux : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ x ∈ s, I ≤ f x
⊢ ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Proof state:
case neg
ι : 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
⊢ ∃ i ∈ insert a t, I ≤ f i

Tactic:
rwa [Finset.exists_mem_insert]

Result:
no goals

Proof state:
ι : 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
this : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ i ∈ s, I ≤ f i
⊢ ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
have aux := fun h => (bex_def.2 <| this h)

Result:
ι : 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
this : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ i ∈ s, I ≤ f i
aux : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ x, ∃ (_ : x ∈ s), I ≤ f x
⊢ ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Proof state:
case neg.inr
ι : 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 ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
hbs : b ∉ s
hsne : s.Nonempty
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
obtain ⟨i, his⟩ := hsne

Result:
case neg.inr.intro
ι : 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 ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
hbs : b ∉ s
i : ι
his : i ∈ s
⊢ ∃ i ∈ s, I ≤ f i

Proof state:
case neg
ι : 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 ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
hbs : b ∉ s
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
rcases s.eq_empty_or_nonempty with hse | hsne

Result:
case neg.inl
ι : 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 ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
hbs : b ∉ s
hse : s = ∅
⊢ ∃ i ∈ s, I ≤ f i

case neg.inr
ι : 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 ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
hbs : b ∉ s
hsne : s.Nonempty
⊢ ∃ i ∈ s, I ≤ f i

Proof state:
ι : 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 ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
⊢ ∀ j ∈ t, (f j).IsPrime

Tactic:
intro j hj

Result:
ι : 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 ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
⊢ (f j).IsPrime

Proof state:
ι : 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 ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
⊢ (f j).IsPrime

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
  solve_by_elim only [Finset.mem_insert_of_mem, *]

Result:
no goals