no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
hab : a ≠ b
s : Set α
⊢ insert a (s \ {b}) = insert a s \ {b}
simp_rw [← union_singleton, union_diff_distrib,
  diff_singleton_eq_self (mem_singleton_iff.not.2 hab.symm)]