Theorem: Tutorial.Coequalizer.hom_id (Tutorial/Advanced/Category/Lecture2.lean)

State before:
J : Type u₁
inst✝¹ : Category J
C : Type u₂
inst✝ : Category C
F : Functor J C
i : Shape
⊢ ShapeHom.id i = 𝟙 i
Tactic:
cases i <;> rfl
State after:
no goals