Theorem: Tutorial.id_app (Solution/Advanced/Category/Lecture1.lean)

State before:
C : Type u
inst✝ : Category C
a b c d e : C
X : Type
x : X
⊢ 𝟙 X x = x
Tactic:
rfl
State after:
no goals