Theorem: exercise5_4 (LeanCourse/Assignments/Assignment5.lean)

State before:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module R (M →ₗ[R] M)
h : ∀ (r : R) (f : M →ₗ[R] M) (x : M), ↑(r • f) x = r • ↑f x
r s : R
⊢ r * s = s * r
Tactic:
sorry
State after:
no goals