split_ifs
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
⊢ (if x = a then b else f x) = if a = x then b else f x
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
h✝¹ : x = a
h✝ : a = x
⊢ b = b

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
h✝¹ : x = a
h✝ : ¬a = x
⊢ b = f x

case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
h✝¹ : ¬x = a
h✝ : a = x
⊢ f x = b

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
h✝¹ : ¬x = a
h✝ : ¬a = x
⊢ f x = f x