case a
α : Type u_1
β : Type ?u.86702
γ : Type ?u.86705
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.86702
γ : Type ?u.86705
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.86702
γ : Type ?u.86705
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