case ne_top'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime I
⊢ prod I ⊤ ≠ ⊤

case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime I
⊢ ∀ {x y : R × S}, x * y ∈ prod I ⊤ → x ∈ prod I ⊤ ∨ y ∈ prod I ⊤
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime I
⊢ IsPrime (prod I ⊤)
constructor
case mem_or_mem'.mk.mk.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime I
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : ((r₁, s₁) * (r₂, s₂)).fst ∈ I
right✝ : ((r₁, s₁) * (r₂, s₂)).snd ∈ ⊤
⊢ (r₁, s₁) ∈ prod I ⊤ ∨ (r₂, s₂) ∈ prod I ⊤
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime I
⊢ ∀ {x y : R × S}, x * y ∈ prod I ⊤ → x ∈ prod I ⊤ ∨ y ∈ prod I ⊤
rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨h₁, _⟩
case mem_or_mem'.mk.mk.intro.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h✝ : IsPrime I
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : ((r₁, s₁) * (r₂, s₂)).fst ∈ I
right✝ : ((r₁, s₁) * (r₂, s₂)).snd ∈ ⊤
h : (r₁, s₁).fst ∈ I
⊢ (r₁, s₁) ∈ prod I ⊤ ∨ (r₂, s₂) ∈ prod I ⊤

case mem_or_mem'.mk.mk.intro.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h✝ : IsPrime I
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : ((r₁, s₁) * (r₂, s₂)).fst ∈ I
right✝ : ((r₁, s₁) * (r₂, s₂)).snd ∈ ⊤
h : (r₂, s₂).fst ∈ I
⊢ (r₁, s₁) ∈ prod I ⊤ ∨ (r₂, s₂) ∈ prod I ⊤
case mem_or_mem'.mk.mk.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime I
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : ((r₁, s₁) * (r₂, s₂)).fst ∈ I
right✝ : ((r₁, s₁) * (r₂, s₂)).snd ∈ ⊤
⊢ (r₁, s₁) ∈ prod I ⊤ ∨ (r₂, s₂) ∈ prod I ⊤
cases' h.mem_or_mem h₁ with h h
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : I ≠ ⊤
⊢ prod I ⊤ ≠ ⊤
case ne_top'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime I
⊢ prod I ⊤ ≠ ⊤
rcases h with ⟨h, -⟩
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : prod I ⊤ = ⊤
⊢ I = ⊤
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : I ≠ ⊤
⊢ prod I ⊤ ≠ ⊤
contrapose! h
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : I = ⊤ ∧ ⊤ = ⊤
⊢ I = ⊤
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : prod I ⊤ = ⊤
⊢ I = ⊤
rw [← prod_top_top, prod.ext_iff] at h
no goals
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : I = ⊤ ∧ ⊤ = ⊤
⊢ I = ⊤
exact h.1
no goals
case mem_or_mem'.mk.mk.intro.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h✝ : IsPrime I
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : ((r₁, s₁) * (r₂, s₂)).fst ∈ I
right✝ : ((r₁, s₁) * (r₂, s₂)).snd ∈ ⊤
h : (r₁, s₁).fst ∈ I
⊢ (r₁, s₁) ∈ prod I ⊤ ∨ (r₂, s₂) ∈ prod I ⊤
exact Or.inl ⟨h, trivial⟩
no goals
case mem_or_mem'.mk.mk.intro.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h✝ : IsPrime I
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : ((r₁, s₁) * (r₂, s₂)).fst ∈ I
right✝ : ((r₁, s₁) * (r₂, s₂)).snd ∈ ⊤
h : (r₂, s₂).fst ∈ I
⊢ (r₁, s₁) ∈ prod I ⊤ ∨ (r₂, s₂) ∈ prod I ⊤
exact Or.inr ⟨h, trivial⟩