case intro a1_left a1_right =>
  simp only [if_neg a1_right]
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
a b : β
f : α → β
v : α
a1_left : v ∈ S
a1_right : ¬v = x
⊢ (if v = x then a else f v) = if v = x then b else f v
no goals