awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_3, u_2, u_3} B C
G H : Functor.{v_3, v_4, u_3, u_4} C D
η : G ⟶ H
h₁ :
  Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G))
      (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H)))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η)))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A F G) ≫
        Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
h₂ :
  Eq (α :=
    Quiver.Hom (V := B ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ G))
      (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ H)))
    (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η)))
    (Functor.whiskerLeft (inclRight A B)
      (Iso.hom (mapCompRight A F G) ≫
        Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} A B ⥤ Join.{v_1, v_4, u_1, u_4} A D) (mapPair (𝟭 A) (F ⋙ G))
      (mapPair (𝟭 A) (F ⋙ H)))
    (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))
    (Iso.hom (mapCompRight A F G) ≫
      Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H))

Tactic:
apply natTrans_ext

Premises used: CategoryTheory.Join.natTrans_ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_3, u_2, u_3} B C
G H : Functor.{v_3, v_4, u_3, u_4} C D
η : G ⟶ H
h₁ :
  ∀ (x : A),
    Eq (α :=
      Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D) (obj (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G)) x)
        (obj (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H)) x))
      (NatTrans.app (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclLeft A B)
          (Iso.hom (mapCompRight A F G) ≫
            Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G))
      (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H)))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η)))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A F G) ≫
        Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_3, u_2, u_3} B C
G H : Functor.{v_3, v_4, u_3, u_4} C D
η : G ⟶ H
h₂ :
  ∀ (x : B),
    Eq (α :=
      Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D) (obj (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ G)) x)
        (obj (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ H)) x))
      (NatTrans.app (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclRight A B)
          (Iso.hom (mapCompRight A F G) ≫
            Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := B ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ G))
      (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ H)))
    (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η)))
    (Functor.whiskerLeft (inclRight A B)
      (Iso.hom (mapCompRight A F G) ≫
        Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_3, u_2, u_3} B C
G H : Functor.{v_3, v_4, u_3, u_4} C D
η : G ⟶ H
x : A
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D) (obj (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G)) x)
      (obj (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H)) x))
    (NatTrans.app (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclLeft A B)
        (Iso.hom (mapCompRight A F G) ≫
          Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
      x)

Tactic:
simp [mapCompRight]

Premises used: CategoryTheory.Join.mapCompRight
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_3, u_2, u_3} B C
G H : Functor.{v_3, v_4, u_3, u_4} C D
η : G ⟶ H
x : B
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D) (obj (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ G)) x)
      (obj (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ H)) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclRight A B)
        (Iso.hom (mapCompRight A F G) ≫
          Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
      x)

Tactic:
simp [mapCompRight]

Premises used: CategoryTheory.Join.mapCompRight
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_1, v_2, u_1, u_2} A B
G H : Functor.{v_2, v_3, u_2, u_3} B C
η : G ⟶ H
h₁ :
  Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_3, v_4, u_3, u_4} C D) (inclLeft A D ⋙ mapPair (F ⋙ G) (𝟭 D))
      (inclLeft A D ⋙ mapPair (F ⋙ H) (𝟭 D)))
    (Functor.whiskerLeft (inclLeft A D) (mapWhiskerRight (F.whiskerLeft η) (𝟭 D)))
    (Functor.whiskerLeft (inclLeft A D)
      (Iso.hom (mapCompLeft D F G) ≫
        Functor.whiskerLeft (mapPair F (𝟭 D)) (mapWhiskerRight η (𝟭 D)) ≫ Iso.inv (mapCompLeft D F H)))
h₂ :
  Eq (α :=
    Quiver.Hom (V := D ⥤ Join.{v_3, v_4, u_3, u_4} C D) (inclRight A D ⋙ mapPair (F ⋙ G) (𝟭 D))
      (inclRight A D ⋙ mapPair (F ⋙ H) (𝟭 D)))
    (Functor.whiskerLeft (inclRight A D) (mapWhiskerRight (F.whiskerLeft η) (𝟭 D)))
    (Functor.whiskerLeft (inclRight A D)
      (Iso.hom (mapCompLeft D F G) ≫
        Functor.whiskerLeft (mapPair F (𝟭 D)) (mapWhiskerRight η (𝟭 D)) ≫ Iso.inv (mapCompLeft D F H)))
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D ⥤ Join.{v_3, v_4, u_3, u_4} C D) (mapPair (F ⋙ G) (𝟭 D))
      (mapPair (F ⋙ H) (𝟭 D)))
    (mapWhiskerRight (F.whiskerLeft η) (𝟭 D))
    (Iso.hom (mapCompLeft D F G) ≫
      Functor.whiskerLeft (mapPair F (𝟭 D)) (mapWhiskerRight η (𝟭 D)) ≫ Iso.inv (mapCompLeft D F H))

