case refl
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category D
A : C
X Y : Subobject A
⊢ eqToHom (_ : underlying.obj X = underlying.obj X) ≫ arrow X = arrow X
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category D
A : C
X Y : Subobject A
h : X = Y
⊢ eqToHom (_ : underlying.obj X = underlying.obj Y) ≫ arrow Y = arrow X
induction h
no goals
case refl
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category D
A : C
X Y : Subobject A
⊢ eqToHom (_ : underlying.obj X = underlying.obj X) ≫ arrow X = arrow X
simp