α : Type u_1
β : Type ?u.241033
γ : Type ?u.241036
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b : α
s : Finset α
x : α
h : x ∈ t
⊢ insert x ↑s \ ↑t = ↑s \ ↑t
α : Type u_1
β : Type ?u.241033
γ : Type ?u.241036
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b : α
s : Finset α
x : α
h : x ∈ t
⊢ insert x s \ t = s \ t
rw [← coe_inj, coe_sdiff, coe_sdiff, coe_insert]
no goals
α : Type u_1
β : Type ?u.241033
γ : Type ?u.241036
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b : α
s : Finset α
x : α
h : x ∈ t
⊢ insert x ↑s \ ↑t = ↑s \ ↑t
exact Set.insert_diff_of_mem _ h