case a
α : Type u_1
β : Type ?u.88416
γ : Type ?u.88419
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s \ t)
a✝ : α
⊢ a✝ ∈ toFinset (s \ t) ↔ a✝ ∈ toFinset s \ toFinset t
α : Type u_1
β : Type ?u.88416
γ : Type ?u.88419
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s \ t)
⊢ toFinset (s \ t) = toFinset s \ toFinset t
ext
no goals
case a
α : Type u_1
β : Type ?u.88416
γ : Type ?u.88419
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s \ t)
a✝ : α
⊢ a✝ ∈ toFinset (s \ t) ↔ a✝ ∈ toFinset s \ toFinset t
simp