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