α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ swapCore a b r = swapCore b a r
unfold swapCore
case inl.inl
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : r = b
⊢ b = a
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r
split_ifs with h₁ h₂ h₃ <;> simp
case inl.inl.refl
α : Sort u_1
inst✝ : DecidableEq α
r b : α
h₂ : r = b
⊢ b = r
case inl.inl
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : r = b
⊢ b = a
cases h₁
case inl.inl.refl.refl
α : Sort u_1
inst✝ : DecidableEq α
r : α
⊢ r = r
case inl.inl.refl
α : Sort u_1
inst✝ : DecidableEq α
r b : α
h₂ : r = b
⊢ b = r
cases h₂
no goals
case inl.inl.refl.refl
α : Sort u_1
inst✝ : DecidableEq α
r : α
⊢ r = r
rfl