Tactic:
apply natTrans_ext

Premises used: CategoryTheory.Join.natTrans_ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_1, v_2, u_1, u_2} A B
G H : Functor.{v_2, v_3, u_2, u_3} B C
η : G ⟶ H
h₁ :
  ∀ (x : A),
    Eq (α :=
      Quiver.Hom (V := Join.{v_3, v_4, u_3, u_4} C D) (obj (inclLeft A D ⋙ mapPair (F ⋙ G) (𝟭 D)) x)
        (obj (inclLeft A D ⋙ mapPair (F ⋙ H) (𝟭 D)) x))
      (NatTrans.app (Functor.whiskerLeft (inclLeft A D) (mapWhiskerRight (F.whiskerLeft η) (𝟭 D))) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclLeft A D)
          (Iso.hom (mapCompLeft D F G) ≫
            Functor.whiskerLeft (mapPair F (𝟭 D)) (mapWhiskerRight η (𝟭 D)) ≫ Iso.inv (mapCompLeft D F H)))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_3, v_4, u_3, u_4} C D) (inclLeft A D ⋙ mapPair (F ⋙ G) (𝟭 D))
      (inclLeft A D ⋙ mapPair (F ⋙ H) (𝟭 D)))
    (Functor.whiskerLeft (inclLeft A D) (mapWhiskerRight (F.whiskerLeft η) (𝟭 D)))
    (Functor.whiskerLeft (inclLeft A D)
      (Iso.hom (mapCompLeft D F G) ≫
        Functor.whiskerLeft (mapPair F (𝟭 D)) (mapWhiskerRight η (𝟭 D)) ≫ Iso.inv (mapCompLeft D F H)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_1, v_2, u_1, u_2} A B
G H : Functor.{v_2, v_3, u_2, u_3} B C
η : G ⟶ H
h₂ :
  ∀ (x : D),
    Eq (α :=
      Quiver.Hom (V := Join.{v_3, v_4, u_3, u_4} C D) (obj (inclRight A D ⋙ mapPair (F ⋙ G) (𝟭 D)) x)
        (obj (inclRight A D ⋙ mapPair (F ⋙ H) (𝟭 D)) x))
      (NatTrans.app (Functor.whiskerLeft (inclRight A D) (mapWhiskerRight (F.whiskerLeft η) (𝟭 D))) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclRight A D)
          (Iso.hom (mapCompLeft D F G) ≫
            Functor.whiskerLeft (mapPair F (𝟭 D)) (mapWhiskerRight η (𝟭 D)) ≫ Iso.inv (mapCompLeft D F H)))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := D ⥤ Join.{v_3, v_4, u_3, u_4} C D) (inclRight A D ⋙ mapPair (F ⋙ G) (𝟭 D))
      (inclRight A D ⋙ mapPair (F ⋙ H) (𝟭 D)))
    (Functor.whiskerLeft (inclRight A D) (mapWhiskerRight (F.whiskerLeft η) (𝟭 D)))
    (Functor.whiskerLeft (inclRight A D)
      (Iso.hom (mapCompLeft D F G) ≫
        Functor.whiskerLeft (mapPair F (𝟭 D)) (mapWhiskerRight η (𝟭 D)) ≫ Iso.inv (mapCompLeft D F H)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_1, v_2, u_1, u_2} A B
G H : Functor.{v_2, v_3, u_2, u_3} B C
η : G ⟶ H
x : A
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_3, v_4, u_3, u_4} C D) (obj (inclLeft A D ⋙ mapPair (F ⋙ G) (𝟭 D)) x)
      (obj (inclLeft A D ⋙ mapPair (F ⋙ H) (𝟭 D)) x))
    (NatTrans.app (Functor.whiskerLeft (inclLeft A D) (mapWhiskerRight (F.whiskerLeft η) (𝟭 D))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclLeft A D)
        (Iso.hom (mapCompLeft D F G) ≫
          Functor.whiskerLeft (mapPair F (𝟭 D)) (mapWhiskerRight η (𝟭 D)) ≫ Iso.inv (mapCompLeft D F H)))
      x)

Tactic:
simp [mapCompLeft]

Premises used: CategoryTheory.Join.mapCompLeft
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_1, v_2, u_1, u_2} A B
G H : Functor.{v_2, v_3, u_2, u_3} B C
η : G ⟶ H
x : D
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_3, v_4, u_3, u_4} C D) (obj (inclRight A D ⋙ mapPair (F ⋙ G) (𝟭 D)) x)
      (obj (inclRight A D ⋙ mapPair (F ⋙ H) (𝟭 D)) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A D) (mapWhiskerRight (F.whiskerLeft η) (𝟭 D))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclRight A D)
        (Iso.hom (mapCompLeft D F G) ≫
          Functor.whiskerLeft (mapPair F (𝟭 D)) (mapWhiskerRight η (𝟭 D)) ≫ Iso.inv (mapCompLeft D F H)))
      x)

