no goals
α : Type u_1
β : Type ?u.267553
γ : Type ?u.267556
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
hts : t ⊆ s
ha : a ∈ t
⊢ s \ t ∪ erase t a = erase s a
simp_rw [erase_eq, sdiff_union_sdiff_cancel hts (singleton_subset_iff.2 ha)]