no goals
C : Type u
inst✝ : Category C
X Y : C
f g : X ⟶ Y
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f
simp
case h
C : Type u
inst✝ : Category C
X Y : C
f g : X ⟶ Y
⊢ (isoSourceOfSelf f).inv ≫ ι f f = lift (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f) ≫ ι f f
C : Type u
inst✝ : Category C
X Y : C
f g : X ⟶ Y
⊢ (isoSourceOfSelf f).inv = lift (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f)
apply equalizer.hom_ext
no goals
case h
C : Type u
inst✝ : Category C
X Y : C
f g : X ⟶ Y
⊢ (isoSourceOfSelf f).inv ≫ ι f f = lift (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f) ≫ ι f f
simp [equalizer.isoSourceOfSelf]