case pos
R : Type u_2
A : Type ?u.1190669
K : Type ?u.1190672
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
P : Ideal R
hP : IsPrime P
hP0 : P = ⊥
⊢ ∏ i in s, f i ≤ P ↔ ∃ i, i ∈ s ∧ f i ≤ P

case neg
R : Type u_2
A : Type ?u.1190669
K : Type ?u.1190672
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
P : Ideal R
hP : IsPrime P
hP0 : ¬P = ⊥
⊢ ∏ i in s, f i ≤ P ↔ ∃ i, i ∈ s ∧ f i ≤ P
R : Type u_2
A : Type ?u.1190669
K : Type ?u.1190672
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
P : Ideal R
hP : IsPrime P
⊢ ∏ i in s, f i ≤ P ↔ ∃ i, i ∈ s ∧ f i ≤ P
by_cases hP0 : P = ⊥
case neg
R : Type u_2
A : Type ?u.1190669
K : Type ?u.1190672
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
P : Ideal R
hP : IsPrime P
hP0 : ¬P = ⊥
⊢ P ∣ ∏ i in s, f i ↔ ∃ i, i ∈ s ∧ P ∣ f i
case neg
R : Type u_2
A : Type ?u.1190669
K : Type ?u.1190672
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
P : Ideal R
hP : IsPrime P
hP0 : ¬P = ⊥
⊢ ∏ i in s, f i ≤ P ↔ ∃ i, i ∈ s ∧ f i ≤ P
simp only [← Ideal.dvd_iff_le]
no goals
case neg
R : Type u_2
A : Type ?u.1190669
K : Type ?u.1190672
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
P : Ideal R
hP : IsPrime P
hP0 : ¬P = ⊥
⊢ P ∣ ∏ i in s, f i ↔ ∃ i, i ∈ s ∧ P ∣ f i
exact ((Ideal.prime_iff_isPrime hP0).mpr hP).dvd_finset_prod_iff _
case pos
R : Type u_2
A : Type ?u.1190669
K : Type ?u.1190672
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
P : Ideal R
hP : IsPrime P
hP0 : P = ⊥
⊢ ∏ i in s, f i = ⊥ ↔ ∃ i, i ∈ s ∧ f i = ⊥
case pos
R : Type u_2
A : Type ?u.1190669
K : Type ?u.1190672
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
P : Ideal R
hP : IsPrime P
hP0 : P = ⊥
⊢ ∏ i in s, f i ≤ P ↔ ∃ i, i ∈ s ∧ f i ≤ P
simp only [hP0, le_bot_iff]
no goals
case pos
R : Type u_2
A : Type ?u.1190669
K : Type ?u.1190672
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
P : Ideal R
hP : IsPrime P
hP0 : P = ⊥
⊢ ∏ i in s, f i = ⊥ ↔ ∃ i, i ∈ s ∧ f i = ⊥
rw [← Ideal.zero_eq_bot, Finset.prod_eq_zero_iff]