Theorem: Usa2002P1.Finset.subtype_union (Compfiles/Usa2002P1.lean)

State before:
α : Type u_1
p : α → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
s1 s2 : Finset α
⊢ Finset.subtype p (s1 ∪ s2) = Finset.subtype p s1 ∪ Finset.subtype p s2
Tactic:
ext a
State after:
case a
α : Type u_1
p : α → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
s1 s2 : Finset α
a : Subtype p
⊢ a ∈ Finset.subtype p (s1 ∪ s2) ↔ a ∈ Finset.subtype p s1 ∪ Finset.subtype p s2

State before:
case a
α : Type u_1
p : α → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
s1 s2 : Finset α
a : Subtype p
⊢ a ∈ Finset.subtype p (s1 ∪ s2) ↔ a ∈ Finset.subtype p s1 ∪ Finset.subtype p s2
Tactic:
simp
State after:
no goals