Theorem: Equiv.comp_assoc (Extra/Equiv/Basic.lean)

State before:
γ : Sort u_1
δ : Sort u_2
β : Sort u_3
α : Sort u_4
g : Equiv γ δ
f : Equiv β γ
e : Equiv α β
⊢ (g.comp f).comp e = g.comp (f.comp e)
Tactic:
ext
State after:
case h.h
γ : Sort u_1
δ : Sort u_2
β : Sort u_3
α : Sort u_4
g : Equiv γ δ
f : Equiv β γ
e : Equiv α β
x✝ : α
⊢ ((g.comp f).comp e).fwd x✝ = (g.comp (f.comp e)).fwd x✝

State before:
case h.h
γ : Sort u_1
δ : Sort u_2
β : Sort u_3
α : Sort u_4
g : Equiv γ δ
f : Equiv β γ
e : Equiv α β
x✝ : α
⊢ ((g.comp f).comp e).fwd x✝ = (g.comp (f.comp e)).fwd x✝
Tactic:
rfl
State after:
no goals