no goals
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
P : MorphismProperty D
h : StableUnderComposition P
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.inverseImage P F f
hg : MorphismProperty.inverseImage P F g
⊢ MorphismProperty.inverseImage P F (f ≫ g)
simpa only [← F.map_comp] using h (F.map f) (F.map g) hf hg