awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
iso :
  NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X)
⊢ NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X ≫
      B.functor.map (L.map (T.unitIso.hom.app X)) =
    NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X ≫
      B.functor.map (L.map (T.unitIso.hom.app X))

Tactic:
rw [← Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
iso :
  NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
⊢ NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X)

Tactic:
erw [← h.iso.hom.naturality (T.unitIso.hom.app X)]

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.CatCommSq.iso, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
iso :
  (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map
            (NatTrans.app (Iso.inv (CatCommSq.iso T.symm.functor R L B.symm.functor)) (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
⊢ NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)

Tactic:
rw [hInv_iso_hom_app]

Premises used: CategoryTheory.CatCommSq.hInv_iso_hom_app
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
iso :
  (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map (NatTrans.app (Iso.inv (CatCommSq.iso T.inverse R L B.inverse)) (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map
            (NatTrans.app (Iso.inv (CatCommSq.iso T.symm.functor R L B.symm.functor)) (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)

Tactic:
simp only [Equivalence.symm_functor]

Premises used: CategoryTheory.Equivalence.symm_functor
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
iso :
  (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.symm.inverse.obj X))) ≫
              B.inverse.map
                  (NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor))
                    (T.inverse.obj (T.symm.inverse.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.symm.inverse.obj X)))) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map (NatTrans.app (Iso.inv (CatCommSq.iso T.inverse R L B.inverse)) (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)

Tactic:
rw [hInv_iso_inv_app]

Premises used: CategoryTheory.CatCommSq.hInv_iso_inv_app
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
iso :
  (B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
        B.functor.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.functor.obj X))) ≫
              B.inverse.map
                  (NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X)))) ≫
          B.functor.map (L.map (T.unitIso.inv.app X))) ≫
      B.functor.map (L.map (T.unitIso.hom.app X)) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫
      NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.symm.inverse.obj X))) ≫
              B.inverse.map
                  (NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor))
                    (T.inverse.obj (T.symm.inverse.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.symm.inverse.obj X)))) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
iso :
  B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
      B.functor.map
        (B.inverse.map (R.map (T.functor.map (T.unit.app X))) ≫
          B.inverse.map
              (NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))) ≫
            B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X))) ≫ 𝟙 (L.obj (T.inverse.obj (T.functor.obj X)))) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫
      NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))
⊢ (B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
        B.functor.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.functor.obj X))) ≫
              B.inverse.map
                  (NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X)))) ≫
          B.functor.map (L.map (T.unitIso.inv.app X))) ≫
      B.functor.map (L.map (T.unitIso.hom.app X)) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫
      NatTrans.app (Iso.hom (CatCommSq.iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))

Tactic:
simp only [Functor.comp_obj, assoc, ← Functor.map_comp, Iso.inv_hom_id_app,
    Equivalence.counitInv_app_functor, Functor.map_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Equivalence.counitInv_app_functor, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
      B.functor.map
        (B.inverse.map (R.map (T.functor.map (T.unit.app X))) ≫
          B.inverse.map (NatTrans.app (Iso.hom (iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))) ≫
            B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X))) ≫ 𝟙 (L.obj (T.inverse.obj (T.functor.obj X)))) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫
      NatTrans.app (Iso.hom (iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))

Tactic:
simp only [Functor.map_comp, Equivalence.fun_inv_map, assoc,
    Equivalence.counitInv_functor_comp, comp_id, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Equivalence.counitInv_functor_comp, CategoryTheory.Category.comp_id, CategoryTheory.Equivalence.fun_inv_map, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app_assoc
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
iso :
  ∀ (X : C₁),
    (CatCommSq.iso T L.symm.inverse R.symm.inverse B).hom.app X =
      (CatCommSq.iso T L.symm.inverse R.symm.inverse B).hom.app X
⊢ vInv B L.symm R.symm T (vInv T L R B h) = h

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
iso :
  R.symm.inverse.map (T.map (L.symm.counitIso.inv.app X)) ≫
      R.symm.inverse.map ((CatCommSq.iso B L.symm.functor R.symm.functor T).inv.app (L.symm.inverse.obj X)) ≫
        R.symm.unitIso.inv.app (B.obj (L.symm.inverse.obj X)) =
    (CatCommSq.iso T L.symm.inverse R.symm.inverse B).hom.app X
⊢ (CatCommSq.iso T L.symm.inverse R.symm.inverse B).hom.app X =
    (CatCommSq.iso T L.symm.inverse R.symm.inverse B).hom.app X

Tactic:
rw [vInv_iso_hom_app]

Premises used: CategoryTheory.CatCommSq.vInv_iso_hom_app
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
iso :
  R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map ((CatCommSq.iso B L.inverse R.inverse T).inv.app (L.functor.obj X)) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X
⊢ R.symm.inverse.map (T.map (L.symm.counitIso.inv.app X)) ≫
      R.symm.inverse.map ((CatCommSq.iso B L.symm.functor R.symm.functor T).inv.app (L.symm.inverse.obj X)) ≫
        R.symm.unitIso.inv.app (B.obj (L.symm.inverse.obj X)) =
    (CatCommSq.iso T L.symm.inverse R.symm.inverse B).hom.app X

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
iso :
  R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map ((CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map ((CatCommSq.iso B L.inverse R.inverse T).inv.app (L.functor.obj X)) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X

Tactic:
rw [vInv_iso_inv_app]

Premises used: CategoryTheory.CatCommSq.vInv_iso_inv_app
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
iso :
  (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map ((CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X

Tactic:
rw [← cancel_mono (B.map (L.functor.map (NatTrans.app L.unitIso.hom X)))]

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Equivalence.functor, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
iso :
  ((T ⋙ R.functor).map (L.unitIso.hom.app X) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
⊢ (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))

Tactic:
rw [← Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
iso :
  (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
⊢ ((T ⋙ R.functor).map (L.unitIso.hom.app X) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
iso :
  R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
        R.counit.app (R.functor.obj (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
          (CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X)) ≫
            B.map (L.counitIso.hom.app (L.functor.obj X)) ≫ B.map (L.functor.map (L.unitIso.hom.app X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
⊢ (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))

Tactic:
simp only [Functor.map_comp, Equivalence.fun_inv_map, Functor.comp_obj,
    Functor.id_obj, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Equivalence.fun_inv_map, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv_hom_id_app_assoc
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
iso :
  R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
        R.counit.app (R.functor.obj (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
          (CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X)) ≫
            B.map (𝟙 (L.functor.obj ((L.functor ⋙ L.inverse).obj X))) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
        R.counit.app (R.functor.obj (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
          (CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X)) ≫
            B.map (L.counitIso.hom.app (L.functor.obj X)) ≫ B.map (L.functor.map (L.unitIso.hom.app X)) =
    (CatCommSq.iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))

Tactic:
rw [← B.map_comp, L.counit_app_functor, ← L.functor.map_comp, ← NatTrans.comp_app,
    Iso.inv_hom_id, NatTrans.id_app, L.functor.map_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.Equivalence.counit_app_functor