R : Type u_2
S : Type ?u.31171
M : Type ?u.31174
a b : R
s : S
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x => g • x) x = (fun x => g • x) y
⊢ x = y
R : Type u_2
S : Type ?u.31171
M : Type ?u.31174
a b : R
s : S
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
⊢ IsSMulRegular R g
intro x y h