case h.e'_2
C : Type u
inst✝ : Category C
X Y Z : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = f ≫ 𝟙 X
C : Type u
inst✝ : Category C
X Y Z : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = 𝟙 X
convert w (𝟙 X)
no goals
case h.e'_2
C : Type u
inst✝ : Category C
X Y Z : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = f ≫ 𝟙 X
aesop