α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ (if r = a then a else if r = a then a else r) = r
α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ swapCore a a r = r
unfold swapCore
no goals
α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ (if r = a then a else if r = a then a else r) = r
split_ifs <;> simp [*]