Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case e₁
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₁ F G)).app x✝ =
    (whiskerRight
          ({
                  preimage := fun {X_1 Y} f ↦
                    (functorEquiv F G X).unitIso.hom.app X_1 ≫
                      (functorEquiv F G X).inverse.map f ≫ (functorEquiv F G X).unitIso.inv.app Y,
                  map_preimage := ⋯, preimage_map := ⋯ }.preimageIso
              ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh))).hom
          (π₁ F G)).app
      x✝

pp: case e₂
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₂ F G)).app x✝ =
    (whiskerRight
          ({
                  preimage := fun {X_1 Y} f ↦
                    (functorEquiv F G X).unitIso.hom.app X_1 ≫
                      (functorEquiv F G X).inverse.map f ≫ (functorEquiv F G X).unitIso.inv.app Y,
                  map_preimage := ⋯, preimage_map := ⋯ }.preimageIso
              ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh))).hom
          (π₂ F G)).app
      x✝

Tactic:
<;>

Goal state after:
case e₁
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₁ F G)).app x✝ =
    (whiskerRight
          ({
                  preimage := fun {X_1 Y} f ↦
                    (functorEquiv F G X).unitIso.hom.app X_1 ≫
                      (functorEquiv F G X).inverse.map f ≫ (functorEquiv F G X).unitIso.inv.app Y,
                  map_preimage := ⋯, preimage_map := ⋯ }.preimageIso
              ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh))).hom
          (π₁ F G)).app
      x✝

case e₂
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₂ F G)).app x✝ =
    (whiskerRight
          ({
                  preimage := fun {X_1 Y} f ↦
                    (functorEquiv F G X).unitIso.hom.app X_1 ≫
                      (functorEquiv F G X).inverse.map f ≫ (functorEquiv F G X).unitIso.inv.app Y,
                  map_preimage := ⋯, preimage_map := ⋯ }.preimageIso
              ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh))).hom
          (π₂ F G)).app
      x✝