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
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:
exact e₁.hom.naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- 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.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)

Tactic:
e₂.hom.naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- 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.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)

Tactic:
exact e₂.hom.naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- 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
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
w : ∀ (x : X), (α.app x).fst = (β.app x).fst
w₁ : ∀ (x : X), (α.app x).snd = (β.app x).snd
⊢ α = β

Tactic:
ext x
-- 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
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
x : X
⊢ (α.app x).fst = (β.app x).fst

Tactic:
congrArg (fun t ↦ t.app x) e₁

Premises used: congrArg
-- 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
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
x : X
⊢ (α.app x).fst = (β.app x).fst

Tactic:
exact congrArg (fun t ↦ t.app x) e₁

Premises used: congrArg
-- 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
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
x : X
⊢ (α.app x).snd = (β.app x).snd

Tactic:
congrArg (fun t ↦ t.app x) e₂

Premises used: congrArg
-- 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
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
x : X
⊢ (α.app x).snd = (β.app x).snd

Tactic:
exact congrArg (fun t ↦ t.app x) e₂

Premises used: congrArg
-- 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 :
  autoParam
    (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)
    toCatCommSqOver_mapIso_mkNatIso_eq_mkIso._auto_1
⊢ whiskerRight e₁.hom F ≫ (obj (toCatCommSqOver F G X) K).iso.hom =
    (obj (toCatCommSqOver F G X) J).iso.hom ≫ whiskerRight e₂.hom G

Tactic:
simpa [functorEquiv, toCatCommSqOver] using coh

Premises used: CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver, CategoryTheory.Limits.CategoricalPullback.functorEquiv
-- 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
w :
  ∀ (x : X),
    Eq (α := (obj (toCatCommSqOver F G X) J).fst.obj x ⟶ (obj (toCatCommSqOver F G X) K).fst.obj x)
      (NatTrans.app (CatCommSqOver.Hom.fst (Iso.hom (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh)))) x)
      (NatTrans.app (CatCommSqOver.Hom.fst (Iso.hom (CatCommSqOver.mkIso e₁ e₂ ⋯))) x)
w₁ :
  ∀ (x : X),
    Eq (α := (obj (toCatCommSqOver F G X) J).snd.obj x ⟶ (obj (toCatCommSqOver F G X) K).snd.obj x)
      (NatTrans.app (CatCommSqOver.Hom.snd (Iso.hom (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh)))) x)
      (NatTrans.app (CatCommSqOver.Hom.snd (Iso.hom (CatCommSqOver.mkIso e₁ e₂ ⋯))) x)
⊢ Eq (α := obj (toCatCommSqOver F G X) J ≅ obj (toCatCommSqOver F G X) K)
    (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh)) (CatCommSqOver.mkIso e₁ e₂ ⋯)

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
⊢ Eq (α := (obj (toCatCommSqOver F G X) J).fst.obj x ⟶ (obj (toCatCommSqOver F G X) K).fst.obj x)
    (NatTrans.app (CatCommSqOver.Hom.fst (Iso.hom (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh)))) x)
    (NatTrans.app (CatCommSqOver.Hom.fst (Iso.hom (CatCommSqOver.mkIso e₁ e₂ ⋯))) 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
⊢ Eq (α := (obj (toCatCommSqOver F G X) J).snd.obj x ⟶ (obj (toCatCommSqOver F G X) K).snd.obj x)
    (NatTrans.app (CatCommSqOver.Hom.snd (Iso.hom (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh)))) x)
    (NatTrans.app (CatCommSqOver.Hom.snd (Iso.hom (CatCommSqOver.mkIso e₁ e₂ ⋯))) 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 :
  autoParam
    (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)
    mkNatIso_eq._auto_1
⊢ whiskerRight e₁.hom F ≫ (obj (Equivalence.functor (functorEquiv F G X)) K).iso.hom =
    (obj (Equivalence.functor (functorEquiv F G X)) J).iso.hom ≫ whiskerRight e₂.hom G

Tactic:
simpa [functorEquiv, toCatCommSqOver] using coh

Premises used: CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver, CategoryTheory.Limits.CategoricalPullback.functorEquiv
-- 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
rw :
  mkNatIso e₁ e₂ coh =
    FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
      (Equivalence.fullyFaithfulFunctor (functorEquiv F G X)) (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))
