awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
X_1 Y Z : X ⥤ F ⊡ G
f : X_1 ⟶ Y
g : Y ⟶ Z
x : X
⊢ Eq.{v₁ + 1} (α :=
    { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
              iso :=
                X_1.associator (π₁ F G) F ≪≫
                  X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }.fst.obj
        x ⟶
      { fst := Z ⋙ π₁ F G, snd := Z ⋙ π₂ F G,
              iso :=
                Z.associator (π₁ F G) F ≪≫
                  Z.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (Z.associator (π₂ F G) G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }.fst.obj
        x)
    (NatTrans.app
      (CatCommSqOver.Hom.fst { fst := whiskerRight (f ≫ g) (π₁ F G), snd := whiskerRight (f ≫ g) (π₂ F G), w := ⋯ }) x)
    (NatTrans.app
      (CatCommSqOver.Hom.fst
        (CategoryStruct.comp (Y :=
          { fst := Y ⋙ π₁ F G, snd := Y ⋙ π₂ F G,
            iso :=
              Y.associator (π₁ F G) F ≪≫
                Y.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (Y.associator (π₂ F G) G).symm })
          { fst := whiskerRight f (π₁ F G), snd := whiskerRight f (π₂ F G), w := ⋯ }
          { fst := whiskerRight g (π₁ F G), snd := whiskerRight g (π₂ F G), w := ⋯ }))
      x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
X_1 Y Z : X ⥤ F ⊡ G
f : X_1 ⟶ Y
g : Y ⟶ Z
x : X
⊢ Eq.{v₃ + 1} (α :=
    { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
              iso :=
                X_1.associator (π₁ F G) F ≪≫
                  X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }.snd.obj
        x ⟶
      { fst := Z ⋙ π₁ F G, snd := Z ⋙ π₂ F G,
              iso :=
                Z.associator (π₁ F G) F ≪≫
                  Z.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (Z.associator (π₂ F G) G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }.snd.obj
        x)
    (NatTrans.app
      (CatCommSqOver.Hom.snd { fst := whiskerRight (f ≫ g) (π₁ F G), snd := whiskerRight (f ≫ g) (π₂ F G), w := ⋯ }) x)
    (NatTrans.app
      (CatCommSqOver.Hom.snd
        (CategoryStruct.comp (Y :=
          { fst := Y ⋙ π₁ F G, snd := Y ⋙ π₂ F G,
            iso :=
              Y.associator (π₁ F G) F ≪≫
                Y.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (Y.associator (π₂ F G) G).symm })
          { fst := whiskerRight f (π₁ F G), snd := whiskerRight f (π₂ F G), w := ⋯ }
          { fst := whiskerRight g (π₁ F G), snd := whiskerRight g (π₂ F G), w := ⋯ }))
      x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
X_1 : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
x : X
⊢ ({
            app := fun (x : X) ↦
              { fst := (Hom.fst (𝟙 X_1)).app x, snd := (Hom.snd (𝟙 X_1)).app x, w := ⋯ :
                CategoricalPullback.Hom.{v₁, v₂, v₃, u₁, u₂, u₃} (A := A) (B := B) (C := C) (F := F) (G := G)
                  ((fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }) x)
                  ((fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }) x) },
            naturality := ⋯ :
            NatTrans (C := X) (D := F ⊡ G)
              { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G },
                map := fun {x y : X} (f : x ⟶ y) ↦
                  { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ :
                    { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }.Hom
                      { fst := X_1.fst.obj y, snd := X_1.snd.obj y, iso := X_1.iso.app y : F ⊡ G } },
                map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G }
              { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G },
                map := fun {x y : X} (f : x ⟶ y) ↦
                  { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ :
                    { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }.Hom
                      { fst := X_1.fst.obj y, snd := X_1.snd.obj y, iso := X_1.iso.app y : F ⊡ G } },
                map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G } }.app
        x).fst =
    CategoricalPullback.Hom.fst
      (NatTrans.app
        (𝟙
          { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x },
            map := fun {x y : X} (f : x ⟶ y) ↦ { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ }, map_id := ⋯,
            map_comp := ⋯ })
        x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
