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

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

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