[GOAL]
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β : Type u
h : α ≃ β
x : f α
⊢ ↑h.symm <$> ↑h <$> x = x
[PROOFSTEP]
simp [map_map]
[GOAL]
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β : Type u
h : α ≃ β
x : f β
⊢ ↑h <$> ↑h.symm <$> x = x
[PROOFSTEP]
simp [map_map]
