[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ ∀ {a b : R × S},
    a ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → a + b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}
[PROOFSTEP]
rintro ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ⟨ha₁, ha₂⟩ ⟨hb₁, hb₂⟩
[GOAL]
case mk.mk.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
a₁ : R
a₂ : S
b₁ : R
b₂ : S
ha₁ : (a₁, a₂).fst ∈ I
ha₂ : (a₁, a₂).snd ∈ J
hb₁ : (b₁, b₂).fst ∈ I
hb₂ : (b₁, b₂).snd ∈ J
⊢ (a₁, a₂) + (b₁, b₂) ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}
[PROOFSTEP]
exact ⟨I.add_mem ha₁ hb₁, J.add_mem ha₂ hb₂⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ 0 ∈
    { carrier := {x | x.fst ∈ I ∧ x.snd ∈ J},
        add_mem' :=
          (_ :
            ∀ {a b : R × S},
              a ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} →
                b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → a + b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}) }.carrier
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ ∀ (c : R × S) {x : R × S},
    x ∈
        {
              toAddSubsemigroup :=
                { carrier := {x | x.fst ∈ I ∧ x.snd ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {a b : R × S},
                        a ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} →
                          b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → a + b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}) },
              zero_mem' := (_ : 0 ∈ I ∧ 0 ∈ J) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := {x | x.fst ∈ I ∧ x.snd ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {a b : R × S},
                        a ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} →
                          b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → a + b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}) },
              zero_mem' := (_ : 0 ∈ I ∧ 0 ∈ J) }.toAddSubsemigroup.carrier
[PROOFSTEP]
rintro ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ⟨hb₁, hb₂⟩
[GOAL]
case mk.mk.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
a₁ : R
a₂ : S
b₁ : R
b₂ : S
hb₁ : (b₁, b₂).fst ∈ I
hb₂ : (b₁, b₂).snd ∈ J
⊢ (a₁, a₂) • (b₁, b₂) ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | x.fst ∈ I ∧ x.snd ∈ J},
              add_mem' :=
                (_ :
                  ∀ {a b : R × S},
                    a ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} →
                      b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → a + b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}) },
          zero_mem' := (_ : 0 ∈ I ∧ 0 ∈ J) }.toAddSubsemigroup.carrier
[PROOFSTEP]
exact ⟨I.mul_mem_left _ hb₁, J.mul_mem_left _ hb₂⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ ∀ (x : R × S), x ∈ prod ⊤ ⊤ ↔ x ∈ ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ I = prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I)
[PROOFSTEP]
apply Ideal.ext
[GOAL]
case 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)
⊢ ∀ (x : R × S), x ∈ I ↔ x ∈ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I)
[PROOFSTEP]
rintro ⟨r, s⟩
[GOAL]
case h.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
r : R
s : S
⊢ (r, s) ∈ I ↔ (r, s) ∈ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I)
[PROOFSTEP]
rw [mem_prod, mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective,
  mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
[GOAL]
case h.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
r : R
s : S
⊢ (r, s) ∈ I ↔ (∃ x, x ∈ I ∧ ↑(RingHom.fst R S) x = r) ∧ ∃ x, x ∈ I ∧ ↑(RingHom.snd R S) x = s
[PROOFSTEP]
refine' ⟨fun h => ⟨⟨_, ⟨h, rfl⟩⟩, ⟨_, ⟨h, rfl⟩⟩⟩, _⟩
[GOAL]
case h.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
r : R
s : S
⊢ ((∃ x, x ∈ I ∧ ↑(RingHom.fst R S) x = r) ∧ ∃ x, x ∈ I ∧ ↑(RingHom.snd R S) x = s) → (r, s) ∈ I
[PROOFSTEP]
rintro ⟨⟨⟨r, s'⟩, ⟨h₁, rfl⟩⟩, ⟨⟨r', s⟩, ⟨h₂, rfl⟩⟩⟩
[GOAL]
case h.mk.intro.intro.mk.intro.intro.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 × S)
r : R
s' : S
h₁ : (r, s') ∈ I
r' : R
s : S
h₂ : (r', s) ∈ I
⊢ (↑(RingHom.fst R S) (r, s'), ↑(RingHom.snd R S) (r', s)) ∈ I
[PROOFSTEP]
simpa using I.add_mem (I.mul_mem_left (1, 0) h₁) (I.mul_mem_left (0, 1) h₂)
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ map (RingHom.fst R S) (prod I J) = I
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R
⊢ x ∈ map (RingHom.fst R S) (prod I J) ↔ x ∈ I
[PROOFSTEP]
rw [mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective]
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.fst R S) x_1 = x) ↔ x ∈ I
[PROOFSTEP]
exact
  ⟨by
    rintro ⟨x, ⟨h, rfl⟩⟩
    exact h.1, fun h => ⟨⟨x, 0⟩, ⟨⟨h, Ideal.zero_mem _⟩, rfl⟩⟩⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.fst R S) x_1 = x) → x ∈ I
