case inl
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : Abs.abs p = p
⊢ Prime p

case inr
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : Abs.abs p = -p
⊢ Prime (-p)
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
⊢ Prime (Abs.abs p)
obtain h | h := abs_choice p <;> rw [h]
no goals
case inl
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : Abs.abs p = p
⊢ Prime p
exact hp
no goals
case inr
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : Abs.abs p = -p
⊢ Prime (-p)
exact hp.neg