Theorem: Nat.combination_mulAction_apply (Jordan/MulActionCombination.lean)

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n✝ n : ℕ
g : G
s : Finset α
hs : s ∈ Combination α n
⊢ g • s = g • ↑{ val := s, property := hs }
Tactic:
rfl
State after:
no goals