Theorem: PointedFunction.comp (LeanCourse/Lectures/Lecture8Before.lean)

State before:
n : ℕ
X : PointedType
Y : PointedType
Z : PointedType
g : Y →. Z
f : X →. Y
⊢ (↑g ∘ ↑f) X.pt = Z.pt
Tactic:
sorry
State after:
no goals