Theorem: Section3sheet1.comp_eval (FormalisingMathematics2024/Section03functions/Sheet1.lean)

State before:
X Y Z : Type
f : X → Y
g : Y → Z
x : X
⊢ (g ∘ f) x = g (f x)
Tactic:
rfl
State after:
no goals