no goals
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category D
X : C
f g : MonoOver X
Y : C
h : Y ⟶ X
e : f ≅ g
x✝ : Factors f h
u : Y ⟶ f.obj.left
hu : u ≫ arrow f = h
⊢ (u ≫ ((forget X).map e.hom).left) ≫ arrow g = h
simp [hu]
no goals
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category D
X : C
f g : MonoOver X
Y : C
h : Y ⟶ X
e : f ≅ g
x✝ : Factors g h
u : Y ⟶ g.obj.left
hu : u ≫ arrow g = h
⊢ (u ≫ ((forget X).map e.inv).left) ≫ arrow f = h
simp [hu]