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

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

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