ext
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ (s ∪ t).erase a = s.erase a ∪ t.erase a
case a
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
s t : Finset α
a✝ : α
⊢ a✝ ∈ (s ∪ t).erase a ↔ a✝ ∈ s.erase a ∪ t.erase a