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 : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
h' : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f i) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
ih : I ≤ f a
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
exact Or.inl ih

Premises used: Or.inl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
h' : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f i) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
ih : I ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
Or.inr (Or.inr ⟨i, Finset.mem_insert_self i t, ih⟩)

Premises used: Finset.mem_insert_self, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
h' : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f i) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
ih : I ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
exact Or.inr (Or.inr ⟨i, Finset.mem_insert_self i t, ih⟩)

Premises used: Or.inr
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
h' : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f i) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
k : ι
hkt : k ∈ t
ih : I ≤ f k
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
Or.inr (Or.inr ⟨k, Finset.mem_insert_of_mem hkt, ih⟩)

Premises used: Finset.mem_insert_of_mem, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
h' : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f i) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
k : ι
hkt : k ∈ t
ih : I ≤ f k
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
exact Or.inr (Or.inr ⟨k, Finset.mem_insert_of_mem hkt, ih⟩)

Premises used: 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
pos : ∀ (Hi : I ≤ f i), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
neg : ∀ (Hi : ¬I ≤ f i), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
by_cases Hi : I ≤ f i
-- 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
Or.inr (Or.inr ⟨i, Finset.mem_insert_self i t, Hi⟩)

Premises used: Finset.mem_insert_self, And.intro, Exists.intro, 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
exact Or.inr (Or.inr ⟨i, Finset.mem_insert_self i t, Hi⟩)

Premises used: 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
simp : ((¬I ≤ f i ∧ ¬f a ≤ f i) ∧ ¬f b ≤ f i) ∧ ¬∃ i_1 ∈ t, f i_1 ≤ f i
⊢ ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i

Tactic:
simp only [hp.1.inf_le, hp.1.inf_le', not_or]

Premises used: Ideal.IsPrime.inf_le, Ideal.IsPrime.inf_le', not_or, And.left
-- 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
⊢ ((¬I ≤ f i ∧ ¬f a ≤ f i) ∧ ¬f b ≤ f i) ∧ ¬∃ i_1 ∈ t, f i_1 ≤ f i

Tactic:
⟨⟨⟨Hi, Ha⟩, Hb⟩, Ht⟩

Premises used: And.intro
-- 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
⊢ ((¬I ≤ f i ∧ ¬f a ≤ f i) ∧ ¬f b ≤ f i) ∧ ¬∃ i_1 ∈ t, f i_1 ≤ f i

Tactic:
exact ⟨⟨⟨Hi, Ha⟩, Hb⟩, Ht⟩
-- 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
⊢ ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i

Tactic:
have : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i := by
      simp only [hp.1.inf_le, hp.1.inf_le', not_or]
      exact ⟨⟨⟨Hi, Ha⟩, Hb⟩, Ht⟩
-- 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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
neg :
  ∀ (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)), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
rcases Set.not_subset.1 this with ⟨r, ⟨⟨⟨hrI, hra⟩, hrb⟩, hr⟩, hri⟩

Premises used: Set.not_subset, Iff.mp
-- 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
pos :
  ∀ (HI : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)),
    I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
neg :
  ∀ (HI : ¬(↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)),
    I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
by_cases HI : (I : Set R) ⊆ f a ∪ f b ∪ ⋃ j ∈ (↑t : Set ι), f j

Premises used: SetLike.coe
-- 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ t, I ≤ f i

Tactic:
specialize ih hp.2 hn HI

Premises used: And.right
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
ih : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
pos : ∀ (ih : I ≤ f a), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
pos₁ : ∀ (ih : I ≤ f b), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
pos₂ : ∀ (k : ι) (hkt : k ∈ t) (ih : I ≤ f k), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
rcases ih with (ih | ih | ⟨k, hkt, ih⟩)
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
ih : I ≤ f a
pos pos₁ pos₂ pos₃ : ¬(I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1) → False
pos₄ pos₅ pos₆ pos₇ pos₈ pos₉ pos₁₀ pos₁₁ :
  (¬I ≤ f a ∧ ¬I ≤ f b ∧ ∀ (i_1 : ι) (_ : i_1 ∈ insert i t), ¬I ≤ f i_1) → False
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
order
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
ih : I ≤ f b
pos pos₁ pos₂ pos₃ : ¬(I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1) → False
pos₄ pos₅ pos₆ pos₇ pos₈ pos₉ pos₁₀ pos₁₁ :
  (¬I ≤ f a ∧ ¬I ≤ f b ∧ ∀ (i_1 : ι) (_ : i_1 ∈ insert i t), ¬I ≤ f i_1) → False
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
order
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
k : ι
hkt : k ∈ t
ih : I ≤ f k
pos : I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
right
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
k : ι
hkt : k ∈ t
ih : I ≤ f k
pos : ∃ i_1 ∈ insert i t, I ≤ f i_1
⊢ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
right
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
k : ι
hkt : k ∈ t
ih : I ≤ f k
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
⟨k, Finset.mem_insert_of_mem hkt, ih⟩

Premises used: Finset.mem_insert_of_mem, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
k : ι
hkt : k ∈ t
ih : I ≤ f k
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
exact ⟨k, Finset.mem_insert_of_mem hkt, ih⟩
-- 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
neg : False
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
exfalso
-- 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
neg :
  ∀ (s : R) (hsI : s ∈ (↑I : Set R))
    (hs : s ∉ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)), False
⊢ False

Tactic:
rcases Set.not_subset.1 HI with ⟨s, hsI, hs⟩

Premises used: Set.not_subset, Iff.mp
-- 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) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : 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)
neg :
  ∀ (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)),
    False
⊢ False

Tactic:
rw [Finset.coe_insert, Set.biUnion_insert] at h

Premises used: Set.biUnion_insert, Finset.coe_insert
-- 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)
⊢ s ∈ f i

Tactic:
have hsi : s ∈ f i := ((h hsI).resolve_left (mt Or.inl hs)).resolve_right (mt Or.inr hs)