-- Mathlib/RingTheory/Ideal/Prod.lean
theorem isPrime_ideal_prod_top {I : Ideal R} [h : I.IsPrime] : (prod I (⊤ : Ideal S)).IsPrime

Proof state:
case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.IsPrime
⊢ I.prod ⊤ ≠ ⊤

Tactic:
rcases h with ⟨h, -⟩

Result:
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I ≠ ⊤
⊢ I.prod ⊤ ≠ ⊤

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.IsPrime
⊢ (I.prod ⊤).IsPrime

Tactic:
constructor

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

case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.IsPrime
⊢ ∀ {x y : R × S}, x * y ∈ I.prod ⊤ → x ∈ I.prod ⊤ ∨ y ∈ I.prod ⊤

Proof state:
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.IsPrime
⊢ ∀ {x y : R × S}, x * y ∈ I.prod ⊤ → x ∈ I.prod ⊤ ∨ y ∈ I.prod ⊤

Tactic:
rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨h₁, _⟩

Result:
case mem_or_mem'.mk.mk.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.IsPrime
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.fst R S) I)
right✝ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.snd R S) ⊤)
⊢ (r₁, s₁) ∈ I.prod ⊤ ∨ (r₂, s₂) ∈ I.prod ⊤

Proof state:
case mem_or_mem'.mk.mk.intro.inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h✝ : I.IsPrime
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.fst R S) I)
right✝ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.snd R S) ⊤)
h : (r₁, s₁).1 ∈ I
⊢ (r₁, s₁) ∈ I.prod ⊤ ∨ (r₂, s₂) ∈ I.prod ⊤

Tactic:
exact Or.inl ⟨h, trivial⟩

Result:
no goals

Proof state:
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤ ∧ ⊤ = ⊤
⊢ I = ⊤

Tactic:
exact h.1

Result:
no goals

Proof state:
case mem_or_mem'.mk.mk.intro.inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h✝ : I.IsPrime
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.fst R S) I)
right✝ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.snd R S) ⊤)
h : (r₂, s₂).1 ∈ I
⊢ (r₁, s₁) ∈ I.prod ⊤ ∨ (r₂, s₂) ∈ I.prod ⊤

Tactic:
exact Or.inr ⟨h, trivial⟩

Result:
no goals

Proof state:
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I ≠ ⊤
⊢ I.prod ⊤ ≠ ⊤

Tactic:
contrapose! h

Result:
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.prod ⊤ = ⊤
⊢ I = ⊤

Proof state:
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.prod ⊤ = ⊤
⊢ I = ⊤

Tactic:
rw [← prod_top_top, prod.ext_iff] at h

Result:
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤ ∧ ⊤ = ⊤
⊢ I = ⊤

Proof state:
case mem_or_mem'.mk.mk.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.IsPrime
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.fst R S) I)
right✝ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.snd R S) ⊤)
⊢ (r₁, s₁) ∈ I.prod ⊤ ∨ (r₂, s₂) ∈ I.prod ⊤

Tactic:
rcases h.mem_or_mem h₁ with h | h

Result:
case mem_or_mem'.mk.mk.intro.inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h✝ : I.IsPrime
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.fst R S) I)
right✝ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.snd R S) ⊤)
h : (r₁, s₁).1 ∈ I
⊢ (r₁, s₁) ∈ I.prod ⊤ ∨ (r₂, s₂) ∈ I.prod ⊤

case mem_or_mem'.mk.mk.intro.inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h✝ : I.IsPrime
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.fst R S) I)
right✝ : (r₁, s₁) * (r₂, s₂) ∈ ↑(comap (RingHom.snd R S) ⊤)
h : (r₂, s₂).1 ∈ I
⊢ (r₁, s₁) ∈ I.prod ⊤ ∨ (r₂, s₂) ∈ I.prod ⊤