awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have 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
Tactic: by_cases HI : (I : Set R) ⊆ f a ∪ f b ∪ ⋃ j ∈ (↑t : Set ι), f j
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
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_1 ∈ insert i t, I ≤ f i_1
have ih₁ : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
Tactic: specialize ih hp.2 hn HI
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos : ∀ (ih : I ≤ f a), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: rcases ih with (ih | ih | ⟨k, hkt, ih⟩)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos₁ : ∀ (ih : I ≤ f b), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: rcases ih with (ih | ih | ⟨k, hkt, ih⟩)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos₂ : ∀ (k : ι) (hkt : k ∈ t) (ih : I ≤ f k), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: rcases ih with (ih | ih | ⟨k, hkt, ih⟩)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos : ¬(I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1) → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos₄ : (¬I ≤ f a ∧ ¬I ≤ f b ∧ ∀ (i_1 : ι) (_ : i_1 ∈ insert i t), ¬I ≤ f i_1) → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos : ¬(I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1) → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos₄ : (¬I ≤ f a ∧ ¬I ≤ f b ∧ ∀ (i_1 : ι) (_ : i_1 ∈ insert i t), ¬I ≤ f i_1) → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos : I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: right
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos : ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: right
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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_1 ∈ insert i t, I ≤ f i_1
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ False
have 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
Tactic: rcases Set.not_subset.1 HI with ⟨s, hsI, hs⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ False
have 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
Tactic: rw [Finset.coe_insert, Set.biUnion_insert] at h
Cleared hypotheses: h, hp, Ht, Ha, Hb, Hi, this, r, hri, hr, hrb, hrI, hra, HI, s, hsI, hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
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)
⊢ False
have hsi : s ∈ f i
Tactic: have hsi : s ∈ f i := ((h hsI).resolve_left (mt Or.inl hs)).resolve_right (mt Or.inr hs)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ False
have neg : ∀ (ha : r + s ∈ (↑(f a) : Set R)), False
Tactic: rcases h (I.add_mem hrI hsI) with (⟨ha | hb⟩ | hi | ht)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ False
have neg₁ : ∀ (hb : r + s ∈ (↑(f b) : Set R)), False
Tactic: rcases h (I.add_mem hrI hsI) with (⟨ha | hb⟩ | hi | ht)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ False
have neg₂ : ∀ (hi : r + s ∈ (↑(f i) : Set R)), False
Tactic: rcases h (I.add_mem hrI hsI) with (⟨ha | hb⟩ | hi | ht)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ False
have neg₃ : ∀ (ht : Membership.mem (γ := Set R) (⋃ x ∈ (↑t : Set ι), (↑(f x) : Set R)) (r + s)), False
Tactic: rcases h (I.add_mem hrI hsI) with (⟨ha | hb⟩ | hi | ht)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
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)
⊢ False
have ht₁ : ∃ (i : ι) (_ : i ∈ (↑t : Set ι)), r + s ∈ (↑(f i) : Set R)
Tactic: rw [Set.mem_iUnion₂] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ False
have neg : ∀ (j : ι) (hjt : j ∈ (↑t : Set ι)) (hj : r + s ∈ (↑(f j) : Set R)), False
Tactic: rcases ht with ⟨j, hjt, hj⟩
Cleared hypotheses: ht