Theorem: HTPI.comp_def (HTPILib/Chap5.lean)

State before:
A B C : Type
g : B → C
f : A → B
x : A
⊢ (g ∘ f) x = g (f x)
Tactic:
rfl
State after:
no goals