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

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

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