case a
α : Type u_1
β : Type ?u.12137
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ ↑eraseNone (s ∩ t) ↔ a✝ ∈ ↑eraseNone s ∩ ↑eraseNone t
α : Type u_1
β : Type ?u.12137
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ ↑eraseNone (s ∩ t) = ↑eraseNone s ∩ ↑eraseNone t
ext
no goals
case a
α : Type u_1
β : Type ?u.12137
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ ↑eraseNone (s ∩ t) ↔ a✝ ∈ ↑eraseNone s ∩ ↑eraseNone t
simp