[GOAL]
k : Type u
inst✝² : Field k
A : Type w
inst✝¹ : Ring A
inst✝ : Algebra k A
⊢ ∀ (X Y Z : ModuleCat A) (r : k) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case h
k : Type u
inst : Field k
A : Type w
inst_1 : Ring A
inst_2 : Algebra k A
X Y Z : ModuleCat A
r : k
f : X ⟶ Y
g : Y ⟶ Z
x✝ : ↑X
⊢ ↑g (↑(r • f) x✝) = ↑(r • f ≫ g) x✝
[PROOFSTEP]
rw [LinearMap.smul_apply, LinearMap.smul_apply, LinearMap.map_smul_of_tower]
[GOAL]
case h
k : Type u
inst : Field k
A : Type w
inst_1 : Ring A
inst_2 : Algebra k A
X Y Z : ModuleCat A
r : k
f : X ⟶ Y
g : Y ⟶ Z
x✝ : ↑X
⊢ r • ↑g (↑f x✝) = r • ↑(f ≫ g) x✝
[PROOFSTEP]
rfl
