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