case smul.h.h
α : Type ?u.96211
R✝ : Type ?u.96214
k : Type ?u.96217
S : Type ?u.96220
M✝ : Type ?u.96223
M₂ : Type ?u.96226
M₃ : Type ?u.96229
ι : Type ?u.96232
R : Type u_1
inst✝¹ : Semiring R
M : Type u_2
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
x✝¹ : R
x✝ : M
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
α : Type ?u.96211
R✝ : Type ?u.96214
k : Type ?u.96217
S : Type ?u.96220
M✝ : Type ?u.96223
M₂ : Type ?u.96226
M₃ : Type ?u.96229
ι : Type ?u.96232
R : Type u_1
inst✝¹ : Semiring R
M : Type u_2
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
⊢ P = Q
ext
no goals
case smul.h.h
α : Type ?u.96211
R✝ : Type ?u.96214
k : Type ?u.96217
S : Type ?u.96220
M✝ : Type ?u.96223
M₂ : Type ?u.96226
M₃ : Type ?u.96229
ι : Type ?u.96232
R : Type u_1
inst✝¹ : Semiring R
M : Type u_2
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
x✝¹ : R
x✝ : M
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
exact w _ _