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

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