C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
⊢ mk' (inverse F) ((unitIso ≪≫ hcomp e (Iso.refl (inverse F))) ≪≫ hcomp e' (Iso.refl (inverse F)))
      (hcomp (Iso.refl (inverse F)) e'.symm ≪≫ hcomp (Iso.refl (inverse F)) e.symm ≪≫ counitIso) =
    mk' (inverse F) (unitIso ≪≫ hcomp (e ≪≫ e') (Iso.refl (inverse F)))
      (hcomp (Iso.refl (inverse F)) (e'.symm ≪≫ e.symm) ≪≫ counitIso)
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
⊢ ofIso e' (ofIso e hF) = ofIso (e ≪≫ e') hF
dsimp [ofIso]
case e_unitIso.w.w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
X : C
⊢ (unitIso.hom.app X ≫ 𝟙 ((inverse F).obj (F.obj X)) ≫ (inverse F).map (e.hom.app X)) ≫
      𝟙 ((inverse F).obj (G.obj X)) ≫ (inverse F).map (e'.hom.app X) =
    unitIso.hom.app X ≫ 𝟙 ((inverse F).obj (F.obj X)) ≫ (inverse F).map (e.hom.app X ≫ e'.hom.app X)

case e_counitIso.w.w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
X : D
⊢ (e'.inv.app ((inverse F).obj X) ≫ G.map (𝟙 ((inverse F).obj X))) ≫
      (e.inv.app ((inverse F).obj X) ≫ F.map (𝟙 ((inverse F).obj X))) ≫ counitIso.hom.app X =
    ((e'.inv.app ((inverse F).obj X) ≫ e.inv.app ((inverse F).obj X)) ≫ F.map (𝟙 ((inverse F).obj X))) ≫
      counitIso.hom.app X
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
⊢ mk' (inverse F) ((unitIso ≪≫ hcomp e (Iso.refl (inverse F))) ≪≫ hcomp e' (Iso.refl (inverse F)))
      (hcomp (Iso.refl (inverse F)) e'.symm ≪≫ hcomp (Iso.refl (inverse F)) e.symm ≪≫ counitIso) =
    mk' (inverse F) (unitIso ≪≫ hcomp (e ≪≫ e') (Iso.refl (inverse F)))
      (hcomp (Iso.refl (inverse F)) (e'.symm ≪≫ e.symm) ≪≫ counitIso)
congr 1 <;> ext X <;> dsimp [NatIso.hcomp]
no goals
case e_unitIso.w.w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
X : C
⊢ (unitIso.hom.app X ≫ 𝟙 ((inverse F).obj (F.obj X)) ≫ (inverse F).map (e.hom.app X)) ≫
      𝟙 ((inverse F).obj (G.obj X)) ≫ (inverse F).map (e'.hom.app X) =
    unitIso.hom.app X ≫ 𝟙 ((inverse F).obj (F.obj X)) ≫ (inverse F).map (e.hom.app X ≫ e'.hom.app X)
simp only [id_comp, assoc, Functor.map_comp]
no goals
case e_counitIso.w.w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
X : D
⊢ (e'.inv.app ((inverse F).obj X) ≫ G.map (𝟙 ((inverse F).obj X))) ≫
      (e.inv.app ((inverse F).obj X) ≫ F.map (𝟙 ((inverse F).obj X))) ≫ counitIso.hom.app X =
    ((e'.inv.app ((inverse F).obj X) ≫ e.inv.app ((inverse F).obj X)) ≫ F.map (𝟙 ((inverse F).obj X))) ≫
      counitIso.hom.app X
simp only [Functor.map_id, comp_id, id_comp, assoc]