[PROOFSTEP]
rintro ⟨x, ⟨h, rfl⟩⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ prod I J
⊢ ↑(RingHom.fst R S) x ∈ I
[PROOFSTEP]
exact h.1
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ map (RingHom.snd R S) (prod I J) = J
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : S
⊢ x ∈ map (RingHom.snd R S) (prod I J) ↔ x ∈ J
[PROOFSTEP]
rw [mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.snd R S) x_1 = x) ↔ x ∈ J
[PROOFSTEP]
exact
  ⟨by
    rintro ⟨x, ⟨h, rfl⟩⟩
    exact h.2, fun h => ⟨⟨0, x⟩, ⟨⟨Ideal.zero_mem _, h⟩, rfl⟩⟩⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.snd R S) x_1 = x) → x ∈ J
[PROOFSTEP]
rintro ⟨x, ⟨h, rfl⟩⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ prod I J
⊢ ↑(RingHom.snd R S) x ∈ J
[PROOFSTEP]
exact h.2
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ map (↑RingEquiv.prodComm) (prod I J) = prod J I
[PROOFSTEP]
refine' Trans.trans (ideal_prod_eq _) _
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ prod (map (RingHom.fst S R) (map (↑RingEquiv.prodComm) (prod I J)))
      (map (RingHom.snd S R) (map (↑RingEquiv.prodComm) (prod I J))) =
    prod J I
[PROOFSTEP]
simp [map_map]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
x✝ : Ideal R × Ideal S
I : Ideal R
J : Ideal S
⊢ (fun I => (map (RingHom.fst R S) I, map (RingHom.snd R S) I)) ((fun I => prod I.fst I.snd) (I, J)) = (I, J)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I'✝ : Ideal R
J✝ J'✝ : Ideal S
I I' : Ideal R
J J' : Ideal S
⊢ prod I J = prod I' J' ↔ I = I' ∧ J = J'
[PROOFSTEP]
simp only [← idealProdEquiv_symm_apply, idealProdEquiv.symm.injective.eq_iff, Prod.mk.inj_iff]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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 ≠ ⊤
[PROOFSTEP]
contrapose! h
[GOAL]
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 ⊤)
[PROOFSTEP]
rw [h, prod_top_top, isPrime_iff]
[GOAL]
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 ∈ ⊤)
[PROOFSTEP]
simp [isPrime_iff, h]
[GOAL]
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
[PROOFSTEP]
intro x y hxy
[GOAL]
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
[PROOFSTEP]
have : (⟨x, 1⟩ : R × S) * ⟨y, 1⟩ ∈ prod I ⊤ :=
  by
  rw [Prod.mk_mul_mk, mul_one, mem_prod]
  exact ⟨hxy, trivial⟩
