case h
α : Type ?u.197112
β : Type ?u.197115
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.197127
H : Type ?u.197130
F : Type ?u.197133
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
x✝ : M
⊢ ↑(comp f 1) x✝ = ↑1 x✝
α : Type ?u.197112
β : Type ?u.197115
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.197127
H : Type ?u.197130
F : Type ?u.197133
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
⊢ comp f 1 = 1
ext
no goals
case h
α : Type ?u.197112
β : Type ?u.197115
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.197127
H : Type ?u.197130
F : Type ?u.197133
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
x✝ : M
⊢ ↑(comp f 1) x✝ = ↑1 x✝
simp only [OneHom.map_one, OneHom.coe_comp, Function.comp_apply, OneHom.one_apply]