R : Type u
inst✝ : CommSemiring R
I : Ideal R
hi : IsPrimary I
x y : R
x✝ : x * y ∈ radical I
m : ℕ
hxy : x ^ m * y ^ m ∈ I
⊢ x ∈ radical I ∨ y ∈ radical I
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hi : IsPrimary I
x y : R
x✝ : x * y ∈ radical I
m : ℕ
hxy : (x * y) ^ m ∈ I
⊢ x ∈ radical I ∨ y ∈ radical I
rw [mul_pow] at hxy
case inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hi : IsPrimary I
x y : R
x✝ : x * y ∈ radical I
m : ℕ
hxy : x ^ m * y ^ m ∈ I
h : x ^ m ∈ I
⊢ x ∈ radical I ∨ y ∈ radical I

case inr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hi : IsPrimary I
x y : R
x✝ : x * y ∈ radical I
m : ℕ
hxy : x ^ m * y ^ m ∈ I
h : y ^ m ∈ radical I
⊢ x ∈ radical I ∨ y ∈ radical I
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hi : IsPrimary I
x y : R
x✝ : x * y ∈ radical I
m : ℕ
hxy : x ^ m * y ^ m ∈ I
⊢ x ∈ radical I ∨ y ∈ radical I
cases' hi.2 hxy with h h
no goals
case inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hi : IsPrimary I
x y : R
x✝ : x * y ∈ radical I
m : ℕ
hxy : x ^ m * y ^ m ∈ I
h : x ^ m ∈ I
⊢ x ∈ radical I ∨ y ∈ radical I
exact Or.inl ⟨m, h⟩
no goals
case inr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hi : IsPrimary I
x y : R
x✝ : x * y ∈ radical I
m : ℕ
hxy : x ^ m * y ^ m ∈ I
h : y ^ m ∈ radical I
⊢ x ∈ radical I ∨ y ∈ radical I
exact Or.inr (mem_radical_of_pow_mem h)