case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ IsPrime I → (∃ p, IsPrime p ∧ I = prod p ⊤) ∨ ∃ p, IsPrime p ∧ I = prod ⊤ p

case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ ((∃ p, IsPrime p ∧ I = prod p ⊤) ∨ ∃ p, IsPrime p ∧ I = prod ⊤ p) → IsPrime I
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ IsPrime I ↔ (∃ p, IsPrime p ∧ I = prod p ⊤) ∨ ∃ p, IsPrime p ∧ I = prod ⊤ p
constructor
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I)) →
    (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
      ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ IsPrime I → (∃ p, IsPrime p ∧ I = prod p ⊤) ∨ ∃ p, IsPrime p ∧ I = prod ⊤ p
rw [ideal_prod_eq I]
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
⊢ (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
    ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I)) →
    (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
      ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
intro hI
case mp.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.fst R S) I = ⊤
⊢ (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
    ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p

case mp.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.snd R S) I = ⊤
⊢ (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
    ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
⊢ (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
    ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
rcases ideal_prod_prime_aux hI with (h | h)
case mp.inl.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.fst R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
case mp.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.fst R S) I = ⊤
⊢ (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
    ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
right
case mp.inl.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod ⊤ (map (RingHom.snd R S) I))
h : map (RingHom.fst R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod ⊤ (map (RingHom.snd R S) I) = prod ⊤ p
case mp.inl.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.fst R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
rw [h] at hI⊢
no goals
case mp.inl.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod ⊤ (map (RingHom.snd R S) I))
h : map (RingHom.fst R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod ⊤ (map (RingHom.snd R S) I) = prod ⊤ p
exact ⟨_, ⟨isPrime_of_isPrime_prod_top' hI, rfl⟩⟩
case mp.inr.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.snd R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤
case mp.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.snd R S) I = ⊤
⊢ (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
    ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
left
case mp.inr.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) ⊤)
h : map (RingHom.snd R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) ⊤ = prod p ⊤
case mp.inr.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.snd R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤
rw [h] at hI⊢
no goals
case mp.inr.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) ⊤)
h : map (RingHom.snd R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) ⊤ = prod p ⊤
exact ⟨_, ⟨isPrime_of_isPrime_prod_top hI, rfl⟩⟩
case mpr.inl.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
p : Ideal R
h : IsPrime p
⊢ IsPrime (prod p ⊤)

case mpr.inr.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' p : Ideal S
h : IsPrime p
⊢ IsPrime (prod ⊤ p)
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ ((∃ p, IsPrime p ∧ I = prod p ⊤) ∨ ∃ p, IsPrime p ∧ I = prod ⊤ p) → IsPrime I
rintro (⟨p, ⟨h, rfl⟩⟩ | ⟨p, ⟨h, rfl⟩⟩)
no goals
case mpr.inl.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
p : Ideal R
h : IsPrime p
⊢ IsPrime (prod p ⊤)
exact isPrime_ideal_prod_top
no goals
case mpr.inr.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' p : Ideal S
h : IsPrime p
⊢ IsPrime (prod ⊤ p)
exact isPrime_ideal_prod_top'