[GOAL]
M : Type u_1
α : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M α
s : Set α
x y : M
hx : x ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
hy : y ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
z : ↑s
⊢ (x * y) • ↑z = ↑z
[PROOFSTEP]
rw [mul_smul, hy z, hx z]
[GOAL]
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
src✝ : Submonoid M := fixingSubmonoid M s
x✝ : M
hx : x✝ ∈ { toSubsemigroup := src✝.toSubsemigroup, one_mem' := (_ : 1 ∈ src✝.carrier) }.toSubsemigroup.carrier
z : ↑s
⊢ x✝⁻¹ • ↑z = ↑z
[PROOFSTEP]
rw [inv_smul_eq_iff, hx z]