X_1 : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
x : X
⊢ ({
            app := fun (x : X) ↦
              { fst := (Hom.fst (𝟙 X_1)).app x, snd := (Hom.snd (𝟙 X_1)).app x, w := ⋯ :
                CategoricalPullback.Hom.{v₁, v₂, v₃, u₁, u₂, u₃} (A := A) (B := B) (C := C) (F := F) (G := G)
                  ((fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }) x)
                  ((fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }) x) },
            naturality := ⋯ :
            NatTrans (C := X) (D := F ⊡ G)
              { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G },
                map := fun {x y : X} (f : x ⟶ y) ↦
                  { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ :
                    { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }.Hom
                      { fst := X_1.fst.obj y, snd := X_1.snd.obj y, iso := X_1.iso.app y : F ⊡ G } },
                map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G }
              { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G },
                map := fun {x y : X} (f : x ⟶ y) ↦
                  { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ :
                    { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }.Hom
                      { fst := X_1.fst.obj y, snd := X_1.snd.obj y, iso := X_1.iso.app y : F ⊡ G } },
                map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G } }.app
        x).snd =
    CategoricalPullback.Hom.snd
      (NatTrans.app
        (𝟙
          { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x },
            map := fun {x y : X} (f : x ⟶ y) ↦ { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ }, map_id := ⋯,
            map_comp := ⋯ })
        x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
x : X ⥤ F ⊡ G
x_1 : X
⊢ F.map (Iso.hom (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)) ≫
      ((obj (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) x).obj x_1).iso.hom =
    ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).iso.hom ≫ G.map (Iso.hom (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
X_1 Y : X ⥤ F ⊡ G
f : X_1 ⟶ Y
x : X
⊢ Eq (α :=
    ((obj (𝟭 (X ⥤ F ⊡ G)) X_1).obj x).fst ⟶
      ((obj (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) Y).obj x).fst)
    (Hom.fst
      (NatTrans.app
        (map (𝟭 (X ⥤ F ⊡ G)) f ≫
          Iso.hom
            ((fun (x : X ⥤ F ⊡ G) ↦
                NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                      (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) ⋯)
                  ⋯)
              Y))
        x))
    (Hom.fst
      (NatTrans.app
        (Iso.hom
            ((fun (x : X ⥤ F ⊡ G) ↦
                NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                      (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) ⋯)
                  ⋯)
              X_1) ≫
          map (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) f)
        x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
X_1 Y : X ⥤ F ⊡ G
f : X_1 ⟶ Y
x : X
⊢ Eq (α :=
    ((obj (𝟭 (X ⥤ F ⊡ G)) X_1).obj x).snd ⟶
      ((obj (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) Y).obj x).snd)
    (Hom.snd
      (NatTrans.app
        (map (𝟭 (X ⥤ F ⊡ G)) f ≫
          Iso.hom
            ((fun (x : X ⥤ F ⊡ G) ↦
                NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                      (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) ⋯)
                  ⋯)
              Y))
        x))
    (Hom.snd
      (NatTrans.app
        (Iso.hom
            ((fun (x : X ⥤ F ⊡ G) ↦
                NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                      (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) ⋯)
                  ⋯)
              X_1) ≫
          map (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) f)
        x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
X_1 Y : X
f : X_1 ⟶ Y
⊢ (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.map f ≫
      Iso.hom
        ((fun (x_1 : X) ↦
            (Iso.refl
                ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj x_1) :
              (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj x_1 ≅
                (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj x_1))
          Y) =
    Iso.hom
        ((fun (x_1 : X) ↦
            (Iso.refl
                ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj x_1) :
              (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj x_1 ≅
                (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj x_1))
          X_1) ≫
      (obj (𝟭 (CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X)) x).fst.map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
X_1 Y : X
f : X_1 ⟶ Y
⊢ (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.map f ≫
      Iso.hom
        ((fun (x_1 : X) ↦
            (Iso.refl
                ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj x_1) :
              (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj x_1 ≅
                (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj x_1))
          Y) =
    Iso.hom
        ((fun (x_1 : X) ↦
            (Iso.refl
                ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj x_1) :
              (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj x_1 ≅
                (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj x_1))
          X_1) ≫
      (obj (𝟭 (CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X)) x).snd.map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
w :
  ∀ (x_1 : X),
    (whiskerRight
              (NatIso.ofComponents
                  (fun (x_2 : X) ↦
                    Iso.refl
                      ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj
                        x_2))
                  ⋯).hom
              F ≫
            (obj (𝟭 (CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X)) x).iso.hom).app
        x_1 =
      ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).iso.hom ≫
            whiskerRight
              (NatIso.ofComponents
                  (fun (x_2 : X) ↦
                    Iso.refl
                      ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj
                        x_2))
                  ⋯).hom
              G).app
        x_1
⊢ whiskerRight
        (NatIso.ofComponents
            (fun (x_1 : X) ↦
              Iso.refl
                ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj x_1))
            ⋯).hom
        F ≫
      (obj (𝟭 (CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X)) x).iso.hom =
    (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).iso.hom ≫
      whiskerRight
        (NatIso.ofComponents
            (fun (x_1 : X) ↦
              Iso.refl
                ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj x_1))
            ⋯).hom
        G

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
x_1 : X
⊢ (whiskerRight
            (NatIso.ofComponents
                (fun (x_2 : X) ↦
                  Iso.refl
                    ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj x_2))
                ⋯).hom
            F ≫
          (obj (𝟭 (CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X)) x).iso.hom).app
      x_1 =
    ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).iso.hom ≫
          whiskerRight
            (NatIso.ofComponents
                (fun (x_2 : X) ↦
                  Iso.refl
                    ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj x_2))
                ⋯).hom
            G).app
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
X_1 : X ⥤ F ⊡ G
x : X
⊢ NatTrans.app
      (CatCommSqOver.Hom.fst
        (map (toCatCommSqOver F G X)
            (NatTrans.app
              (Iso.hom
                (NatIso.ofComponents
                  (fun (x : X ⥤ F ⊡ G) ↦
                    NatIso.ofComponents
                      (fun (x_1 : X) ↦
                        mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                          (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) ⋯)
                      ⋯)
                  ⋯))
              X_1) ≫
          NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X) ↦
                  CatCommSqOver.mkIso
                    (NatIso.ofComponents
                      (fun (x_1 : X) ↦
                        Iso.refl
                          ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj
                            x_1))
                      ⋯)
                    (NatIso.ofComponents
                      (fun (x_1 : X) ↦
                        Iso.refl
                          ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj
                            x_1))
                      ⋯)
                    ⋯)
                ⋯))
            (obj (toCatCommSqOver F G X) X_1)))
      x =
    (CatCommSqOver.Hom.fst (𝟙 (obj (toCatCommSqOver F G X) X_1))).app x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
