Theorem: Nat.Combination.mem_iff (Jordan/MulActionCombination.lean)

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
⊢ s ∈ Combination α n ↔ s.card = n
Tactic:
unfold Combination
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
⊢ s ∈ {s | s.card = n} ↔ s.card = n

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
⊢ s ∈ {s | s.card = n} ↔ s.card = n
Tactic:
simp only [Set.mem_setOf_eq]
State after:
no goals