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

State before:
α : Sort u_1
β : Sort u_2
e : Equiv α β
x : α
⊢ e.rev (e.fwd x) = x
Tactic:
rw [←Equiv.fwd_eq_iff_rev_eq]
State after:
no goals