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

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

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