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

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