case h
α : Type ?u.214013
β : Type ?u.214016
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.214028
H : Type ?u.214031
F : Type ?u.214034
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
x✝ : M
⊢ ↑(comp f 1) x✝ = ↑1 x✝
α : Type ?u.214013
β : Type ?u.214016
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.214028
H : Type ?u.214031
F : Type ?u.214034
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
⊢ comp f 1 = 1
ext
no goals
case h
α : Type ?u.214013
β : Type ?u.214016
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.214028
H : Type ?u.214031
F : Type ?u.214034
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
x✝ : M
⊢ ↑(comp f 1) x✝ = ↑1 x✝
simp only [map_one, coe_comp, Function.comp_apply, one_apply]