awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
hIm : I ≤ ⊤
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) ⊤
hrm : r ∉ radical ⊤
this : ∀ x ∉ ⊤, Membership.mem (γ := Ideal R) (radical (⊤ ⊔ span {x})) r
⊢ False
have hrm₁ : r ∉ ⊤
Tactic: rw [radical_top] at hrm
Cleared hypotheses: hrm, this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
x y : R
hxym : x * y ∈ m
hxm : x ∉ m
hym : y ∉ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : Membership.mem (γ := Submodule R R) (span {x}) q
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : Membership.mem (γ := Submodule R R) (span {y}) g
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ r ^ (n + k) ∈ m
have rw : p * (f + d * y) + (c * x * f + c * d * (x * y)) ∈ m
Tactic: rw [pow_add, ← hpqrn, ← hcxq, ← hfgrk, ← hdyg, add_mul, mul_add (c * x),
                      mul_assoc c x (d * y), mul_left_comm x, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
n : ℕ
h : n + 2 ≠ 0
⊢ (I ^ (n + 2)).radical = I.radical
have rw : (I ^ (n + 1) * I).radical = I.radical
Tactic: rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
n : ℕ
h : n + 2 ≠ 0
rw : (I ^ (n + 1) * I).radical = I.radical
⊢ (I ^ (n + 2)).radical = I.radical
have rw₁ : (I ^ (n + 1)).radical ⊓ I.radical = I.radical
Tactic: rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ (I ^ (n + 2)).radical = I.radical
have rw₂ : I.radical ⊓ I.radical = I.radical
Tactic: rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ (I ^ (n + 2)).radical = I.radical
have rw₃ : I.radical = I.radical
Tactic: rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ I * J ≤ P ↔ I ≤ P ∨ J ≤ P
have rw : (∀ r ∈ I, ∀ s ∈ J, r * s ∈ P) ↔ J ≤ P ∨ I ≤ P
Tactic: rw [or_comm, Ideal.mul_le]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ (∀ r ∈ I, ∀ s ∈ J, r * s ∈ P) ↔ J ≤ P ∨ I ≤ P
have simp_rw : (∀ r ∈ I, ∀ s ∈ J, r ∈ P ∨ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ (∀ r ∈ I, ∀ s ∈ J, r * s ∈ P) ↔ J ≤ P ∨ I ≤ P
have simp_rw₁ : (∀ r ∈ I, ∀ s ∈ J, r ∈ P ∨ s ∈ P) ↔ (∀ ⦃x : R⦄, x ∈ J → x ∈ P) ∨ ∀ ⦃x : R⦄, x ∈ I → x ∈ P
Tactic: simp_rw [hp.mul_mem_iff_mem_or_mem, SetLike.le_def, ← forall_or_left, or_comm, forall_or_left]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ (∀ r ∈ I, ∀ s ∈ J, r * s ∈ P) ↔ J ≤ P ∨ I ≤ P
have simp_rw₂ : (∀ r ∈ I, ∀ s ∈ J, r ∈ P ∨ s ∈ P) ↔ ∀ (x : R) (x_1 : x ∈ I), (∀ ⦃x : R⦄, x ∈ J → x ∈ P) ∨ x ∈ P
Tactic: simp_rw [hp.mul_mem_iff_mem_or_mem, SetLike.le_def, ← forall_or_left, or_comm, forall_or_left]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ (∀ r ∈ I, ∀ s ∈ J, r * s ∈ P) ↔ J ≤ P ∨ I ≤ P
have simp_rw₃ : (∀ r ∈ I, ∀ s ∈ J, r ∈ P ∨ s ∈ P) ↔ ∀ (x : R) (x_1 : x ∈ I), x ∈ P ∨ ∀ ⦃x : R⦄, x ∈ J → x ∈ P
Tactic: simp_rw [hp.mul_mem_iff_mem_or_mem, SetLike.le_def, ← forall_or_left, or_comm, forall_or_left]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Multiset ι
f : ι → Ideal R
P : Ideal R
hp : P.IsPrime
⊢ (Multiset.map f s).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P
have simp_rw : (∃ I ∈ Multiset.map f s, I ≤ P) ↔ ∃ i ∈ s, f i ≤ P
Tactic: simp_rw [hp.multiset_prod_le, Multiset.mem_map, exists_exists_and_eq_and]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ (Multiset.map f s).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P
have simp_rw₁ : (∃ (I : Ideal R), (∃ a ∈ s, f a = I) ∧ I ≤ P) ↔ ∃ i ∈ s, f i ≤ P
Tactic: simp_rw [hp.multiset_prod_le, Multiset.mem_map, exists_exists_and_eq_and]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
⊢ I ^ n ≤ P ↔ I ≤ P
have h : (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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
⊢ I ≤ P
have pos : ∀ (hn : n = 0), I ≤ P
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ≤ P
have neg : ∀ (hn : ¬n = 0), I ≤ P
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : n = 0
⊢ I ≤ P
have h₁ : ⊤ ≤ P
Tactic: rw [hn, pow_zero, one_eq_top] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
x : ι → R
p : Ideal R
hp : p.IsPrime
⊢ ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p
have simp_rw : ∏ i ∈ s, span {x i} ≤ p ↔ ∃ i ∈ s, span {x i} ≤ p
Tactic: simp_rw [← span_singleton_le_iff_mem, ← prod_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
⊢ ∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I
have rw : s.val.prod ∈ I ↔ ∃ p ∈ s, p ∈ I
Tactic: rw [Finset.prod_eq_multiset_prod, Multiset.map_id']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
have refine : (↑(f i) : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
Tactic: refine Set.Subset.trans hi <| Set.Subset.trans ?_ Set.subset_union_right
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ (↑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
have Set : (↑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: 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)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ (↑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
have 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
Tactic: generalize hn : s.card = n
-- 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
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)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
have hn₁ : s = ∅
Tactic: rw [Finset.card_eq_zero] at hn
Cleared hypotheses: hn, h
-- 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
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)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
have 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
Tactic: subst hn
Cleared hypotheses: s, hn, 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
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 ∨ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ I ≤ f i
have h₁ : I ≤ f a ∨ I ≤ f b
Tactic: rw [Finset.coe_empty, Set.biUnion_empty, Set.union_empty, subset_union] 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
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 ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
have hn₁ : ∃ (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
Cleared hypotheses: 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
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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
have 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
Tactic: rcases hn with ⟨i, t, hit, rfl, hn⟩
Cleared hypotheses: s, hp, h, hn
-- 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
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
have hp₁ : (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
Cleared hypotheses: hp
-- 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have pos : ∀ (Ht : ∃ j ∈ t, f j ≤ f i), 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
-- 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
pos : ∀ (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
have neg : ∀ (Ht : ¬∃ j ∈ t, f j ≤ f i), 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
-- 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 : ∀ (j : ι) (hjt : j ∈ t) (hfji : f j ≤ f i), 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
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) ∪ ⋃ 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
have 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
Tactic: obtain ⟨u, hju, rfl⟩ : ∃ u, j ∉ u ∧ insert j u = t :=
        ⟨t.erase j, t.notMem_erase j, Finset.insert_erase hjt⟩
Cleared hypotheses: t, hit, hn, h, hp, hjt
-- 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
⊢ ∀ k ∈ insert i u, (f k).IsPrime
have 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
Tactic: rw [Finset.forall_mem_insert] at hp ⊢
Cleared hypotheses: hp, hjt
-- 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i (insert j u), I ≤ f i_1
have hp' : ∀ k ∈ insert i u, (f k).IsPrime
Tactic: have hp' : ∀ k ∈ insert i u, IsPrime (f k) := by
        rw [Finset.forall_mem_insert] at hp ⊢
        exact ⟨hp.1, hp.2.2⟩
-- 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i (insert j u), I ≤ f i_1
have hiu : i ∉ u
Tactic: have hiu : i ∉ u := mt Finset.mem_insert_of_mem hit
-- 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
⊢ (insert i u).card = n
have rwa : ∀ (hn : u.card + 1 = 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), i ∉ u
Tactic: rwa [Finset.card_insert_of_notMem] at hn ⊢
Cleared hypotheses: hn, h, hp, hjt, hp', hiu
-- 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i (insert j u), I ≤ f i_1
have hn' : (insert i u).card = n
Tactic: have hn' : (insert i u).card = n := by
        rwa [Finset.card_insert_of_notMem] at hn ⊢
        exacts [hiu, hju]
-- 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 rw : ∀
  (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)
Tactic: rw [Finset.coe_insert] at h ⊢
Cleared hypotheses: h, hp, hjt, hp', hiu, hn'