⊢ mkNatIso e₁ e₂ coh =
    FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
      (Equivalence.fullyFaithfulFunctor (functorEquiv F G X)) (CatCommSqOver.mkIso e₁ e₂ ⋯)

Tactic:
rw [← toCatCommSqOver_mapIso_mkNatIso_eq_mkIso e₁ e₂ coh]

Premises used: CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_mapIso_mkNatIso_eq_mkIso
-- 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
w :
  ∀ (x : X),
    (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₁ F G)).app x =
      (whiskerRight
            (FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
                {
                  preimage :=
                    fun {X_1 Y : X ⥤ F ⊡ G}
                      (f :
                        obj (Equivalence.functor (functorEquiv F G X)) X_1 ⟶
                          obj (Equivalence.functor (functorEquiv F G X)) Y) ↦
                    NatTrans.app (Iso.hom (Equivalence.unitIso (functorEquiv F G X))) X_1 ≫
                      map (Equivalence.inverse (functorEquiv F G X)) f ≫
                        NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv F G X))) Y,
                  map_preimage := ⋯, preimage_map := ⋯ }
                (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))).hom
            (π₁ F G)).app
        x
w₁ :
  ∀ (x : X),
    (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₂ F G)).app x =
      (whiskerRight
            (FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
                {
                  preimage :=
                    fun {X_1 Y : X ⥤ F ⊡ G}
                      (f :
                        obj (Equivalence.functor (functorEquiv F G X)) X_1 ⟶
                          obj (Equivalence.functor (functorEquiv F G X)) Y) ↦
                    NatTrans.app (Iso.hom (Equivalence.unitIso (functorEquiv F G X))) X_1 ≫
                      map (Equivalence.inverse (functorEquiv F G X)) f ≫
                        NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv F G X))) Y,
                  map_preimage := ⋯, preimage_map := ⋯ }
                (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))).hom
            (π₂ F G)).app
        x
⊢ mkNatIso e₁ e₂ coh =
    FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
      {
        preimage :=
          fun {X_1 Y : X ⥤ F ⊡ G}
            (f :
              obj (Equivalence.functor (functorEquiv F G X)) X_1 ⟶ obj (Equivalence.functor (functorEquiv F G X)) Y) ↦
          NatTrans.app (Iso.hom (Equivalence.unitIso (functorEquiv F G X))) X_1 ≫
            map (Equivalence.inverse (functorEquiv F G X)) f ≫
              NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv F G X))) Y,
        map_preimage := ⋯, preimage_map := ⋯ }
      (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))

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
⊢ (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₁ F G)).app x =
    (whiskerRight
          (FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
              {
                preimage :=
                  fun {X_1 Y : X ⥤ F ⊡ G}
                    (f :
                      obj (Equivalence.functor (functorEquiv F G X)) X_1 ⟶
                        obj (Equivalence.functor (functorEquiv F G X)) Y) ↦
                  NatTrans.app (Iso.hom (Equivalence.unitIso (functorEquiv F G X))) X_1 ≫
                    map (Equivalence.inverse (functorEquiv F G X)) f ≫
                      NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv F G X))) Y,
                map_preimage := ⋯, preimage_map := ⋯ }
              (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))).hom
          (π₁ F G)).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
