case a
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
s t : Finset α
n : ℕ
m : Sym α n
⊢ m ∈ Finset.sym (s ∩ t) n ↔ m ∈ Finset.sym s n ∩ Finset.sym t n
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a b : α
n✝ : ℕ
m : Sym α n✝
s t : Finset α
n : ℕ
⊢ Finset.sym (s ∩ t) n = Finset.sym s n ∩ Finset.sym t n
ext m
no goals
case a
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
s t : Finset α
n : ℕ
m : Sym α n
⊢ m ∈ Finset.sym (s ∩ t) n ↔ m ∈ Finset.sym s n ∩ Finset.sym t n
simp only [mem_inter, mem_sym_iff, imp_and, forall_and]