awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ insert i (↑(insert j u) : Set ι), (↑(f i_1) : Set R)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
⊢ (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ k ∈ insert i (↑u : Set ι), (↑(f k) : Set R)
have h₁ : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ insert i (insert j (↑u : Set ι)), (↑(f i_1) : Set R)
Tactic: rw [Finset.coe_insert] at h
Cleared hypotheses: h, hp, hjt, hp', hiu, hn'
-- 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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ insert i (insert j (↑u : Set ι)), (↑(f i_1) : Set R)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
⊢ (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ k ∈ insert i (↑u : Set ι), (↑(f k) : Set R)
have simp : ∀
  (h :
    (↑I : Set R) ⊆
      (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪
        ((↑(f i) : Set R) ∪ ((↑(f j) : Set R) ∪ ⋃ x ∈ (↑u : Set ι), (↑(f x) : Set R)))),
  (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ((↑(f i) : Set R) ∪ ⋃ x ∈ (↑u : Set ι), (↑(f x) : Set R))
Tactic: simp only [Set.biUnion_insert] at h ⊢
Cleared hypotheses: h
-- 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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i (insert j u)) : Set ι), (↑(f i_1) : Set R)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i (insert j u), I ≤ f i_1
have h' : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ k ∈ (↑(insert i u) : Set ι), (↑(f k) : Set R)
Tactic: have h' : (I : Set R) ⊆ f a ∪ f b ∪ ⋃ k ∈ (↑(insert i u) : Set ι), f k := by
        rw [Finset.coe_insert] at h ⊢
        rw [Finset.coe_insert] at h
        simp only [Set.biUnion_insert] at h ⊢
        rw [← Set.union_assoc (f i : Set R),
            Set.union_eq_self_of_subset_right hfji] at h
        exact h
-- 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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i (insert j u)) : Set ι), (↑(f i_1) : Set R)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
h' : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ k ∈ (↑(insert i u) : Set ι), (↑(f k) : Set R)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i (insert j u), I ≤ f i_1
have ih₁ : I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i u, I ≤ f i_1
Tactic: specialize ih hp' hn' h'
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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i (insert j u)) : Set ι), (↑(f i_1) : Set R)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
h' : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ k ∈ (↑(insert i u) : Set ι), (↑(f k) : Set R)
ih : I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i u, I ≤ f i_1
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i (insert j u), I ≤ f i_1
have pos : ∀ (k : ι), k ∈ insert i u ∧ I ≤ f k → k ∈ insert i (insert j u) ∧ I ≤ f k
Tactic: refine ih.imp id (Or.imp id (Exists.imp fun k => ?_))
-- 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos : ∀ (Ha : f a ≤ f i), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: by_cases Ha : f a ≤ f i
-- 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
pos : ∀ (Ha : f a ≤ 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
have neg : ∀ (Ha : ¬f a ≤ f i), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: by_cases Ha : f a ≤ f i
-- 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have h' : (↑I : Set R) ⊆ (↑(f i) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
Tactic: have h' : (I : Set R) ⊆ f i ∪ f b ∪ ⋃ j ∈ (↑t : Set ι), f j := by
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_assoc,
          Set.union_right_comm (f a : Set R),
          Set.union_eq_self_of_subset_left Ha] at h
        exact h
-- 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
h' : (↑I : Set R) ⊆ (↑(f i) : 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 i ∨ I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
Tactic: specialize ih hp.2 hn h'
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
h' : (↑I : Set R) ⊆ (↑(f i) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
ih : I ≤ f i ∨ 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 : 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
h' : (↑I : Set R) ⊆ (↑(f i) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
ih : I ≤ f i ∨ I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
⊢ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos : ∀ (ih : I ≤ f i), 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
h' : (↑I : Set R) ⊆ (↑(f i) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
ih : I ≤ f i ∨ I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
pos : ∀ (ih : I ≤ f i), I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
⊢ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos₁ : ∀ (ih : I ≤ f b), 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
h' : (↑I : Set R) ⊆ (↑(f i) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
ih : I ≤ f i ∨ I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
pos : ∀ (ih : I ≤ f i), I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
pos₁ : ∀ (ih : I ≤ f b), I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
⊢ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos₂ : ∀ (k : ι) (hkt : k ∈ t) (ih : I ≤ f k), 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 : ℕ
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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos : ∀ (Hb : f b ≤ f i), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: by_cases Hb : f b ≤ f i
-- 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
pos : ∀ (Hb : f b ≤ 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
have neg : ∀ (Hb : ¬f b ≤ f i), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: by_cases Hb : f b ≤ f i
-- 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have h' : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f i) : Set R) ∪ ⋃ j ∈ (↑t : Set ι), (↑(f j) : Set R)
Tactic: have h' : (I : Set R) ⊆ f a ∪ f i ∪ ⋃ j ∈ (↑t : Set ι), f j := by
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_assoc,
          Set.union_assoc (f a : Set R),
          Set.union_eq_self_of_subset_left Hb] at h
        exact h
-- 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
h' : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f i) : 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 i ∨ ∃ i ∈ t, I ≤ f i
Tactic: specialize ih hp.2 hn h'
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
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 i ∨ ∃ 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
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 i ∨ ∃ 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 i), 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
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 i ∨ ∃ 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 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
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 : ℕ
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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos : ∀ (Hi : I ≤ f i), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: by_cases Hi : I ≤ f i
-- 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
pos : ∀ (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
have neg : ∀ (Hi : ¬I ≤ f i), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: by_cases Hi : I ≤ f i
-- 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
⊢ ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
have simp : ((¬I ≤ f i ∧ ¬f a ≤ f i) ∧ ¬f b ≤ f i) ∧ ¬∃ i_1 ∈ t, f i_1 ≤ f i
Tactic: simp only [hp.1.inf_le, hp.1.inf_le', not_or]
-- 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have this : ¬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⟩
-- 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have 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
Tactic: rcases Set.not_subset.1 this with ⟨r, ⟨⟨⟨hrI, hra⟩, hrb⟩, hr⟩, hri⟩
-- 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)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have 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
Tactic: by_cases HI : (I : Set R) ⊆ f a ∪ f b ∪ ⋃ j ∈ (↑t : Set ι), f j