R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
P : Ideal R
hp : IsPrime P
hne : s ≠ 0
⊢ Multiset.prod s ≤ P → ∃ I, I ∈ s ∧ I ≤ P
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
P : Ideal R
hp : IsPrime P
hne : s ≠ 0
⊢ Multiset.prod s ≤ P ↔ ∃ I, I ∈ s ∧ I ≤ P
suffices s.prod ≤ P → ∃ I ∈ s, I ≤ P from
  ⟨this, fun ⟨i, his, hip⟩ => le_trans multiset_prod_le_inf <| le_trans (Multiset.inf_le his) hip⟩
case intro
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
P : Ideal R
hp : IsPrime P
hne : s ≠ 0
b : Ideal R
hb : b ∈ s
⊢ Multiset.prod s ≤ P → ∃ I, I ∈ s ∧ I ≤ P
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
P : Ideal R
hp : IsPrime P
hne : s ≠ 0
⊢ Multiset.prod s ≤ P → ∃ I, I ∈ s ∧ I ≤ P
obtain ⟨b, hb⟩ : ∃ b, b ∈ s := Multiset.exists_mem_of_ne_zero hne
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
P : Ideal R
hp : IsPrime P
hne : s ≠ 0
b : Ideal R
hb : b ∈ s
⊢ ∃ t, s = b ::ₘ t

case intro.intro
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
⊢ Multiset.prod (b ::ₘ t) ≤ P → ∃ I, I ∈ b ::ₘ t ∧ I ≤ P
case intro
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
P : Ideal R
hp : IsPrime P
hne : s ≠ 0
b : Ideal R
hb : b ∈ s
⊢ Multiset.prod s ≤ P → ∃ I, I ∈ s ∧ I ≤ P
obtain ⟨t, rfl⟩ : ∃ t, s = b ::ₘ t
case intro.intro
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
⊢ Multiset.prod (b ::ₘ t) ≤ P → ∃ I, I ∈ b ::ₘ t ∧ I ≤ P
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
P : Ideal R
hp : IsPrime P
hne : s ≠ 0
b : Ideal R
hb : b ∈ s
⊢ ∃ t, s = b ::ₘ t

case intro.intro
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
⊢ Multiset.prod (b ::ₘ t) ≤ P → ∃ I, I ∈ b ::ₘ t ∧ I ≤ P
exact ⟨s.erase b, (Multiset.cons_erase hb).symm⟩
case intro.intro.refine'_1
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
⊢ Multiset.prod (b ::ₘ 0) ≤ P → ∃ I, I ∈ b ::ₘ 0 ∧ I ≤ P

case intro.intro.refine'_2
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
⊢ ∀ ⦃a : Ideal R⦄ {s : Multiset (Ideal R)},
    (Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P) →
      Multiset.prod (b ::ₘ a ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ a ::ₘ s ∧ I ≤ P
case intro.intro
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
⊢ Multiset.prod (b ::ₘ t) ≤ P → ∃ I, I ∈ b ::ₘ t ∧ I ≤ P
refine' t.induction_on _ _
case intro.intro.refine'_2
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : Multiset.prod (b ::ₘ a ::ₘ s) ≤ P
⊢ ∃ I, I ∈ b ::ₘ a ::ₘ s ∧ I ≤ P
case intro.intro.refine'_2
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
⊢ ∀ ⦃a : Ideal R⦄ {s : Multiset (Ideal R)},
    (Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P) →
      Multiset.prod (b ::ₘ a ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ a ::ₘ s ∧ I ≤ P
intro a s ih h
case intro.intro.refine'_2
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : a ≤ P ∨ Multiset.prod (b ::ₘ s) ≤ P
⊢ ∃ I, I ∈ b ::ₘ a ::ₘ s ∧ I ≤ P
case intro.intro.refine'_2
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : Multiset.prod (b ::ₘ a ::ₘ s) ≤ P
⊢ ∃ I, I ∈ b ::ₘ a ::ₘ s ∧ I ≤ P
rw [Multiset.cons_swap, Multiset.prod_cons, hp.mul_le] at h
case intro.intro.refine'_2
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : a ≤ P ∨ Multiset.prod (b ::ₘ s) ≤ P
⊢ ∃ I, I ∈ a ::ₘ b ::ₘ s ∧ I ≤ P
case intro.intro.refine'_2
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : a ≤ P ∨ Multiset.prod (b ::ₘ s) ≤ P
⊢ ∃ I, I ∈ b ::ₘ a ::ₘ s ∧ I ≤ P
rw [Multiset.cons_swap]
case intro.intro.refine'_2.inl
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : a ≤ P
⊢ ∃ I, I ∈ a ::ₘ b ::ₘ s ∧ I ≤ P

case intro.intro.refine'_2.inr
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : Multiset.prod (b ::ₘ s) ≤ P
⊢ ∃ I, I ∈ a ::ₘ b ::ₘ s ∧ I ≤ P
case intro.intro.refine'_2
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : a ≤ P ∨ Multiset.prod (b ::ₘ s) ≤ P
⊢ ∃ I, I ∈ a ::ₘ b ::ₘ s ∧ I ≤ P
cases' h with h h
case intro.intro.refine'_2.inr.intro.intro
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I✝ J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih✝ : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : Multiset.prod (b ::ₘ s) ≤ P
I : Ideal R
hI : I ∈ b ::ₘ s
ih : I ≤ P
⊢ ∃ I, I ∈ a ::ₘ b ::ₘ s ∧ I ≤ P
case intro.intro.refine'_2.inr
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : Multiset.prod (b ::ₘ s) ≤ P
⊢ ∃ I, I ∈ a ::ₘ b ::ₘ s ∧ I ≤ P
obtain ⟨I, hI, ih⟩ : ∃ I ∈ b ::ₘ s, I ≤ P := ih h
no goals
case intro.intro.refine'_2.inr.intro.intro
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I✝ J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih✝ : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : Multiset.prod (b ::ₘ s) ≤ P
I : Ideal R
hI : I ∈ b ::ₘ s
ih : I ≤ P
⊢ ∃ I, I ∈ a ::ₘ b ::ₘ s ∧ I ≤ P
exact ⟨I, Multiset.mem_cons_of_mem hI, ih⟩
no goals
case intro.intro.refine'_1
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
⊢ Multiset.prod (b ::ₘ 0) ≤ P → ∃ I, I ∈ b ::ₘ 0 ∧ I ≤ P
simp only [exists_prop, Multiset.cons_zero, Multiset.prod_singleton, Multiset.mem_singleton,
  exists_eq_left, imp_self]
no goals
case intro.intro.refine'_2.inl
R : Type u
ι : Type ?u.344408
inst✝ : CommSemiring R
I J K L P : Ideal R
hp : IsPrime P
b : Ideal R
t : Multiset (Ideal R)
hne : b ::ₘ t ≠ 0
hb : b ∈ b ::ₘ t
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod (b ::ₘ s) ≤ P → ∃ I, I ∈ b ::ₘ s ∧ I ≤ P
h : a ≤ P
⊢ ∃ I, I ∈ a ::ₘ b ::ₘ s ∧ I ≤ P
exact ⟨a, Multiset.mem_cons_self a _, h⟩