Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg.inl.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → 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 ⊆ ↑(f a) ∪ ↑(f b) ∪ (↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x))
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)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
hsi : s ∈ f i
hb : r + s ∈ ↑(f b)
⊢ False

pp: case neg.inr.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → 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 ⊆ ↑(f a) ∪ ↑(f b) ∪ (↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x))
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)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
hsi : s ∈ f i
hi : r + s ∈ ↑(f i)
⊢ False

pp: case neg.inr.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → 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 ⊆ ↑(f a) ∪ ↑(f b) ∪ (↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x))
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)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
hsi : s ∈ f i
ht : r + s ∈ ⋃ x ∈ ↑t, ↑(f x)
⊢ False

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

Goal state after:
case neg.inr.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → 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 ⊆ ↑(f a) ∪ ↑(f b) ∪ (↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x))
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)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
hsi : s ∈ f i
hi : r + s ∈ ↑(f i)
⊢ False

case neg.inr.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → 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 ⊆ ↑(f a) ∪ ↑(f b) ∪ (↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x))
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)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
hsi : s ∈ f i
ht : r + s ∈ ⋃ x ∈ ↑t, ↑(f x)
⊢ False