awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ 𝟙 (F.map f₀₁ ≫ F.map f₁₃) =
    (F.mapComp' f₀₁ f₁₃ f ⋯).inv ≫
      (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
        (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
          (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv

Tactic:
simp [mapComp'₀₁₃_inv _ _ _ _ _ _ f h₀₂ h₁₃ hf]

Premises used: CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    (F.mapComp' f₀₁ f₁₃ f ⋯).hom ≫
      F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃

Tactic:
simp [← mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_assoc _ _ _ _ _ _ f h₀₂ h₁₃ hf]

Premises used: CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
rw :
  𝟙 (F.map f) =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
          F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
        F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv

Tactic:
rw [← cancel_epi (F.mapComp' f₀₂ f₂₃ f).hom, Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Pseudofunctor.mapComp', CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ 𝟙 (F.map f) =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
          F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv

Tactic:
simp [mapComp'₀₂₃_hom _ _ _ _ _ _ f h₀₂ h₁₃ hf]

Premises used: CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).hom =
    (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv

Tactic:
simp [mapComp'₀₂₃_inv _ _ _ _ _ _ _ h₀₂ h₁₃ hf]

Premises used: CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
t : X₁ ⟶ Y₁
l : X₁ ⟶ X₂
r : Y₁ ⟶ Y₂
b : X₂ ⟶ Y₂
sq : CommSq.{v₁, u₁} (C := B) (W := X₁) (X := Y₁) (Y := X₂) (Z := Y₂) t l r b
rw rw₁ : l ≫ b = l ≫ b
⊢ l ≫ b = t ≫ r

Tactic:
rw [sq.w]

Premises used: CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
t : X₁ ⟶ Y₁
l : X₁ ⟶ X₂
r : Y₁ ⟶ Y₂
b : X₂ ⟶ Y₂
sq : CommSq.{v₁, u₁} (C := B) (W := X₁) (X := Y₁) (Y := X₂) (Z := Y₂) t l r b
φ : X₁ ⟶ Y₂
hφ : t ≫ r = φ
rw rw₁ : φ = φ
⊢ t ≫ r = φ

Tactic:
rw [hφ]
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
t : X₁ ⟶ Y₁
l : X₁ ⟶ X₂
r : Y₁ ⟶ Y₂
b : X₂ ⟶ Y₂
sq : CommSq.{v₁, u₁} (C := B) (W := X₁) (X := Y₁) (Y := X₂) (Z := Y₂) t l r b
φ : X₁ ⟶ Y₂
hφ : t ≫ r = φ
rw : l ≫ b = t ≫ r
rw₁ rw₂ : l ≫ b = l ≫ b
⊢ l ≫ b = φ

Tactic:
rw [← hφ, sq.w]

Premises used: CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ Y₁ Y₂ : B
t : X₁ ⟶ Y₁
l : X₁ ⟶ X₂
r : Y₁ ⟶ Y₂
b : X₂ ⟶ Y₂
sq : CommSq.{v₁, u₁} (C := B) (W := X₁) (X := Y₁) (Y := X₂) (Z := Y₂) t l r b
φ : X₁ ⟶ Y₂
hφ : t ≫ r = φ
subst : F.isoMapOfCommSq sq = (F.mapComp' t r (t ≫ r) ⋯).symm ≪≫ F.mapComp' l b (t ≫ r) ⋯
⊢ F.isoMapOfCommSq sq = (F.mapComp' t r φ ⋯).symm ≪≫ F.mapComp' l b φ ⋯

Tactic:
subst hφ
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ Y₁ Y₂ : B
t : X₁ ⟶ Y₁
l : X₁ ⟶ X₂
r : Y₁ ⟶ Y₂
b : X₂ ⟶ Y₂
sq : CommSq.{v₁, u₁} (C := B) (W := X₁) (X := Y₁) (Y := X₂) (Z := Y₂) t l r b
⊢ F.isoMapOfCommSq sq = (F.mapComp' t r (t ≫ r) ⋯).symm ≪≫ F.mapComp' l b (t ≫ r) ⋯

Tactic:
simp [isoMapOfCommSq, mapComp'_eq_mapComp]

Premises used: CategoryTheory.Pseudofunctor.mapComp'_eq_mapComp, CategoryTheory.Pseudofunctor.isoMapOfCommSq
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
f : X₁ ⟶ X₂
⊢ 𝟙 X₁ ≫ f = f ≫ 𝟙 X₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ : B
f : X₁ ⟶ X₂
w :
  (F.isoMapOfCommSq ⋯).hom =
    (F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm).hom
⊢ F.isoMapOfCommSq ⋯ = F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ 𝟙 X₁ ≫ f = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ : B
f : X₁ ⟶ X₂
w :
  (((λ_ (F.map f)).symm ≪≫ (F.mapId X₁).symm ▷ᵢ F.map f).symm ≪≫
        (ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId X₂).symm).hom =
    (F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm).hom
⊢ (F.isoMapOfCommSq ⋯).hom =
    (F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm).hom

Tactic:
rw [isoMapOfCommSq_eq _ _ f (by simp), mapComp'_comp_id, mapComp'_id_comp]

Premises used: CategoryTheory.Pseudofunctor.mapComp'_comp_id, CategoryTheory.Pseudofunctor.mapComp'_id_comp, CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ (((λ_ (F.map f)).symm ≪≫ (F.mapId X₁).symm ▷ᵢ F.map f).symm ≪≫
        (ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId X₂).symm).hom =
    (F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
f : X₁ ⟶ X₂
⊢ f ≫ 𝟙 X₂ = 𝟙 X₁ ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ : B
f : X₁ ⟶ X₂
w :
  (F.isoMapOfCommSq ⋯).hom =
    (F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm).hom
⊢ F.isoMapOfCommSq ⋯ = F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ f ≫ 𝟙 X₂ = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ : B
f : X₁ ⟶ X₂
w :
  (((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId X₂).symm).symm ≪≫
        (λ_ (F.map f)).symm ≪≫ (F.mapId X₁).symm ▷ᵢ F.map f).hom =
    (F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm).hom
⊢ (F.isoMapOfCommSq ⋯).hom =
    (F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm).hom

Tactic:
rw [isoMapOfCommSq_eq _ _ f (by simp), mapComp'_comp_id, mapComp'_id_comp]

Premises used: CategoryTheory.Pseudofunctor.mapComp'_comp_id, CategoryTheory.Pseudofunctor.mapComp'_id_comp, CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ (((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId X₂).symm).symm ≪≫
        (λ_ (F.map f)).symm ≪≫ (F.mapId X₁).symm ▷ᵢ F.map f).hom =
    (F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
subst :
  F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯ ≫ F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
      F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯ ▷ F.map f₂₃ ≫ F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯
⊢ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ ≫ F.mapComp' f₀₁ f₁₃ f hf =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f ⋯

Tactic:
subst hf h₀₂ h₁₃
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
⊢ F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.map₂ (α_ f₀₁ f₁₂ f₂₃).hom =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ F.mapComp f₁₂ f₂₃ ≫ F.mapComp f₀₁ (f₁₂ ≫ f₂₃)

Tactic:
have := F.map₂_associator f₀₁ f₁₂ f₂₃
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
this :
  F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.map₂ (α_ f₀₁ f₁₂ f₂₃).hom =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ F.mapComp f₁₂ f₂₃ ≫ F.mapComp f₀₁ (f₁₂ ≫ f₂₃)
⊢ F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.map₂ (eqToHom ⋯) =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ F.mapComp f₁₂ f₂₃ ≫ F.mapComp f₀₁ (f₁₂ ≫ f₂₃)

Tactic:
simp only [Strict.associator_eqToIso, eqToIso.hom] at this

Premises used: CategoryTheory.eqToIso.hom, CategoryTheory.Bicategory.Strict.associator_eqToIso
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
this :
  F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.map₂ (eqToHom ⋯) =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ F.mapComp f₁₂ f₂₃ ≫ F.mapComp f₀₁ (f₁₂ ≫ f₂₃)
⊢ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯ ≫ F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
      F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯ ▷ F.map f₂₃ ≫ F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯

Tactic:
simp [LaxFunctor.mapComp', this]

Premises used: CategoryTheory.LaxFunctor.mapComp'
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
rw :
  F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f ⋯ =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f ⋯
rw₁ rw₂ :
  F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f ⋯ =
    F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f ⋯
⊢ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f ⋯ =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ ≫ F.mapComp' f₀₁ f₁₃ f ⋯

Tactic:
rw [whiskerLeft_mapComp'_comp_mapComp' _ _ _ _ _ _ f h₀₂ h₁₃,
    Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp', CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
subst :
  F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯ =
    F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ ≫
      F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯ ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
⊢ F.mapComp' f₀₁ f₁₃ f ⋯ ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ =
    F.mapComp' f₀₂ f₂₃ f ⋯ ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom

Tactic:
subst h₀₂ h₁₃ hf
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
⊢ F.map₂ (α_ f₀₁ f₁₂ f₂₃).hom ≫ F.mapComp f₀₁ (f₁₂ ≫ f₂₃) ≫ F.map f₀₁ ◁ F.mapComp f₁₂ f₂₃ =
    F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom

Tactic:
have := F.map₂_associator f₀₁ f₁₂ f₂₃
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
this :
  F.map₂ (α_ f₀₁ f₁₂ f₂₃).hom ≫ F.mapComp f₀₁ (f₁₂ ≫ f₂₃) ≫ F.map f₀₁ ◁ F.mapComp f₁₂ f₂₃ =
    F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
⊢ F.map₂ (eqToHom ⋯) ≫ F.mapComp f₀₁ (f₁₂ ≫ f₂₃) ≫ F.map f₀₁ ◁ F.mapComp f₁₂ f₂₃ =
    F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom

Tactic:
simp only [Strict.associator_eqToIso, eqToIso.hom] at this

Premises used: CategoryTheory.eqToIso.hom, CategoryTheory.Bicategory.Strict.associator_eqToIso
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
this :
  F.map₂ (eqToHom ⋯) ≫ F.mapComp f₀₁ (f₁₂ ≫ f₂₃) ≫ F.map f₀₁ ◁ F.mapComp f₁₂ f₂₃ =
    F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
⊢ F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯ =
    F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ ≫
      F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯ ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom

Tactic:
simp [OplaxFunctor.mapComp', ← this, PrelaxFunctor.map₂_eqToHom]

Premises used: CategoryTheory.PrelaxFunctor.map₂_eqToHom, CategoryTheory.OplaxFunctor.mapComp'
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
rw :
  F.mapComp' f₀₂ f₂₃ f ⋯ ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ =
    F.mapComp' f₀₂ f₂₃ f ⋯ ≫
      F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
⊢ F.mapComp' f₀₂ f₂₃ f ⋯ ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ =
    F.mapComp' f₀₁ f₁₃ f ⋯ ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv

Tactic:
rw [F.mapComp'_comp_whiskerLeft_mapComp'_assoc _ _ _ _ _ f h₀₂ h₁₃ (by cat_disch)]

Premises used: CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ F.mapComp' f₀₂ f₂₃ f ⋯ ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ =
    F.mapComp' f₀₂ f₂₃ f ⋯ ≫
      F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv

Tactic:
simp
-- 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 : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{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 R B
x y : C₁
f : x ⟶ y
⊢ R.map (T.map f) ≫ (iso T L R B).hom.app y = (iso T L R B).hom.app x ≫ B.map (L.map f)

Tactic:
(iso T L R B).hom.naturality f

Premises used: CategoryTheory.CatCommSq.iso, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- 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 : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{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 R B
x y : C₁
f : x ⟶ y
⊢ B.map (L.map f) ≫ (iso T L R B).inv.app y = (iso T L R B).inv.app x ≫ R.map (T.map f)

Tactic:
(iso T L R B).inv.naturality f

Premises used: CategoryTheory.CatCommSq.iso, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv
-- 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
iso :
  ∀ (X : C₁),
    Eq (α := (T.symm.inverse ⋙ R).obj X ⟶ (L ⋙ B.symm.inverse).obj X)
      (NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X)
      (NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X)
⊢ hInv T.symm R L B.symm (hInv 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 : 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 ≫
      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))
⊢ Eq (α := (T.symm.inverse ⋙ R).obj X ⟶ (L ⋙ B.symm.inverse).obj X)
    (NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X)
    (NatTrans.app (Iso.hom (CatCommSq.iso T.symm.inverse L R B.symm.inverse)) X)

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

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Equivalence.functor, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app