X_1 : X ⥤ F ⊡ G
x : X
⊢ NatTrans.app
      (CatCommSqOver.Hom.snd
        (map (toCatCommSqOver F G X)
            (NatTrans.app
              (Iso.hom
                (NatIso.ofComponents
                  (fun (x : X ⥤ F ⊡ G) ↦
                    NatIso.ofComponents
                      (fun (x_1 : X) ↦
                        mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                          (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) ⋯)
                      ⋯)
                  ⋯))
              X_1) ≫
          NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X) ↦
                  CatCommSqOver.mkIso
                    (NatIso.ofComponents
                      (fun (x_1 : X) ↦
                        Iso.refl
                          ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj
                            x_1))
                      ⋯)
                    (NatIso.ofComponents
                      (fun (x_1 : X) ↦
                        Iso.refl
                          ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj
                            x_1))
                      ⋯)
                    ⋯)
                ⋯))
            (obj (toCatCommSqOver F G X) X_1)))
      x =
    (CatCommSqOver.Hom.snd (𝟙 (obj (toCatCommSqOver F G X) X_1))).app x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : 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
⊢ F.map (e₁.app x).hom ≫ (K.obj x).iso.hom = (J.obj x).iso.hom ≫ G.map (e₂.app x).hom

Tactic:
simpa using NatTrans.congr_app coh x

Premises used: CategoryTheory.NatTrans.congr_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : 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_1 : X
f : x ⟶ x_1
hₗ :
  Hom.fst (J.map f ≫ Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x_1)) =
    Hom.fst (Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x) ≫ K.map f)
hᵣ :
  Hom.snd (J.map f ≫ Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x_1)) =
    Hom.snd (Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x) ≫ K.map f)
⊢ J.map f ≫ Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x_1) =
    Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x) ≫ K.map f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : 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_1 : X
f : x ⟶ x_1
⊢ Hom.fst (J.map f ≫ Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x_1)) =
    Hom.fst (Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x) ≫ K.map f)

Tactic:
e₁.hom.naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom