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
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
neg : ∀ (ha : r + s ∈ (↑(f a) : Set R)), False
neg₁ : ∀ (hb : r + s ∈ (↑(f b) : Set R)), False
neg₂ : ∀ (hi : r + s ∈ (↑(f i) : Set R)), False
neg₃ : ∀ (ht : Membership.mem (γ := Set R) (⋃ x ∈ (↑t : Set ι), (↑(f x) : Set R)) (r + s)), False
⊢ False

Tactic:
rcases h (I.add_mem hrI hsI) with (⟨ha | hb⟩ | hi | ht)

Premises used: Ideal.add_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
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
ha : r + s ∈ (↑(f a) : Set R)
⊢ False

Tactic:
hs (Or.inl <| Or.inl <| add_sub_cancel_left r s ▸ (f a).sub_mem ha hra)

Premises used: add_sub_cancel_left, Eq.rec, Ideal.sub_mem, Or.inl
-- Module: Mathlib.RingTheory.Ideal.Operations
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
ha : r + s ∈ (↑(f a) : Set R)
⊢ False

Tactic:
exact hs (Or.inl <| Or.inl <| add_sub_cancel_left r s ▸ (f a).sub_mem ha hra)

Premises used: add_sub_cancel_left, Eq.rec, Ideal.sub_mem, Or.inl
-- Module: Mathlib.RingTheory.Ideal.Operations
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
hb : r + s ∈ (↑(f b) : Set R)
⊢ False

Tactic:
hs (Or.inl <| Or.inr <| add_sub_cancel_left r s ▸ (f b).sub_mem hb hrb)

Premises used: add_sub_cancel_left, Eq.rec, Ideal.sub_mem, Or.inl, Or.inr
-- Module: Mathlib.RingTheory.Ideal.Operations
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
hb : r + s ∈ (↑(f b) : Set R)
⊢ False

Tactic:
exact hs (Or.inl <| Or.inr <| add_sub_cancel_left r s ▸ (f b).sub_mem hb hrb)

Premises used: add_sub_cancel_left, Eq.rec, Ideal.sub_mem, Or.inl, Or.inr
-- Module: Mathlib.RingTheory.Ideal.Operations
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
hi : r + s ∈ (↑(f i) : Set R)
⊢ False

Tactic:
hri (add_sub_cancel_right r s ▸ (f i).sub_mem hi hsi)

Premises used: Eq.rec, Ideal.sub_mem, add_sub_cancel_right
-- Module: Mathlib.RingTheory.Ideal.Operations
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
hi : r + s ∈ (↑(f i) : Set R)
⊢ False

Tactic:
exact hri (add_sub_cancel_right r s ▸ (f i).sub_mem hi hsi)

Premises used: Eq.rec, Ideal.sub_mem, add_sub_cancel_right
-- Module: Mathlib.RingTheory.Ideal.Operations
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
ht : Membership.mem (γ := Set R) (⋃ x ∈ (↑t : Set ι), (↑(f x) : Set R)) (r + s)
⊢ ∃ (i : ι) (_ : i ∈ (↑t : Set ι)), r + s ∈ (↑(f i) : Set R)

Tactic:
rw [Set.mem_iUnion₂] at ht

Premises used: Set.mem_iUnion₂
-- Module: Mathlib.RingTheory.Ideal.Operations
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
ht : ∃ (i : ι) (_ : i ∈ (↑t : Set ι)), r + s ∈ (↑(f i) : Set R)
neg : ∀ (j : ι) (hjt : j ∈ (↑t : Set ι)) (hj : r + s ∈ (↑(f j) : Set R)), False
⊢ False

Tactic:
rcases ht with ⟨j, hjt, hj⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
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)
⊢ ∀ (i : ι) (i_1 : i ∈ t), r ∈ f i

Tactic:
simp only [Finset.inf_eq_iInf, SetLike.mem_coe, Submodule.mem_iInf] at hr

Premises used: Submodule.mem_iInf, SetLike.mem_coe, Finset.inf_eq_iInf
-- Module: Mathlib.RingTheory.Ideal.Operations
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)
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)
hr : ∀ (i : ι) (i_1 : i ∈ t), r ∈ f i
⊢ False

Tactic:
hs <| Or.inr <| Set.mem_biUnion hjt <|
        add_sub_cancel_left r s ▸ (f j).sub_mem hj <| hr j hjt

Premises used: Set.mem_biUnion, Or.inr
-- Module: Mathlib.RingTheory.Ideal.Operations
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)
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)
hr : ∀ (i : ι) (i_1 : i ∈ t), r ∈ f i
⊢ False

Tactic:
exact hs <| Or.inr <| Set.mem_biUnion hjt <|
        add_sub_cancel_left r s ▸ (f j).sub_mem hj <| hr j hjt

Premises used: Set.mem_biUnion, Or.inr
-- 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)
pos : ∀ (has : a ∈ s), ∃ i ∈ s, I ≤ f i
neg : ∀ (has : a ∉ s), ∃ i ∈ s, I ≤ f i
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
by_cases has : a ∈ 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
⊢ ∃ (t : Finset ι), a ∉ t ∧ insert a t = s

Tactic:
⟨s.erase a, Finset.notMem_erase a s, Finset.insert_erase has⟩

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
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
⊢ ∃ i ∈ s, 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⟩

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 ι
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
neg : ∀ (hbt : b ∉ t), ∃ i ∈ insert a t, I ≤ f i
⊢ ∃ i ∈ insert a t, I ≤ f i

Tactic:
by_cases hbt : b ∈ t
-- 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
⊢ ∃ (u : Finset ι), b ∉ u ∧ insert b u = t

Tactic:
⟨t.erase b, Finset.notMem_erase b t, Finset.insert_erase hbt⟩

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
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
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
⊢ ∃ i ∈ insert a t, 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⟩

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
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

Tactic:
hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_

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
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
refine_2 : i ≠ b
⊢ (f i).IsPrime

Tactic:
refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_

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
u : Finset ι
hbu : b ∉ u
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
hat : i ∉ insert b u
hp : ∀ i_1 ∈ insert i (insert b u), i_1 ≠ i → i_1 ≠ b → (f i_1).IsPrime
h : (↑I : Set R) ⊆ ⋃ i_1 ∈ (↑(insert i (insert b u)) : Set ι), (↑(f i_1) : Set R)
has : i ∈ insert i (insert b u)
⊢ 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
u : Finset ι
i : ι
hiu : i ∈ u
hbu : i ∉ u
hat : a ∉ insert i u
hp : ∀ i_1 ∈ insert a (insert i u), i_1 ≠ a → i_1 ≠ i → (f i_1).IsPrime
h : (↑I : Set R) ⊆ ⋃ i_1 ∈ (↑(insert a (insert i u)) : Set ι), (↑(f i_1) : Set R)
has : a ∈ insert a (insert i u)
hbt : i ∈ insert i u
⊢ 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
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 ∈ 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, *]
-- 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 : 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 ≤ 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

Premises used: Ideal.subset_union_prime', Set.biUnion_insert, Set.union_assoc, Finset.coe_insert
-- 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 : 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
h₁ : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
⊢ a ∈ insert a (insert b u)

Tactic:
rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ←
          Set.union_assoc, subset_union_prime' hp'] at h

Premises used: Ideal.subset_union_prime', Set.biUnion_insert, Set.union_assoc, Finset.coe_insert
-- 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 : 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
h₁ : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has₁ : a ∈ insert a (insert b u)
⊢ b ∈ insert b u

Tactic:
rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ←
          Set.union_assoc, subset_union_prime' hp'] at h

Premises used: Ideal.subset_union_prime', Set.biUnion_insert, Set.union_assoc, Finset.coe_insert
-- 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 : 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
h₁ : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has₁ : a ∈ insert a (insert b u)
hbt₁ : b ∈ insert b u
⊢ ∀ i ∈ u, (f i).IsPrime

Tactic:
rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ←
          Set.union_assoc, subset_union_prime' hp'] at h

Premises used: Ideal.subset_union_prime', Set.biUnion_insert, Set.union_assoc, Finset.coe_insert