Theorem: Function.comp_assoc (MLIR/Dialects/ToyModel.lean)

State before:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → β
g : β → γ
h : γ → δ
⊢ (h ∘ g) ∘ f = h ∘ g ∘ f
Tactic:
funext x
State after:
case h
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → β
g : β → γ
h : γ → δ
x : α
⊢ comp (h ∘ g) f x = comp h (g ∘ f) x

State before:
case h
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → β
g : β → γ
h : γ → δ
x : α
⊢ comp (h ∘ g) f x = comp h (g ∘ f) x
Tactic:
simp
State after:
no goals