no goals
C : Type u_2
inst✝ : Category C
r : HomRel C
a b c : C
f : a ⟶ b
a✝ b✝ : C
x : b ⟶ a✝
m₁ m₂ : a✝ ⟶ b✝
y : b✝ ⟶ c
h : r m₁ m₂
⊢ CompClosure r (f ≫ x ≫ m₁ ≫ y) (f ≫ x ≫ m₂ ≫ y)
simpa using CompClosure.intro (f ≫ x) m₁ m₂ y h