awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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.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₂₃
have rw : (F.mapComp' f₀₂ f₂₃ f sorry).hom =
  (F.mapComp' f₀₂ f₂₃ f sorry).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.map f₁₂) (F.map f₂₃)).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃
Tactic: rw [← cancel_epi (F.mapComp' f₀₁ f₁₃ f hf).hom, Iso.hom_inv_id_assoc,
    F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ _ h₀₂ h₁₃ hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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₀₂ h₀₂).hom ▷ F.map f₂₃ =
    (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
have rw : (F.mapComp' f₀₂ f₂₃ f sorry).hom ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ =
  (F.mapComp' f₀₂ f₂₃ f sorry).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.map f₁₂) (F.map f₂₃)).inv
Tactic: rw [F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ f h₀₂ h₁₃ (by cat_disch)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (α_ (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
have rw : (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f sorry).inv =
  (α_ (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₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f sorry).inv
Tactic: rw [whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv _ _ _ _ _ _ f h₀₂ h₁₃,
    Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (α_ (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₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv
⊢ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (α_ (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
have rw₁ : (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f sorry).inv =
  (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f sorry).inv
Tactic: rw [whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv _ _ _ _ _ _ f h₀₂ h₁₃,
    Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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.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
have rw : 𝟙 (F.map f₀₁ ≫ F.map f₁₃) =
  (F.mapComp' f₀₁ f₁₃ f sorry).inv ≫
    (F.mapComp' f₀₂ f₂₃ f sorry).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: rw [← cancel_epi (F.mapComp' f₀₁ f₁₃ f).inv, Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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₀₂ 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
have rw : 𝟙 (F.map f) =
  (F.mapComp' f₀₂ f₂₃ f sorry).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 sorry).inv
Tactic: rw [← cancel_epi (F.mapComp' f₀₂ f₂₃ f).hom, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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
⊢ l ≫ b = t ≫ r
have rw : l ≫ b = l ≫ b
Tactic: rw [sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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 = φ
⊢ t ≫ r = φ
have rw : φ = φ
Tactic: rw [hφ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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 = φ
⊢ l ≫ b = φ
have rw : l ≫ b = t ≫ r
Tactic: rw [← hφ, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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
⊢ l ≫ b = φ
have rw₁ : l ≫ b = l ≫ b
Tactic: rw [← hφ, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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 = φ
⊢ F.isoMapOfCommSq sq = (F.mapComp' t r φ ⋯).symm ≪≫ F.mapComp' l b φ ⋯
have subst : F.isoMapOfCommSq sq = (F.mapComp' t r (t ≫ r) sorry).symm ≪≫ F.mapComp' l b (t ≫ r) sorry
Tactic: subst hφ
Cleared hypotheses: φ, hφ
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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.isoMapOfCommSq ⋯ = F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm
have w : (F.isoMapOfCommSq sorry).hom =
  (F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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.isoMapOfCommSq ⋯).hom =
    (F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm).hom
have 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
Tactic: rw [isoMapOfCommSq_eq _ _ f (by simp), mapComp'_comp_id, mapComp'_id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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.isoMapOfCommSq ⋯ = F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm
have w : (F.isoMapOfCommSq sorry).hom =
  (F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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.isoMapOfCommSq ⋯).hom =
    (F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm).hom
have 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
Tactic: rw [isoMapOfCommSq_eq _ _ f (by simp), mapComp'_comp_id, mapComp'_id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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
⊢ 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 ⋯
have subst : F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) sorry ≫ F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) sorry =
  (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
    F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) sorry ▷ F.map f₂₃ ≫ F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) sorry
Tactic: subst hf h₀₂ h₁₃
Cleared hypotheses: f₀₂, f₁₃, f, h₀₂, h₁₃, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (hypothesis)
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.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₂₃) ⋯
have 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₂₃)
Tactic: have := F.map₂_associator f₀₁ f₁₂ f₂₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (hypothesis)
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.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₂₃) ⋯
have this₁ : F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.map₂ (eqToHom sorry) =
  (α_ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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
⊢ 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 ⋯
have rw : F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f sorry =
  (α_ (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 sorry
Tactic: rw [whiskerLeft_mapComp'_comp_mapComp' _ _ _ _ _ _ f h₀₂ h₁₃,
    Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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 ⋯
⊢ 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 ⋯
have rw₁ : F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f sorry =
  F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f sorry
Tactic: rw [whiskerLeft_mapComp'_comp_mapComp' _ _ _ _ _ _ f h₀₂ h₁₃,
    Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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.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
have subst : F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) sorry ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) sorry =
  F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) sorry ≫
    F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) sorry ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
Tactic: subst h₀₂ h₁₃ hf
Cleared hypotheses: f₀₂, f₁₃, f, h₀₂, h₁₃, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (hypothesis)
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.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
have 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
Tactic: have := F.map₂_associator f₀₁ f₁₂ f₂₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (hypothesis)
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.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
have this₁ : F.map₂ (eqToHom sorry) ≫ 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
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.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
have rw : F.mapComp' f₀₂ f₂₃ f sorry ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ =
  F.mapComp' f₀₂ f₂₃ f sorry ≫
    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: rw [F.mapComp'_comp_whiskerLeft_mapComp'_assoc _ _ _ _ _ f h₀₂ h₁₃ (by cat_disch)]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
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
⊢ hInv T.symm R L B.symm (hInv T L R B h) = h
have iso : ∀ (X : C₁),
  Eq (α := (T.symm.inverse ⋙ R).obj X ⟶ (L ⋙ B.symm.inverse).obj X)
    (NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X)
    (NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
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₁
⊢ Eq (α := (T.symm.inverse ⋙ R).obj X ⟶ (L ⋙ B.symm.inverse).obj X)
    (NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X)
    (NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X)
have iso : NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X ≫ B.functor.map (L.map (T.unitIso.hom.app X)) =
  NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X ≫ B.functor.map (L.map (T.unitIso.hom.app X))
Tactic: rw [← cancel_mono (B.functor.map (L.map (T.unitIso.hom.app X)))]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
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₁
⊢ NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X ≫ B.functor.map (L.map (T.unitIso.hom.app X)) =
    NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X ≫ B.functor.map (L.map (T.unitIso.hom.app X))
have iso : NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X) =
  NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X)
Tactic: rw [← Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
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₁
⊢ NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X)
have iso : NatTrans.app (Iso.hom (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 (iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
Tactic: erw [← h.iso.hom.naturality (T.unitIso.hom.app X)]