awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
⊢ IsRadical.{u_2} (R := R) ⊥

Tactic:
fun _ hx => hx.recOn fun _ hn => eq_zero_of_pow_eq_zero hn

Premises used: Ideal.IsRadical, Exists.recOn
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
⊢ Eq.{u + 1} (α := Ideal R) (radical ⊥) ⊥

Tactic:
eq_bot_iff.2 isRadical_bot_of_noZeroDivisors

Premises used: Iff.mpr, Ideal.isRadical_bot_of_noZeroDivisors, eq_bot_iff
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
h : Ne (α := ℕ) 1 0
⊢ (HPow.hPow (β := ℕ) I 1).radical = I.radical

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
n : ℕ
h : n + 2 ≠ 0
rw : (I ^ (n + 1) * I).radical = I.radical
rw₁ : (I ^ (n + 1)).radical ⊓ I.radical = I.radical
rw₂ : I.radical ⊓ I.radical = I.radical
rw₃ rw₄ : I.radical = I.radical
⊢ (I ^ (n + 2)).radical = I.radical

Tactic:
rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]

Premises used: pow_succ, Nat.succ_ne_zero, inf_idem, Ideal.radical_mul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
rw : (∀ r ∈ I, ∀ s ∈ J, r * s ∈ P) ↔ J ≤ P ∨ I ≤ P
⊢ I * J ≤ P ↔ I ≤ P ∨ J ≤ P

Tactic:
rw [or_comm, Ideal.mul_le]

Premises used: Ideal.mul_le, or_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
simp_rw : (∀ r ∈ I, ∀ s ∈ J, r ∈ P ∨ s ∈ P) ↔ J ≤ P ∨ I ≤ P
simp_rw₁ : (∀ r ∈ I, ∀ s ∈ J, r ∈ P ∨ s ∈ P) ↔ (∀ ⦃x : R⦄, x ∈ J → x ∈ P) ∨ ∀ ⦃x : R⦄, x ∈ I → x ∈ P
simp_rw₂ : (∀ r ∈ I, ∀ s ∈ J, r ∈ P ∨ s ∈ P) ↔ ∀ (x : R) (x_1 : x ∈ I), (∀ ⦃x : R⦄, x ∈ J → x ∈ P) ∨ x ∈ P
simp_rw₃ : (∀ r ∈ I, ∀ s ∈ J, r ∈ P ∨ s ∈ P) ↔ ∀ (x : R) (x_1 : x ∈ I), x ∈ P ∨ ∀ ⦃x : R⦄, x ∈ J → x ∈ P
⊢ (∀ r ∈ I, ∀ s ∈ J, r * s ∈ P) ↔ J ≤ P ∨ I ≤ P

Tactic:
simp_rw [hp.mul_mem_iff_mem_or_mem, SetLike.le_def, ← forall_or_left, or_comm, forall_or_left]

Premises used: SetLike.le_def, forall_or_left, or_comm, Ideal.IsPrime.mul_mem_iff_mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ I ⊓ J ≤ P ↔ I ≤ P ∨ J ≤ P

Tactic:
⟨fun h ↦ hp.mul_le.1 <| mul_le_inf.trans h, fun h ↦ h.elim inf_le_left.trans inf_le_right.trans⟩

Premises used: inf_le_right, Ideal.IsPrime.mul_le, Iff.intro, Iff.mp, Ideal.mul_le_inf, inf_le_left, LE.le.trans, Or.elim
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
s : Multiset (Ideal R)
P : Ideal R
hp : P.IsPrime
⊢ Multiset.prod 0 ≤ P ↔ ∃ (I : Ideal R), Membership.mem (γ := Multiset (Ideal R)) 0 I ∧ I ≤ P

Tactic:
simp [hp.ne_top]

Premises used: Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
s_1 : Multiset (Ideal R)
P : Ideal R
hp : P.IsPrime
I : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ P ↔ ∃ I ∈ s, I ≤ P
⊢ (I ::ₘ s).prod ≤ P ↔ ∃ I_1 ∈ I ::ₘ s, I_1 ≤ P

Tactic:
simp [hp.mul_le, ih]

Premises used: Ideal.IsPrime.mul_le
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Multiset ι
f : ι → Ideal R
P : Ideal R
hp : P.IsPrime
simp_rw : (∃ I ∈ Multiset.map f s, I ≤ P) ↔ ∃ i ∈ s, f i ≤ P
simp_rw₁ : (∃ (I : Ideal R), (∃ a ∈ s, f a = I) ∧ I ≤ P) ↔ ∃ i ∈ s, f i ≤ P
⊢ (Multiset.map f s).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P

Tactic:
simp_rw [hp.multiset_prod_le, Multiset.mem_map, exists_exists_and_eq_and]

