case h
α : Type ?u.215866
β : Type ?u.215869
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.215881
H : Type ?u.215884
F : Type ?u.215887
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
x✝ : M
⊢ ↑(comp g (f₁ * f₂)) x✝ = ↑(comp g f₁ * comp g f₂) x✝
α : Type ?u.215866
β : Type ?u.215869
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.215881
H : Type ?u.215884
F : Type ?u.215887
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid 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.215866
β : Type ?u.215869
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.215881
H : Type ?u.215884
F : Type ?u.215887
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid 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]