Theorem: Finset.erase_union (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ (s ∪ t).erase a = s.erase a ∪ t.erase a
Tactic:
ext
State after:
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

State before:
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
Tactic:
simp[and_or_left]
State after:
no goals