case refl
C : Type u₁
inst✝ : Category C
X Y : C
p : X ⟶ Y
⊢ Eq.mpr (_ : (X ⟶ Y) = (X ⟶ Y)) p = p ≫ eqToHom (_ : Y = Y)
C : Type u₁
inst✝ : Category C
X Y Z : C
p : X ⟶ Y
q : Z = Y
⊢ Eq.mpr (_ : (X ⟶ Z) = (X ⟶ Y)) p = p ≫ eqToHom (_ : Y = Z)
cases q
no goals
case refl
C : Type u₁
inst✝ : Category C
X Y : C
p : X ⟶ Y
⊢ Eq.mpr (_ : (X ⟶ Y) = (X ⟶ Y)) p = p ≫ eqToHom (_ : Y = Y)
simp