⊢ (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₂ F G)).app x =
    (whiskerRight
          (FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
              {
                preimage :=
                  fun {X_1 Y : X ⥤ F ⊡ G}
                    (f :
                      obj (Equivalence.functor (functorEquiv F G X)) X_1 ⟶
                        obj (Equivalence.functor (functorEquiv F G X)) Y) ↦
                  NatTrans.app (Iso.hom (Equivalence.unitIso (functorEquiv F G X))) X_1 ≫
                    map (Equivalence.inverse (functorEquiv F G X)) f ≫
                      NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv F G X))) Y,
                map_preimage := ⋯, preimage_map := ⋯ }
              (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))).hom
          (π₂ F G)).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
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst_3 : Category.{v₄, u₄} A₁
inst_4 : Category.{v₅, u₅} B₁
inst_5 : Category.{v₆, u₆} C₁
F₁ : Functor.{v₄, v₅, u₄, u₅} A₁ B₁
G₁ : Functor.{v₆, v₅, u₆, u₅} C₁ B₁
X : Type u₇
inst_6 : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
x y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
f : x ⟶ y
w :
  ∀ (x_1 : X),
    NatTrans.app
        (whiskerRight (whiskerRight f.fst ψ.left) F₁ ≫
          { fst := y.fst ⋙ ψ.left, snd := y.snd ⋙ ψ.right,
                iso :=
                  y.fst.associator ψ.left F₁ ≪≫
                    y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                      (y.fst.associator F ψ.base).symm ≪≫
                        isoWhiskerRight y.iso ψ.base ≪≫
                          y.snd.associator G ψ.base ≪≫
                            y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                              (y.snd.associator ψ.right G₁).symm }.iso.hom)
        x_1 =
      ({ fst := x.fst ⋙ ψ.left, snd := x.snd ⋙ ψ.right,
                  iso :=
                    x.fst.associator ψ.left F₁ ≪≫
                      x.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                        (x.fst.associator F ψ.base).symm ≪≫
                          isoWhiskerRight x.iso ψ.base ≪≫
                            x.snd.associator G ψ.base ≪≫
                              x.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                (x.snd.associator ψ.right G₁).symm :
                  CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.iso.hom ≫
            whiskerRight (whiskerRight f.snd ψ.right) G₁).app
        x_1
⊢ whiskerRight (whiskerRight f.fst ψ.left) F₁ ≫
      { fst := y.fst ⋙ ψ.left, snd := y.snd ⋙ ψ.right,
            iso :=
              y.fst.associator ψ.left F₁ ≪≫
                y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (y.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight y.iso ψ.base ≪≫
                      y.snd.associator G ψ.base ≪≫
                        y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                          (y.snd.associator ψ.right G₁).symm }.iso.hom =
    { fst := x.fst ⋙ ψ.left, snd := x.snd ⋙ ψ.right,
            iso :=
              x.fst.associator ψ.left F₁ ≪≫
                x.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (x.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight x.iso ψ.base ≪≫
                      x.snd.associator G ψ.base ≪≫
                        x.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫ (x.snd.associator ψ.right G₁).symm :
            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.iso.hom ≫
      whiskerRight (whiskerRight f.snd ψ.right) G₁

Tactic:
ext x
-- 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
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst_3 : Category.{v₄, u₄} A₁
inst_4 : Category.{v₅, u₅} B₁
inst_5 : Category.{v₆, u₆} C₁
F₁ : Functor.{v₄, v₅, u₄, u₅} A₁ B₁
G₁ : Functor.{v₆, v₅, u₆, u₅} C₁ B₁
X : Type u₇
inst_6 : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
x_1 y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
f : x_1 ⟶ y
x : X
⊢ NatTrans.app
      (whiskerRight (whiskerRight f.fst ψ.left) F₁ ≫
        { fst := y.fst ⋙ ψ.left, snd := y.snd ⋙ ψ.right,
              iso :=
                y.fst.associator ψ.left F₁ ≪≫
                  y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (y.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight y.iso ψ.base ≪≫
                        y.snd.associator G ψ.base ≪≫
                          y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (y.snd.associator ψ.right G₁).symm }.iso.hom)
      x =
    ({ fst := x_1.fst ⋙ ψ.left, snd := x_1.snd ⋙ ψ.right,
                iso :=
                  x_1.fst.associator ψ.left F₁ ≪≫
                    x_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                      (x_1.fst.associator F ψ.base).symm ≪≫
                        isoWhiskerRight x_1.iso ψ.base ≪≫
                          x_1.snd.associator G ψ.base ≪≫
                            x_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                              (x_1.snd.associator ψ.right G₁).symm :
                CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.iso.hom ≫
          whiskerRight (whiskerRight f.snd ψ.right) G₁).app
      x

Tactic:
simp [← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc