f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α✝ β : Type u₀
e : α✝ ≃ β
α : Type u₀
⊢ { toFun := id, invFun := id, left_inv := (_ : LeftInverse id id), right_inv := (_ : Function.RightInverse id id) } =
    Equiv.refl (f α)
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α✝ β : Type u₀
e : α✝ ≃ β
α : Type u₀
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
simp [EquivFunctor.mapEquiv]
no goals
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α✝ β : Type u₀
e : α✝ ≃ β
α : Type u₀
⊢ { toFun := id, invFun := id, left_inv := (_ : LeftInverse id id), right_inv := (_ : Function.RightInverse id id) } =
    Equiv.refl (f α)
rfl