case H
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ ↑(mapEquiv f (Equiv.refl α)) x = ↑(Equiv.refl (f α)) x
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
ext x
case H
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ ↑(Equiv.refl α) <$> x = x
case H
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ ↑(mapEquiv f (Equiv.refl α)) x = ↑(Equiv.refl (f α)) x
simp only [mapEquiv_apply, refl_apply]
no goals
case H
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ ↑(Equiv.refl α) <$> x = x
exact LawfulFunctor.id_map x