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

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

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