[GOAL]
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 ⊤
[PROOFSTEP]
rw [Prod.mk_mul_mk, mul_one, mem_prod]
[GOAL]
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 ∈ ⊤
[PROOFSTEP]
exact ⟨hxy, trivial⟩
[GOAL]
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
[PROOFSTEP]
simpa using h.mem_or_mem this
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime (prod ⊤ I)
⊢ IsPrime I
[PROOFSTEP]
apply @isPrime_of_isPrime_prod_top _ R
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime (prod ⊤ I)
⊢ IsPrime (prod I ⊤)
[PROOFSTEP]
rw [← map_prodComm_prod]
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime (prod ⊤ I)
⊢ IsPrime (map (↑RingEquiv.prodComm) (prod ⊤ I))
[PROOFSTEP]
exact map_isPrime_of_equiv _
[GOAL]
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 ⊤)
[PROOFSTEP]
constructor
[GOAL]
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 ⊤ ≠ ⊤
[PROOFSTEP]
rcases h with ⟨h, -⟩
[GOAL]
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 ⊤ ≠ ⊤
[PROOFSTEP]
contrapose! h
[GOAL]
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 = ⊤
[PROOFSTEP]
rw [← prod_top_top, prod.ext_iff] at h 
[GOAL]
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 = ⊤
[PROOFSTEP]
exact h.1
[GOAL]
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 ⊤
[PROOFSTEP]
rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨h₁, _⟩
[GOAL]
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 ⊤
[PROOFSTEP]
cases' h.mem_or_mem h₁ with h h
[GOAL]
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 ⊤
[PROOFSTEP]
exact Or.inl ⟨h, trivial⟩
[GOAL]
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 ⊤
[PROOFSTEP]
exact Or.inr ⟨h, trivial⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime I
⊢ IsPrime (prod ⊤ I)
[PROOFSTEP]
letI : IsPrime (prod I (⊤ : Ideal R)) := isPrime_ideal_prod_top
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime I
this : IsPrime (prod I ⊤) := isPrime_ideal_prod_top
⊢ IsPrime (prod ⊤ I)
[PROOFSTEP]
rw [← map_prodComm_prod]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime I
this : IsPrime (prod I ⊤) := isPrime_ideal_prod_top
⊢ IsPrime (map (↑RingEquiv.prodComm) (prod I ⊤))
[PROOFSTEP]
apply map_isPrime_of_equiv _
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ IsPrime (prod I J) → I = ⊤ ∨ J = ⊤
[PROOFSTEP]
contrapose!
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ I ≠ ⊤ ∧ J ≠ ⊤ → ¬IsPrime (prod I J)
[PROOFSTEP]
simp only [ne_top_iff_one, isPrime_iff, not_and, not_forall, not_or]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ ¬1 ∈ I ∧ ¬1 ∈ J → ¬1 ∈ prod I J → ∃ x x_1 h, ¬x ∈ prod I J ∧ ¬x_1 ∈ prod I J
[PROOFSTEP]
exact fun ⟨hI, hJ⟩ _ => ⟨⟨0, 1⟩, ⟨1, 0⟩, by simp, by simp [hJ], by simp [hI]⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x✝¹ : ¬1 ∈ I ∧ ¬1 ∈ J
x✝ : ¬1 ∈ prod I J
hI : ¬1 ∈ I
hJ : ¬1 ∈ J
⊢ (0, 1) * (1, 0) ∈ prod I J
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x✝¹ : ¬1 ∈ I ∧ ¬1 ∈ J
x✝ : ¬1 ∈ prod I J
hI : ¬1 ∈ I
hJ : ¬1 ∈ J
⊢ ¬(0, 1) ∈ prod I J
[PROOFSTEP]
simp [hJ]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x✝¹ : ¬1 ∈ I ∧ ¬1 ∈ J
x✝ : ¬1 ∈ prod I J
hI : ¬1 ∈ I
hJ : ¬1 ∈ J
⊢ ¬(1, 0) ∈ prod I J
[PROOFSTEP]
simp [hI]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rw [ideal_prod_eq I]
[GOAL]
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
[PROOFSTEP]
intro hI
[GOAL]
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
[PROOFSTEP]
rcases ideal_prod_prime_aux hI with (h | h)
[GOAL]
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
[PROOFSTEP]
right
[GOAL]
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
[PROOFSTEP]
rw [h] at hI ⊢
[GOAL]
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
[PROOFSTEP]
exact ⟨_, ⟨isPrime_of_isPrime_prod_top' hI, rfl⟩⟩
[GOAL]
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
[PROOFSTEP]
left
[GOAL]
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 ⊤
[PROOFSTEP]
rw [h] at hI ⊢
[GOAL]
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 ⊤
[PROOFSTEP]
exact ⟨_, ⟨isPrime_of_isPrime_prod_top hI, rfl⟩⟩
[GOAL]
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
[PROOFSTEP]
rintro (⟨p, ⟨h, rfl⟩⟩ | ⟨p, ⟨h, rfl⟩⟩)
[GOAL]
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 ⊤)
[PROOFSTEP]
exact isPrime_ideal_prod_top
[GOAL]
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)
[PROOFSTEP]
exact isPrime_ideal_prod_top'
