α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ swapCore a b (swapCore a b r) = r
unfold swapCore
case inl.inl
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : b = a
⊢ b = r

case inl.inr.inl
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : ¬b = a
h₃ : b = b
⊢ a = r

case inl.inr.inr
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : ¬b = a
h₃ : ¬b = b
⊢ b = r

case inr.inl.inl
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : r = b
h₅ : a = a
⊢ b = r

case inr.inl.inr.inl
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : r = b
h₅ : ¬a = a
h✝ : a = b
⊢ a = r

case inr.inl.inr.inr
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : r = b
h₅ : ¬a = a
h✝ : ¬a = b
⊢ a = r

case inr.inr
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : ¬r = b
⊢ r = r
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
split_ifs with h₁ h₂ h₃ h₄ h₅
case inl.inl
α : Sort u_1
inst✝ : DecidableEq α
r b : α
h₂ : b = r
⊢ b = r
case inl.inl
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : b = a
⊢ b = r
subst h₁
no goals
case inl.inl
α : Sort u_1
inst✝ : DecidableEq α
r b : α
h₂ : b = r
⊢ b = r
exact h₂
case inl.inr.inl
α : Sort u_1
inst✝ : DecidableEq α
r b : α
h₃ : b = b
h₂ : ¬b = r
⊢ r = r
case inl.inr.inl
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : ¬b = a
h₃ : b = b
⊢ a = r
subst h₁
no goals
case inl.inr.inl
α : Sort u_1
inst✝ : DecidableEq α
r b : α
h₃ : b = b
h₂ : ¬b = r
⊢ r = r
rfl
no goals
case inl.inr.inr
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : ¬b = a
h₃ : ¬b = b
⊢ b = r
cases h₃ rfl
no goals
case inr.inl.inl
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : r = b
h₅ : a = a
⊢ b = r
exact h₄.symm
no goals
case inr.inl.inr.inl
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : r = b
h₅ : ¬a = a
h✝ : a = b
⊢ a = r
cases h₅ rfl
no goals
case inr.inl.inr.inr
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : r = b
h₅ : ¬a = a
h✝ : ¬a = b
⊢ a = r
cases h₅ rfl
no goals
case inr.inr
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : ¬r = b
⊢ r = r
rfl