R : Type u_1
S : Type ?u.8602
M : Type u_2
a✝ b✝ : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : 1 • a = 1 • b
⊢ a = b
R : Type u_1
S : Type ?u.8602
M : Type u_2
a✝ b✝ : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : (fun x => 1 • x) a = (fun x => 1 • x) b
⊢ a = b
dsimp only [Function.comp] at ab
R : Type u_1
S : Type ?u.8602
M : Type u_2
a✝ b✝ : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : a = b
⊢ a = b
R : Type u_1
S : Type ?u.8602
M : Type u_2
a✝ b✝ : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : 1 • a = 1 • b
⊢ a = b
rw [one_smul, one_smul] at ab
no goals
R : Type u_1
S : Type ?u.8602
M : Type u_2
a✝ b✝ : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : a = b
⊢ a = b
assumption