[GOAL]
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
h : α ≃ β
x : f α
⊢ ↑h.symm <$> ↑h <$> x = x
[PROOFSTEP]
simp [map_map]
[GOAL]
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
h : α ≃ β
x : f β
⊢ ↑h <$> ↑h.symm <$> x = x
[PROOFSTEP]
simp [map_map]
[GOAL]
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
[PROOFSTEP]
ext x
[GOAL]
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
[PROOFSTEP]
simp only [mapEquiv_apply, refl_apply]
[GOAL]
case H
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ ↑(Equiv.refl α) <$> x = x
[PROOFSTEP]
exact LawfulFunctor.id_map x
[GOAL]
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
h : α ≃ β
h' : α' ≃ β'
x : F α α'
⊢ bimap (↑h.symm) (↑h'.symm) (bimap (↑h) (↑h') x) = x
[PROOFSTEP]
simp [bimap_bimap, id_bimap]
[GOAL]
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
h : α ≃ β
h' : α' ≃ β'
x : F β β'
⊢ bimap (↑h) (↑h') (bimap (↑h.symm) (↑h'.symm) x) = x
[PROOFSTEP]
simp [bimap_bimap, id_bimap]
[GOAL]
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
⊢ mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α')
[PROOFSTEP]
ext x
[GOAL]
case H
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
x : F α α'
⊢ ↑(mapEquiv F (Equiv.refl α) (Equiv.refl α')) x = ↑(Equiv.refl (F α α')) x
[PROOFSTEP]
simp [id_bimap]