Premises used: Multiset.mem_map, Ideal.IsPrime.multiset_prod_le, exists_exists_and_eq_and
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Multiset R
⊢ s.prod ∈ I ↔ ∃ p ∈ s, p ∈ I

Tactic:
simpa using (hI.multiset_prod_map_le (span {·}))

Premises used: Ideal.IsPrime.multiset_prod_map_le, Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
⊢ (Multiset.replicate n I).prod ≤ P ↔ ∃ I_1 ∈ Multiset.replicate n I, I_1 ≤ P

Tactic:
have h : (Multiset.replicate n I).prod ≤ P ↔ _ := hP.multiset_prod_le
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
h : (Multiset.replicate n I).prod ≤ P ↔ ∃ I_1 ∈ Multiset.replicate n I, I_1 ≤ P
⊢ I ^ n ≤ P ↔ I ≤ P

Tactic:
simp_rw [Multiset.prod_replicate, Multiset.mem_replicate, ne_eq, hn, not_false_eq_true,
    true_and, exists_eq_left] at h

Premises used: Multiset.prod_replicate, exists_eq_left, ne_eq, Multiset.mem_replicate, not_false_eq_true, true_and
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
h : I ^ n ≤ P ↔ I ≤ P
⊢ I ^ n ≤ P ↔ I ≤ P

Tactic:
h

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
h : I ^ n ≤ P ↔ I ≤ P
⊢ I ^ n ≤ P ↔ I ≤ P

Tactic:
exact h
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
pos : ∀ (hn : n = 0), I ≤ P
neg : ∀ (hn : ¬n = 0), I ≤ P
⊢ I ≤ P

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : n = 0
⊢ ⊤ ≤ P

Tactic:
rw [hn, pow_zero, one_eq_top] at h

Premises used: Ideal.one_eq_top, pow_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : n = 0
h₁ : ⊤ ≤ P
⊢ n = 0

Tactic:
rw [hn, pow_zero, one_eq_top] at h

Premises used: Ideal.one_eq_top, pow_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : ⊤ ≤ P
hn : n = 0
⊢ I ≤ P

Tactic:
fun ⦃_⦄ _ ↦ h Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : ⊤ ≤ P
hn : n = 0
⊢ I ≤ P

Tactic:
exact fun ⦃_⦄ _ ↦ h Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : ¬n = 0
⊢ I ≤ P

Tactic:
(pow_le_iff hn).mp h

Premises used: Ideal.IsPrime.pow_le_iff, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : ¬n = 0
⊢ I ≤ P

Tactic:
exact (pow_le_iff hn).mp h

Premises used: Ideal.IsPrime.pow_le_iff, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
f : ι → Ideal R
P : Ideal R
hp : P.IsPrime
⊢ s.prod f ≤ P ↔ ∃ i ∈ s, f i ≤ P

Tactic:
hp.multiset_prod_map_le f

Premises used: Set.Mem, setOf, Ideal.IsPrime.multiset_prod_map_le, Multiset.Mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
x : ι → R
p : Ideal R
hp : p.IsPrime
simp_rw : ∏ i ∈ s, span {x i} ≤ p ↔ ∃ i ∈ s, span {x i} ≤ p
⊢ ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p

Tactic:
simp_rw [← span_singleton_le_iff_mem, ← prod_span_singleton]

Premises used: Ideal.span_singleton_le_iff_mem, Ideal.prod_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
x : ι → R
p : Ideal R
hp : p.IsPrime
⊢ ∏ i ∈ s, span {x i} ≤ p ↔ ∃ i ∈ s, span {x i} ≤ p

Tactic:
hp.prod_le

Premises used: Ideal.IsPrime.prod_le, Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
x : ι → R
p : Ideal R
hp : p.IsPrime
⊢ ∏ i ∈ s, span {x i} ≤ p ↔ ∃ i ∈ s, span {x i} ≤ p

Tactic:
exact hp.prod_le

Premises used: Ideal.IsPrime.prod_le
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
rw : s.val.prod ∈ I ↔ ∃ p ∈ s, p ∈ I
⊢ ∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I

