case h
α : Type ?u.204587
β : Type ?u.204590
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.204602
H : Type ?u.204605
F : Type ?u.204608
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
x✝ : M
⊢ ↑(comp g (f₁ * f₂)) x✝ = ↑(comp g f₁ * comp g f₂) x✝
α : Type ?u.204587
β : Type ?u.204590
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.204602
H : Type ?u.204605
F : Type ?u.204608
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
⊢ comp g (f₁ * f₂) = comp g f₁ * comp g f₂
ext
no goals
case h
α : Type ?u.204587
β : Type ?u.204590
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.204602
H : Type ?u.204605
F : Type ?u.204608
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
x✝ : M
⊢ ↑(comp g (f₁ * f₂)) x✝ = ↑(comp g f₁ * comp g f₂) x✝
simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]