Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_coe (Jordan/SubMulActions.lean)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
⊢ ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx }) = x
Tactic:
rfl
State after:
no goals