C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : HEq (F.map f) (G.map f)
hg : HEq (F.map g) (G.map g)
⊢ HEq (F.map f ≫ F.map g) (G.map f ≫ G.map g)
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : HEq (F.map f) (G.map f)
hg : HEq (F.map g) (G.map g)
⊢ HEq (F.map (f ≫ g)) (G.map (f ≫ g))
rw [F.map_comp, G.map_comp]
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : HEq (F.map f) (G.map f)
hg : HEq (F.map g) (G.map g)
⊢ HEq (F.map f ≫ F.map g) (G.map f ≫ G.map g)
congr