[GOAL]
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
⊢ hInv (Equivalence.symm T) R L (Equivalence.symm B) (hInv T L R B h) = h
[PROOFSTEP]
ext X
[GOAL]
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ NatTrans.app iso'.hom X = NatTrans.app iso'.hom X
[PROOFSTEP]
erw [← cancel_mono (B.functor.map (L.map (T.unitIso.hom.app X))), ← h.iso'.hom.naturality (T.unitIso.hom.app X),
  hInv_iso'_hom_app, hInv_iso'_inv_app]
[GOAL]
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (NatTrans.app (Equivalence.symm B).unitIso.hom (R.obj ((Equivalence.symm T).inverse.obj X)) ≫
        (Equivalence.symm B).inverse.map
            (B.inverse.map (R.map (NatTrans.app T.counitIso.inv ((Equivalence.symm T).inverse.obj X))) ≫
              B.inverse.map
                  (NatTrans.app (iso T.functor L R B.functor).hom
                    (T.inverse.obj ((Equivalence.symm T).inverse.obj X))) ≫
                NatTrans.app B.unitIso.inv (L.obj (T.inverse.obj ((Equivalence.symm T).inverse.obj X)))) ≫
          (Equivalence.symm B).inverse.map (L.map (NatTrans.app (Equivalence.symm T).counitIso.hom X))) ≫
      B.functor.map (L.map (NatTrans.app T.unitIso.hom X)) =
    (T.functor ⋙ R).map (NatTrans.app T.unitIso.hom X) ≫ NatTrans.app iso'.hom ((T.functor ⋙ T.inverse).obj X)
[PROOFSTEP]
dsimp
[GOAL]
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (NatTrans.app B.counitIso.inv (R.obj (T.functor.obj X)) ≫
        B.functor.map
            (B.inverse.map (R.map (NatTrans.app T.counitIso.inv (T.functor.obj X))) ≫
              B.inverse.map (NatTrans.app (iso T.functor L R B.functor).hom (T.inverse.obj (T.functor.obj X))) ≫
                NatTrans.app B.unitIso.inv (L.obj (T.inverse.obj (T.functor.obj X)))) ≫
          B.functor.map (L.map (NatTrans.app T.unitIso.inv X))) ≫
      B.functor.map (L.map (NatTrans.app T.unitIso.hom X)) =
    R.map (T.functor.map (NatTrans.app T.unitIso.hom X)) ≫ NatTrans.app iso'.hom (T.inverse.obj (T.functor.obj X))
[PROOFSTEP]
simp only [Functor.comp_obj, assoc, ← Functor.map_comp, Iso.inv_hom_id_app, Equivalence.counitInv_app_functor,
  Functor.map_id]
[GOAL]
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ NatTrans.app B.counitIso.inv (R.obj (T.functor.obj X)) ≫
      B.functor.map
        (B.inverse.map (R.map (T.functor.map (NatTrans.app (Equivalence.unit T) X))) ≫
          B.inverse.map (NatTrans.app (iso T.functor L R B.functor).hom (T.inverse.obj (T.functor.obj X))) ≫
            NatTrans.app B.unitIso.inv (L.obj (T.inverse.obj (T.functor.obj X))) ≫
              𝟙 (L.obj (T.inverse.obj (T.functor.obj X)))) =
    R.map (T.functor.map (NatTrans.app T.unitIso.hom X)) ≫ NatTrans.app iso'.hom (T.inverse.obj (T.functor.obj X))
[PROOFSTEP]
simp only [Functor.map_comp, Equivalence.fun_inv_map, assoc, Equivalence.counitInv_functor_comp, comp_id,
  Iso.inv_hom_id_app_assoc]
[GOAL]
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ R.map (T.functor.map (NatTrans.app (Equivalence.unit T) X)) ≫
      NatTrans.app (iso T.functor L R B.functor).hom (T.inverse.obj (T.functor.obj X)) =
    R.map (T.functor.map (NatTrans.app T.unitIso.hom X)) ≫ NatTrans.app iso'.hom (T.inverse.obj (T.functor.obj X))
[PROOFSTEP]
rfl