Tactic:
rw [Finset.prod_eq_multiset_prod, Multiset.map_id']

Premises used: Finset.prod_eq_multiset_prod, Multiset.map_id'
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
⊢ s.val.prod ∈ I ↔ ∃ p ∈ s, p ∈ I

Tactic:
hI.multiset_prod_mem_iff_exists_mem s.val

Premises used: Set.Mem, setOf, Finset.val, Multiset.Mem, Ideal.IsPrime.multiset_prod_mem_iff_exists_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
⊢ s.val.prod ∈ I ↔ ∃ p ∈ s, p ∈ I

Tactic:
exact hI.multiset_prod_mem_iff_exists_mem s.val

Premises used: Finset.val, Ideal.IsPrime.multiset_prod_mem_iff_exists_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
f : ι → Ideal R
P : Ideal R
hp : P.IsPrime
⊢ s.inf f ≤ P ↔ ∃ i ∈ s, f i ≤ P

Tactic:
⟨fun h ↦ hp.prod_le.1 <| prod_le_inf.trans h, fun ⟨_, his, hip⟩ ↦ (Finset.inf_le his).trans hip⟩

Premises used: Ideal.IsPrime.prod_le, Ideal.prod_le_inf, LE.le, Iff.intro, Iff.mp, LE.le.trans, Finset.inf_le, Finset.inf, _private.0.Ideal.IsPrime.inf_le'.match_1
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
f : ι → Ideal R
hp : (s.inf f).IsPrime
⊢ ∃ i ∈ s, f i = s.inf f

Tactic:
(hp.inf_le'.mp le_rfl).imp (fun _ ⟨h1, h2⟩ ↦ ⟨h1, le_antisymm h2 (Finset.inf_le h1)⟩)

Premises used: le_rfl, Ideal.IsPrime.inf_le', Exists.imp, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsPrime
x y : R
h : IsCoprime x y
hx : x ∈ I
⊢ y ∉ I

Tactic:
fun hy ↦
  have ⟨a, b, e⟩ := h
  Ideal.IsPrime.one_notMem ‹_› (e ▸ I.add_mem (I.mul_mem_left a hx) (I.mul_mem_left b hy))

Premises used: False, _private.0.Ideal.sup_eq_top_iff_isCoprime.match_1, Ideal.IsPrime.one_notMem, Not
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Ring R
I J K : Ideal R
⊢ (↑I : Set R) ⊆ (↑J : Set R) ∪ (↑K : Set R) ↔ I ≤ J ∨ I ≤ K

Tactic:
AddSubgroupClass.subset_union

Premises used: AddSubgroupClass.subset_union
-- 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, (f i).IsPrime
I : Ideal R
this :
  (↑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
h_1 : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h : I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h_2 : ∃ i ∈ s, I ≤ f i
i : ι
his : i ∈ s
hi : I ≤ f i
⊢ (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)

Tactic:
Set.Subset.trans hi <| Set.Subset.trans ?_ Set.subset_union_right

Premises used: Set.Subset.trans, Set.subset_union_right
-- 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, (f i).IsPrime
I : Ideal R
this :
  (↑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
h_1 : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h : I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h_2 : ∃ i ∈ s, I ≤ f i
i : ι
his : i ∈ s
hi : I ≤ f i
refine : (↑(f i) : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
⊢ (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)

Tactic:
refine Set.Subset.trans hi <| Set.Subset.trans ?_ Set.subset_union_right

Premises used: Set.Subset.trans, Set.subset_union_right
-- 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, (f i).IsPrime
I : Ideal R
this :
  (↑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
h_1 : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h : I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h_2 : ∃ i ∈ s, I ≤ f i
i : ι
his : i ∈ s
hi : I ≤ f i
⊢ (↑(f i) : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)

Tactic:
Set.subset_biUnion_of_mem (u := fun x ↦ (f x : Set R)) (Finset.mem_coe.2 his)

Premises used: Iff.mpr, Set.subset_biUnion_of_mem, Finset.mem_coe
-- 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, (f i).IsPrime
I : Ideal R
this :
  (↑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
h_1 : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h : I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h_2 : ∃ i ∈ s, I ≤ f i
i : ι
his : i ∈ s
hi : I ≤ f i
⊢ (↑(f i) : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)

Tactic:
exact Set.subset_biUnion_of_mem (u := fun x ↦ (f x : Set R)) (Finset.mem_coe.2 his)

Premises used: Iff.mpr, Set.subset_biUnion_of_mem, Finset.mem_coe
-- 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, (f i).IsPrime
I : Ideal R
Set :
  (↑I : _root_.Set R) ⊆
      (↑(f a) : _root_.Set R) ∪ (↑(f b) : _root_.Set R) ∪ ⋃ i ∈ (↑s : _root_.Set ι), (↑(f i) : _root_.Set R) →
    I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
⊢ (↑I : _root_.Set R) ⊆
      (↑(f a) : _root_.Set R) ∪ (↑(f b) : _root_.Set R) ∪ ⋃ i ∈ (↑s : _root_.Set ι), (↑(f i) : _root_.Set R) ↔
    I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
suffices
    ((I : Set R) ⊆ f a ∪ f b ∪ ⋃ i ∈ (↑s : Set ι), f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i from
    ⟨this, fun h =>
      Or.casesOn h
        (fun h =>
          Set.Subset.trans h <|
            Set.Subset.trans Set.subset_union_left Set.subset_union_left)
        fun h =>
        Or.casesOn h
          (fun h =>
            Set.Subset.trans h <|
              Set.Subset.trans Set.subset_union_right Set.subset_union_left)
          fun ⟨i, his, hi⟩ => by
          refine Set.Subset.trans hi <| Set.Subset.trans ?_ Set.subset_union_right
          exact Set.subset_biUnion_of_mem (u := fun x ↦ (f x : Set R)) (Finset.mem_coe.2 his)⟩
-- 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, (f i).IsPrime
I : Ideal R
generalize :
  ∀ (n : ℕ) (hn : s.card = n),
    (↑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
⊢ (↑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

Tactic:
generalize hn : s.card = n

Premises used: Finset.card
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
s : Finset ι
a b : ι
hn : s.card = 0
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
⊢ s = ∅

Tactic:
rw [Finset.card_eq_zero] at hn

Premises used: Finset.card_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
s : Finset ι
a b : ι
hn : s.card = 0
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
hn₁ : s = ∅
⊢ (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)

Tactic:
rw [Finset.card_eq_zero] at hn

Premises used: Finset.card_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
s : Finset ι
a b : ι
hn : s = ∅
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
zero :
  ∀ (h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑∅ : Set ι), (↑(f i) : Set R)),
    I ≤ f a ∨ I ≤ f b ∨ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ I ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
subst hn
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
a b : ι
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑∅ : Set ι), (↑(f i) : Set R)
⊢ I ≤ f a ∨ I ≤ f b

Tactic:
rw [Finset.coe_empty, Set.biUnion_empty, Set.union_empty, subset_union] at h

Premises used: Ideal.subset_union, Finset.coe_empty, Set.union_empty, Set.biUnion_empty
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
a b : ι
h : I ≤ f a ∨ I ≤ f b
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ I ≤ f i

Tactic:
simpa only [exists_prop, Finset.notMem_empty, false_and, exists_false, or_false]

Premises used: false_and, exists_prop, Finset.notMem_empty, exists_false, or_false
-- 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
s : Finset ι
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
hn : s.card = n + 1
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
⊢ ∃ (i : ι) (t : Finset ι), i ∉ t ∧ insert i t = s ∧ t.card = n

Tactic:
replace hn : ∃ (i : ι) (t : Finset ι), i ∉ t ∧ insert i t = s ∧ t.card = n :=
      Finset.card_eq_succ.1 hn
-- 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
s : Finset ι
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
hn : ∃ (i : ι) (t : Finset ι), i ∉ t ∧ insert i t = s ∧ t.card = n
succ :
  ∀ (i : ι) (t : Finset ι) (hit : i ∉ t) (hn : t.card = n) (hp : ∀ i_1 ∈ insert i t, (f i_1).IsPrime)
    (h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R)),
    I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
rcases hn with ⟨i, t, hit, rfl, hn⟩

Premises used: rfl
-- 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
hp : ∀ i_1 ∈ insert i t, (f i_1).IsPrime
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R)
⊢ (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime

Tactic:
replace hp : IsPrime (f i) ∧ ∀ x ∈ t, IsPrime (f x) := (t.forall_mem_insert _ _).1 hp
-- 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
pos : ∀ (Ht : ∃ j ∈ t, f j ≤ f i), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
neg : ∀ (Ht : ¬∃ j ∈ t, f j ≤ 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 Ht : ∃ j ∈ t, f j ≤ 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
⊢ ∃ j ∈ t, f j ≤ f i

Tactic:
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
pos : ∀ (j : ι) (hjt : j ∈ t) (hfji : f j ≤ 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:
obtain ⟨j, hjt, hfji⟩ : ∃ j ∈ t, f j ≤ f i := 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
j : ι
hjt : j ∈ t
hfji : f j ≤ f i
⊢ ∃ (u : Finset ι), j ∉ u ∧ insert j u = t

Tactic:
⟨t.erase j, t.notMem_erase j, Finset.insert_erase hjt⟩

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
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
j : ι
hjt : j ∈ t
hfji : f j ≤ f i
pos :
  ∀ (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),
    I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i (insert j u), I ≤ f i_1
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
obtain ⟨u, hju, rfl⟩ : ∃ u, j ∉ u ∧ insert j u = t :=
        ⟨t.erase j, t.notMem_erase j, Finset.insert_erase hjt⟩

Premises used: rfl
-- 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 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
rw :
  ∀ (hp : (f i).IsPrime ∧ (f j).IsPrime ∧ ∀ x ∈ u, (f x).IsPrime) (hjt : j ∈ insert j u),
    (f i).IsPrime ∧ ∀ x ∈ u, (f x).IsPrime
⊢ ∀ k ∈ insert i u, (f k).IsPrime

Tactic:
rw [Finset.forall_mem_insert] at hp ⊢

Premises used: Finset.forall_mem_insert