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

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

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