case inl
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
hI : IsPrime I
x y : α
h : x ∈ I
⊢ x * y ∈ I

case inr
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
hI : IsPrime I
x y : α
h : y ∈ I
⊢ x * y ∈ I
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
hI : IsPrime I
x y : α
⊢ x ∈ I ∨ y ∈ I → x * y ∈ I
rintro (h | h)
no goals
case inl
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
hI : IsPrime I
x y : α
h : x ∈ I
⊢ x * y ∈ I

case inr
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
hI : IsPrime I
x y : α
h : y ∈ I
⊢ x * y ∈ I
exacts [I.mul_mem_right y h, I.mul_mem_left x h]