Tactic:
simp [mapCompLeft]

Premises used: CategoryTheory.Join.mapCompLeft
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F G : Functor.{v_2, v_3, u_2, u_3} B C
η : F ⟶ G
H : Functor.{v_3, v_4, u_3, u_4} C D
h₁ :
  Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H))
      (inclLeft A B ⋙ mapPair (𝟭 A) (G ⋙ H)))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H)))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A F H) ≫
        Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ Iso.inv (mapCompRight A G H)))
h₂ :
  Eq (α :=
    Quiver.Hom (V := B ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ H))
      (inclRight A B ⋙ mapPair (𝟭 A) (G ⋙ H)))
    (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H)))
    (Functor.whiskerLeft (inclRight A B)
      (Iso.hom (mapCompRight A F H) ≫
        Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ Iso.inv (mapCompRight A G H)))
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} A B ⥤ Join.{v_1, v_4, u_1, u_4} A D) (mapPair (𝟭 A) (F ⋙ H))
      (mapPair (𝟭 A) (G ⋙ H)))
    (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H))
    (Iso.hom (mapCompRight A F H) ≫
      Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ Iso.inv (mapCompRight A G H))

Tactic:
apply natTrans_ext

Premises used: CategoryTheory.Join.natTrans_ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F G : Functor.{v_2, v_3, u_2, u_3} B C
η : F ⟶ G
H : Functor.{v_3, v_4, u_3, u_4} C D
h₁ :
  ∀ (x : A),
    Eq (α :=
      Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D) (obj (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H)) x)
        (obj (inclLeft A B ⋙ mapPair (𝟭 A) (G ⋙ H)) x))
      (NatTrans.app (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H))) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclLeft A B)
          (Iso.hom (mapCompRight A F H) ≫
            Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ Iso.inv (mapCompRight A G H)))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H))
      (inclLeft A B ⋙ mapPair (𝟭 A) (G ⋙ H)))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H)))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A F H) ≫
        Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ Iso.inv (mapCompRight A G H)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F G : Functor.{v_2, v_3, u_2, u_3} B C
η : F ⟶ G
H : Functor.{v_3, v_4, u_3, u_4} C D
h₂ :
  ∀ (x : B),
    Eq (α :=
      Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D) (obj (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ H)) x)
        (obj (inclRight A B ⋙ mapPair (𝟭 A) (G ⋙ H)) x))
      (NatTrans.app (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H))) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclRight A B)
          (Iso.hom (mapCompRight A F H) ≫
            Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ Iso.inv (mapCompRight A G H)))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := B ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ H))
      (inclRight A B ⋙ mapPair (𝟭 A) (G ⋙ H)))
    (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H)))
    (Functor.whiskerLeft (inclRight A B)
      (Iso.hom (mapCompRight A F H) ≫
        Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ Iso.inv (mapCompRight A G H)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F G : Functor.{v_2, v_3, u_2, u_3} B C
η : F ⟶ G
H : Functor.{v_3, v_4, u_3, u_4} C D
x : A
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D) (obj (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H)) x)
      (obj (inclLeft A B ⋙ mapPair (𝟭 A) (G ⋙ H)) x))
    (NatTrans.app (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclLeft A B)
        (Iso.hom (mapCompRight A F H) ≫
          Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ Iso.inv (mapCompRight A G H)))
      x)

Tactic:
simp [mapCompRight]

Premises used: CategoryTheory.Join.mapCompRight
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F G : Functor.{v_2, v_3, u_2, u_3} B C
η : F ⟶ G
H : Functor.{v_3, v_4, u_3, u_4} C D
x : B
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D) (obj (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ H)) x)
      (obj (inclRight A B ⋙ mapPair (𝟭 A) (G ⋙ H)) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclRight A B)
        (Iso.hom (mapCompRight A F H) ≫
          Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ Iso.inv (mapCompRight A G H)))
      x)

Tactic:
simp [mapCompRight]

Premises used: CategoryTheory.Join.mapCompRight
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F G : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ G
H : Functor.{v_2, v_3, u_2, u_3} B C
h₁ :
  Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_3, v_4, u_3, u_4} C D) (inclLeft A D ⋙ mapPair (F ⋙ H) (𝟭 D))
      (inclLeft A D ⋙ mapPair (G ⋙ H) (𝟭 D)))
    (Functor.whiskerLeft (inclLeft A D) (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D)))
    (Functor.whiskerLeft (inclLeft A D)
      (Iso.hom (mapCompLeft D F H) ≫
        Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ Iso.inv (mapCompLeft D G H)))
