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 (prod I ⊤)
⊢ 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 (prod I ⊤)
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ 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 (prod I ⊤)
⊢ IsPrime I
constructor
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 : I = ⊤
⊢ ¬IsPrime (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 (prod I ⊤)
⊢ I ≠ ⊤
contrapose! h
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 : I = ⊤
⊢ ¬(⊤ ≠ ⊤ ∧ ∀ {x y : R × S}, x * y ∈ ⊤ → x ∈ ⊤ ∨ y ∈ ⊤)
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 : I = ⊤
⊢ ¬IsPrime (prod I ⊤)
rw [h, prod_top_top, isPrime_iff]
no goals
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 : I = ⊤
⊢ ¬(⊤ ≠ ⊤ ∧ ∀ {x y : R × S}, x * y ∈ ⊤ → x ∈ ⊤ ∨ y ∈ ⊤)
simp [isPrime_iff, h]
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 (prod I ⊤)
x y : R
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ 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 (prod I ⊤)
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
intro x y hxy
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 (prod I ⊤)
x y : R
hxy : x * y ∈ I
this : (x, 1) * (y, 1) ∈ prod I ⊤
⊢ x ∈ I ∨ y ∈ 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 (prod I ⊤)
x y : R
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I
have : (⟨x, 1⟩ : R × S) * ⟨y, 1⟩ ∈ prod I ⊤ := by
  rw [Prod.mk_mul_mk, mul_one, mem_prod]
  exact ⟨hxy, trivial⟩
no goals
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 (prod I ⊤)
x y : R
hxy : x * y ∈ I
this : (x, 1) * (y, 1) ∈ prod I ⊤
⊢ x ∈ I ∨ y ∈ I
simpa using h.mem_or_mem this
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 (prod I ⊤)
x y : R
hxy : x * y ∈ I
⊢ x * y ∈ I ∧ 1 ∈ ⊤
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 (prod I ⊤)
x y : R
hxy : x * y ∈ I
⊢ (x, 1) * (y, 1) ∈ prod I ⊤
rw [Prod.mk_mul_mk, mul_one, mem_prod]
no goals
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 (prod I ⊤)
x y : R
hxy : x * y ∈ I
⊢ x * y ∈ I ∧ 1 ∈ ⊤
exact ⟨hxy, trivial⟩