h₂ :
  Eq (α :=
    Quiver.Hom (V := D ⥤ Join.{v_3, v_4, u_3, u_4} C D) (inclRight A D ⋙ mapPair (F ⋙ H) (𝟭 D))
      (inclRight A D ⋙ mapPair (G ⋙ H) (𝟭 D)))
    (Functor.whiskerLeft (inclRight A D) (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D)))
    (Functor.whiskerLeft (inclRight A D)
      (Iso.hom (mapCompLeft D F H) ≫
        Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ Iso.inv (mapCompLeft D G H)))
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D ⥤ Join.{v_3, v_4, u_3, u_4} C D) (mapPair (F ⋙ H) (𝟭 D))
      (mapPair (G ⋙ H) (𝟭 D)))
    (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))
    (Iso.hom (mapCompLeft D F H) ≫
      Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ Iso.inv (mapCompLeft D G H))

Tactic:
apply natTrans_ext

Premises used: CategoryTheory.Join.natTrans_ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F G : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ G
H : Functor.{v_2, v_3, u_2, u_3} B C
h₁ :
  ∀ (x : A),
    Eq (α :=
      Quiver.Hom (V := Join.{v_3, v_4, u_3, u_4} C D) (obj (inclLeft A D ⋙ mapPair (F ⋙ H) (𝟭 D)) x)
        (obj (inclLeft A D ⋙ mapPair (G ⋙ H) (𝟭 D)) x))
      (NatTrans.app (Functor.whiskerLeft (inclLeft A D) (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclLeft A D)
          (Iso.hom (mapCompLeft D F H) ≫
            Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ Iso.inv (mapCompLeft D G H)))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_3, v_4, u_3, u_4} C D) (inclLeft A D ⋙ mapPair (F ⋙ H) (𝟭 D))
      (inclLeft A D ⋙ mapPair (G ⋙ H) (𝟭 D)))
    (Functor.whiskerLeft (inclLeft A D) (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D)))
    (Functor.whiskerLeft (inclLeft A D)
      (Iso.hom (mapCompLeft D F H) ≫
        Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ Iso.inv (mapCompLeft D G H)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F G : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ G
H : Functor.{v_2, v_3, u_2, u_3} B C
h₂ :
  ∀ (x : D),
    Eq (α :=
      Quiver.Hom (V := Join.{v_3, v_4, u_3, u_4} C D) (obj (inclRight A D ⋙ mapPair (F ⋙ H) (𝟭 D)) x)
        (obj (inclRight A D ⋙ mapPair (G ⋙ H) (𝟭 D)) x))
      (NatTrans.app (Functor.whiskerLeft (inclRight A D) (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclRight A D)
          (Iso.hom (mapCompLeft D F H) ≫
            Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ Iso.inv (mapCompLeft D G H)))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := D ⥤ Join.{v_3, v_4, u_3, u_4} C D) (inclRight A D ⋙ mapPair (F ⋙ H) (𝟭 D))
      (inclRight A D ⋙ mapPair (G ⋙ H) (𝟭 D)))
    (Functor.whiskerLeft (inclRight A D) (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D)))
    (Functor.whiskerLeft (inclRight A D)
      (Iso.hom (mapCompLeft D F H) ≫
        Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ Iso.inv (mapCompLeft D G H)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F G : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ G
H : Functor.{v_2, v_3, u_2, u_3} B C
x : A
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_3, v_4, u_3, u_4} C D) (obj (inclLeft A D ⋙ mapPair (F ⋙ H) (𝟭 D)) x)
      (obj (inclLeft A D ⋙ mapPair (G ⋙ H) (𝟭 D)) x))
    (NatTrans.app (Functor.whiskerLeft (inclLeft A D) (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclLeft A D)
        (Iso.hom (mapCompLeft D F H) ≫
          Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ Iso.inv (mapCompLeft D G H)))
      x)

Tactic:
simp [mapCompLeft]

Premises used: CategoryTheory.Join.mapCompLeft
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F G : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ G
H : Functor.{v_2, v_3, u_2, u_3} B C
x : D
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_3, v_4, u_3, u_4} C D) (obj (inclRight A D ⋙ mapPair (F ⋙ H) (𝟭 D)) x)
      (obj (inclRight A D ⋙ mapPair (G ⋙ H) (𝟭 D)) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A D) (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclRight A D)
        (Iso.hom (mapCompLeft D F H) ≫
          Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ Iso.inv (mapCompLeft D G H)))
      x)

Tactic:
simp [mapCompLeft]

Premises used: CategoryTheory.Join.mapCompLeft