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
E : Type u_5
inst_4 : Category.{v_5, u_5} E
F : Functor.{v_2, v_3, u_2, u_3} B C
G : Functor.{v_3, v_4, u_3, u_4} C D
H : Functor.{v_4, v_5, u_4, u_5} D E
h₁ :
  Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_1, v_5, u_1, u_5} A E) (inclLeft A B ⋙ mapPair (𝟭 A) ((F ⋙ G) ⋙ H))
      (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G ⋙ H)))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.associator G H).hom))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A (F ⋙ G) H) ≫
        Functor.whiskerRight (Iso.hom (mapCompRight A F G)) (mapPair (𝟭 A) H) ≫
          Iso.hom (Functor.associator (mapPair (𝟭 A) F) (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)) ≫
            Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.inv (mapCompRight A G H)) ≫ Iso.inv (mapCompRight A F (G ⋙ H))))
h₂ :
  Eq (α :=
    Quiver.Hom (V := B ⥤ Join.{v_1, v_5, u_1, u_5} A E) (inclRight A B ⋙ mapPair (𝟭 A) ((F ⋙ G) ⋙ H))
      (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ G ⋙ H)))
    (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (F.associator G H).hom))
    (Functor.whiskerLeft (inclRight A B)
      (Iso.hom (mapCompRight A (F ⋙ G) H) ≫
        Functor.whiskerRight (Iso.hom (mapCompRight A F G)) (mapPair (𝟭 A) H) ≫
          Iso.hom (Functor.associator (mapPair (𝟭 A) F) (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)) ≫
            Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.inv (mapCompRight A G H)) ≫ Iso.inv (mapCompRight A F (G ⋙ H))))
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} A B ⥤ Join.{v_1, v_5, u_1, u_5} A E) (mapPair (𝟭 A) ((F ⋙ G) ⋙ H))
      (mapPair (𝟭 A) (F ⋙ G ⋙ H)))
    (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)
    (Iso.hom (mapCompRight A (F ⋙ G) H) ≫
      Functor.whiskerRight (Iso.hom (mapCompRight A F G)) (mapPair (𝟭 A) H) ≫
        Iso.hom (Functor.associator (mapPair (𝟭 A) F) (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)) ≫
          Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.inv (mapCompRight A G H)) ≫ Iso.inv (mapCompRight A F (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
E : Type u_5
inst_4 : Category.{v_5, u_5} E
F : Functor.{v_2, v_3, u_2, u_3} B C
G : Functor.{v_3, v_4, u_3, u_4} C D
H : Functor.{v_4, v_5, u_4, u_5} D E
h₁ :
  ∀ (x : A),
    Eq (α :=
      Quiver.Hom (V := Join.{v_1, v_5, u_1, u_5} A E) (obj (inclLeft A B ⋙ mapPair (𝟭 A) ((F ⋙ G) ⋙ H)) x)
        (obj (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G ⋙ H)) x))
      (NatTrans.app (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclLeft A B)
          (Iso.hom (mapCompRight A (F ⋙ G) H) ≫
            Functor.whiskerRight (Iso.hom (mapCompRight A F G)) (mapPair (𝟭 A) H) ≫
              Iso.hom (Functor.associator (mapPair (𝟭 A) F) (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)) ≫
                Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.inv (mapCompRight A G H)) ≫
                  Iso.inv (mapCompRight A F (G ⋙ H))))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_1, v_5, u_1, u_5} A E) (inclLeft A B ⋙ mapPair (𝟭 A) ((F ⋙ G) ⋙ H))
      (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G ⋙ H)))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.associator G H).hom))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A (F ⋙ G) H) ≫
        Functor.whiskerRight (Iso.hom (mapCompRight A F G)) (mapPair (𝟭 A) H) ≫
          Iso.hom (Functor.associator (mapPair (𝟭 A) F) (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)) ≫
            Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.inv (mapCompRight A G H)) ≫ Iso.inv (mapCompRight A F (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
E : Type u_5
inst_4 : Category.{v_5, u_5} E
F : Functor.{v_2, v_3, u_2, u_3} B C
G : Functor.{v_3, v_4, u_3, u_4} C D
H : Functor.{v_4, v_5, u_4, u_5} D E
h₂ :
  ∀ (x : B),
    Eq (α :=
      Quiver.Hom (V := Join.{v_1, v_5, u_1, u_5} A E) (obj (inclRight A B ⋙ mapPair (𝟭 A) ((F ⋙ G) ⋙ H)) x)
        (obj (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ G ⋙ H)) x))
      (NatTrans.app (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclRight A B)
          (Iso.hom (mapCompRight A (F ⋙ G) H) ≫
            Functor.whiskerRight (Iso.hom (mapCompRight A F G)) (mapPair (𝟭 A) H) ≫
              Iso.hom (Functor.associator (mapPair (𝟭 A) F) (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)) ≫
                Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.inv (mapCompRight A G H)) ≫
                  Iso.inv (mapCompRight A F (G ⋙ H))))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := B ⥤ Join.{v_1, v_5, u_1, u_5} A E) (inclRight A B ⋙ mapPair (𝟭 A) ((F ⋙ G) ⋙ H))
      (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ G ⋙ H)))
    (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (F.associator G H).hom))
    (Functor.whiskerLeft (inclRight A B)
      (Iso.hom (mapCompRight A (F ⋙ G) H) ≫
        Functor.whiskerRight (Iso.hom (mapCompRight A F G)) (mapPair (𝟭 A) H) ≫
          Iso.hom (Functor.associator (mapPair (𝟭 A) F) (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)) ≫
            Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.inv (mapCompRight A G H)) ≫ Iso.inv (mapCompRight A F (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
E : Type u_5
inst_4 : Category.{v_5, u_5} E
F : Functor.{v_2, v_3, u_2, u_3} B C
G : Functor.{v_3, v_4, u_3, u_4} C D
H : Functor.{v_4, v_5, u_4, u_5} D E
x : A
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_5, u_1, u_5} A E) (obj (inclLeft A B ⋙ mapPair (𝟭 A) ((F ⋙ G) ⋙ H)) x)
      (obj (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G ⋙ H)) x))
    (NatTrans.app (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclLeft A B)
        (Iso.hom (mapCompRight A (F ⋙ G) H) ≫
          Functor.whiskerRight (Iso.hom (mapCompRight A F G)) (mapPair (𝟭 A) H) ≫
            Iso.hom (Functor.associator (mapPair (𝟭 A) F) (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)) ≫
              Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.inv (mapCompRight A G H)) ≫
                Iso.inv (mapCompRight A F (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
E : Type u_5
inst_4 : Category.{v_5, u_5} E
F : Functor.{v_2, v_3, u_2, u_3} B C
G : Functor.{v_3, v_4, u_3, u_4} C D
H : Functor.{v_4, v_5, u_4, u_5} D E
x : B
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_5, u_1, u_5} A E) (obj (inclRight A B ⋙ mapPair (𝟭 A) ((F ⋙ G) ⋙ H)) x)
      (obj (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ G ⋙ H)) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclRight A B)
        (Iso.hom (mapCompRight A (F ⋙ G) H) ≫
          Functor.whiskerRight (Iso.hom (mapCompRight A F G)) (mapPair (𝟭 A) H) ≫
            Iso.hom (Functor.associator (mapPair (𝟭 A) F) (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)) ≫
              Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.inv (mapCompRight A G H)) ≫
                Iso.inv (mapCompRight A F (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
E : Type u_5
inst_4 : Category.{v_5, u_5} E
F : Functor.{v_1, v_2, u_1, u_2} A B
G : Functor.{v_2, v_3, u_2, u_3} B C
H : Functor.{v_3, v_4, u_3, u_4} C D
h₁ :
  Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_4, v_5, u_4, u_5} D E) (inclLeft A E ⋙ mapPair ((F ⋙ G) ⋙ H) (𝟭 E))
      (inclLeft A E ⋙ mapPair (F ⋙ G ⋙ H) (𝟭 E)))
    (Functor.whiskerLeft (inclLeft A E) (mapWhiskerRight (F.associator G H).hom (𝟭 E)))
    (Functor.whiskerLeft (inclLeft A E)
      (Iso.hom (mapCompLeft E (F ⋙ G) H) ≫
        Functor.whiskerRight (Iso.hom (mapCompLeft E F G)) (mapPair H (𝟭 E)) ≫
          Iso.hom (Functor.associator (mapPair F (𝟭 E)) (mapPair G (𝟭 E)) (mapPair H (𝟭 E))) ≫
            Functor.whiskerLeft (mapPair F (𝟭 E)) (Iso.inv (mapCompLeft E G H)) ≫ Iso.inv (mapCompLeft E F (G ⋙ H))))
h₂ :
  Eq (α :=
    Quiver.Hom (V := E ⥤ Join.{v_4, v_5, u_4, u_5} D E) (inclRight A E ⋙ mapPair ((F ⋙ G) ⋙ H) (𝟭 E))
      (inclRight A E ⋙ mapPair (F ⋙ G ⋙ H) (𝟭 E)))
    (Functor.whiskerLeft (inclRight A E) (mapWhiskerRight (F.associator G H).hom (𝟭 E)))
    (Functor.whiskerLeft (inclRight A E)
      (Iso.hom (mapCompLeft E (F ⋙ G) H) ≫
        Functor.whiskerRight (Iso.hom (mapCompLeft E F G)) (mapPair H (𝟭 E)) ≫
          Iso.hom (Functor.associator (mapPair F (𝟭 E)) (mapPair G (𝟭 E)) (mapPair H (𝟭 E))) ≫
            Functor.whiskerLeft (mapPair F (𝟭 E)) (Iso.inv (mapCompLeft E G H)) ≫ Iso.inv (mapCompLeft E F (G ⋙ H))))
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_5, u_1, u_5} A E ⥤ Join.{v_4, v_5, u_4, u_5} D E) (mapPair ((F ⋙ G) ⋙ H) (𝟭 E))
      (mapPair (F ⋙ G ⋙ H) (𝟭 E)))
    (mapWhiskerRight (F.associator G H).hom (𝟭 E))
    (Iso.hom (mapCompLeft E (F ⋙ G) H) ≫
      Functor.whiskerRight (Iso.hom (mapCompLeft E F G)) (mapPair H (𝟭 E)) ≫
        Iso.hom (Functor.associator (mapPair F (𝟭 E)) (mapPair G (𝟭 E)) (mapPair H (𝟭 E))) ≫
          Functor.whiskerLeft (mapPair F (𝟭 E)) (Iso.inv (mapCompLeft E G H)) ≫ Iso.inv (mapCompLeft E F (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
E : Type u_5
inst_4 : Category.{v_5, u_5} E
F : Functor.{v_1, v_2, u_1, u_2} A B
G : Functor.{v_2, v_3, u_2, u_3} B C
H : Functor.{v_3, v_4, u_3, u_4} C D
h₁ :
  ∀ (x : A),
    Eq (α :=
      Quiver.Hom (V := Join.{v_4, v_5, u_4, u_5} D E) (obj (inclLeft A E ⋙ mapPair ((F ⋙ G) ⋙ H) (𝟭 E)) x)
        (obj (inclLeft A E ⋙ mapPair (F ⋙ G ⋙ H) (𝟭 E)) x))
      (NatTrans.app (Functor.whiskerLeft (inclLeft A E) (mapWhiskerRight (F.associator G H).hom (𝟭 E))) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclLeft A E)
          (Iso.hom (mapCompLeft E (F ⋙ G) H) ≫
            Functor.whiskerRight (Iso.hom (mapCompLeft E F G)) (mapPair H (𝟭 E)) ≫
              Iso.hom (Functor.associator (mapPair F (𝟭 E)) (mapPair G (𝟭 E)) (mapPair H (𝟭 E))) ≫
                Functor.whiskerLeft (mapPair F (𝟭 E)) (Iso.inv (mapCompLeft E G H)) ≫
                  Iso.inv (mapCompLeft E F (G ⋙ H))))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_4, v_5, u_4, u_5} D E) (inclLeft A E ⋙ mapPair ((F ⋙ G) ⋙ H) (𝟭 E))
      (inclLeft A E ⋙ mapPair (F ⋙ G ⋙ H) (𝟭 E)))
    (Functor.whiskerLeft (inclLeft A E) (mapWhiskerRight (F.associator G H).hom (𝟭 E)))
    (Functor.whiskerLeft (inclLeft A E)
      (Iso.hom (mapCompLeft E (F ⋙ G) H) ≫
        Functor.whiskerRight (Iso.hom (mapCompLeft E F G)) (mapPair H (𝟭 E)) ≫
          Iso.hom (Functor.associator (mapPair F (𝟭 E)) (mapPair G (𝟭 E)) (mapPair H (𝟭 E))) ≫
            Functor.whiskerLeft (mapPair F (𝟭 E)) (Iso.inv (mapCompLeft E G H)) ≫ Iso.inv (mapCompLeft E F (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
E : Type u_5
inst_4 : Category.{v_5, u_5} E
F : Functor.{v_1, v_2, u_1, u_2} A B
G : Functor.{v_2, v_3, u_2, u_3} B C
H : Functor.{v_3, v_4, u_3, u_4} C D
h₂ :
  ∀ (x : E),
    Eq (α :=
      Quiver.Hom (V := Join.{v_4, v_5, u_4, u_5} D E) (obj (inclRight A E ⋙ mapPair ((F ⋙ G) ⋙ H) (𝟭 E)) x)
        (obj (inclRight A E ⋙ mapPair (F ⋙ G ⋙ H) (𝟭 E)) x))
      (NatTrans.app (Functor.whiskerLeft (inclRight A E) (mapWhiskerRight (F.associator G H).hom (𝟭 E))) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclRight A E)
          (Iso.hom (mapCompLeft E (F ⋙ G) H) ≫
            Functor.whiskerRight (Iso.hom (mapCompLeft E F G)) (mapPair H (𝟭 E)) ≫
              Iso.hom (Functor.associator (mapPair F (𝟭 E)) (mapPair G (𝟭 E)) (mapPair H (𝟭 E))) ≫
                Functor.whiskerLeft (mapPair F (𝟭 E)) (Iso.inv (mapCompLeft E G H)) ≫
                  Iso.inv (mapCompLeft E F (G ⋙ H))))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := E ⥤ Join.{v_4, v_5, u_4, u_5} D E) (inclRight A E ⋙ mapPair ((F ⋙ G) ⋙ H) (𝟭 E))
      (inclRight A E ⋙ mapPair (F ⋙ G ⋙ H) (𝟭 E)))
    (Functor.whiskerLeft (inclRight A E) (mapWhiskerRight (F.associator G H).hom (𝟭 E)))
    (Functor.whiskerLeft (inclRight A E)
      (Iso.hom (mapCompLeft E (F ⋙ G) H) ≫
        Functor.whiskerRight (Iso.hom (mapCompLeft E F G)) (mapPair H (𝟭 E)) ≫
          Iso.hom (Functor.associator (mapPair F (𝟭 E)) (mapPair G (𝟭 E)) (mapPair H (𝟭 E))) ≫
            Functor.whiskerLeft (mapPair F (𝟭 E)) (Iso.inv (mapCompLeft E G H)) ≫ Iso.inv (mapCompLeft E F (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
E : Type u_5
inst_4 : Category.{v_5, u_5} E
F : Functor.{v_1, v_2, u_1, u_2} A B
G : Functor.{v_2, v_3, u_2, u_3} B C
H : Functor.{v_3, v_4, u_3, u_4} C D
x : A
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_4, v_5, u_4, u_5} D E) (obj (inclLeft A E ⋙ mapPair ((F ⋙ G) ⋙ H) (𝟭 E)) x)
      (obj (inclLeft A E ⋙ mapPair (F ⋙ G ⋙ H) (𝟭 E)) x))
    (NatTrans.app (Functor.whiskerLeft (inclLeft A E) (mapWhiskerRight (F.associator G H).hom (𝟭 E))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclLeft A E)
        (Iso.hom (mapCompLeft E (F ⋙ G) H) ≫
          Functor.whiskerRight (Iso.hom (mapCompLeft E F G)) (mapPair H (𝟭 E)) ≫
            Iso.hom (Functor.associator (mapPair F (𝟭 E)) (mapPair G (𝟭 E)) (mapPair H (𝟭 E))) ≫
              Functor.whiskerLeft (mapPair F (𝟭 E)) (Iso.inv (mapCompLeft E G H)) ≫ Iso.inv (mapCompLeft E F (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
E : Type u_5
inst_4 : Category.{v_5, u_5} E
F : Functor.{v_1, v_2, u_1, u_2} A B
G : Functor.{v_2, v_3, u_2, u_3} B C
H : Functor.{v_3, v_4, u_3, u_4} C D
x : E
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_4, v_5, u_4, u_5} D E) (obj (inclRight A E ⋙ mapPair ((F ⋙ G) ⋙ H) (𝟭 E)) x)
      (obj (inclRight A E ⋙ mapPair (F ⋙ G ⋙ H) (𝟭 E)) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A E) (mapWhiskerRight (F.associator G H).hom (𝟭 E))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclRight A E)
        (Iso.hom (mapCompLeft E (F ⋙ G) H) ≫
          Functor.whiskerRight (Iso.hom (mapCompLeft E F G)) (mapPair H (𝟭 E)) ≫
            Iso.hom (Functor.associator (mapPair F (𝟭 E)) (mapPair G (𝟭 E)) (mapPair H (𝟭 E))) ≫
              Functor.whiskerLeft (mapPair F (𝟭 E)) (Iso.inv (mapCompLeft E G H)) ≫ Iso.inv (mapCompLeft E F (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
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
F : Functor.{v_2, v_3, u_2, u_3} B C
h₁ :
  Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_1, v_3, u_1, u_3} A C) (inclLeft A B ⋙ mapPair (𝟭 A) (𝟭 B ⋙ F))
      (inclLeft A B ⋙ mapPair (𝟭 A) F))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A (𝟭 B) F) ≫
        Functor.whiskerRight (Iso.hom mapPairId) (mapPair (𝟭 A) F) ≫ Iso.hom (Functor.leftUnitor (mapPair (𝟭 A) F))))
h₂ :
  Eq (α :=
    Quiver.Hom (V := B ⥤ Join.{v_1, v_3, u_1, u_3} A C) (inclRight A B ⋙ mapPair (𝟭 A) (𝟭 B ⋙ F))
      (inclRight A B ⋙ mapPair (𝟭 A) F))
    (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom))
    (Functor.whiskerLeft (inclRight A B)
      (Iso.hom (mapCompRight A (𝟭 B) F) ≫
        Functor.whiskerRight (Iso.hom mapPairId) (mapPair (𝟭 A) F) ≫ Iso.hom (Functor.leftUnitor (mapPair (𝟭 A) F))))
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} A B ⥤ Join.{v_1, v_3, u_1, u_3} A C) (mapPair (𝟭 A) (𝟭 B ⋙ F))
      (mapPair (𝟭 A) F))
    (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom)
    (Iso.hom (mapCompRight A (𝟭 B) F) ≫
      Functor.whiskerRight (Iso.hom mapPairId) (mapPair (𝟭 A) F) ≫ Iso.hom (Functor.leftUnitor (mapPair (𝟭 A) F)))

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
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
F : Functor.{v_2, v_3, u_2, u_3} B C
h₁ :
  ∀ (x : A),
    Eq (α :=
      Quiver.Hom (V := Join.{v_1, v_3, u_1, u_3} A C) (obj (inclLeft A B ⋙ mapPair (𝟭 A) (𝟭 B ⋙ F)) x)
        (obj (inclLeft A B ⋙ mapPair (𝟭 A) F) x))
      (NatTrans.app (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom)) x)
      (NatTrans.app
        (Functor.whiskerLeft (inclLeft A B)
          (Iso.hom (mapCompRight A (𝟭 B) F) ≫
            Functor.whiskerRight (Iso.hom mapPairId) (mapPair (𝟭 A) F) ≫
              Iso.hom (Functor.leftUnitor (mapPair (𝟭 A) F))))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_1, v_3, u_1, u_3} A C) (inclLeft A B ⋙ mapPair (𝟭 A) (𝟭 B ⋙ F))
      (inclLeft A B ⋙ mapPair (𝟭 A) F))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A (𝟭 B) F) ≫
        Functor.whiskerRight (Iso.hom mapPairId) (mapPair (𝟭 A) F) ≫ Iso.hom (Functor.leftUnitor (mapPair (𝟭 A) F))))

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

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
F : Functor.{v_2, v_3, u_2, u_3} B C
x : A
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_3, u_1, u_3} A C) (obj (inclLeft A B ⋙ mapPair (𝟭 A) (𝟭 B ⋙ F)) x)
      (obj (inclLeft A B ⋙ mapPair (𝟭 A) F) x))
    (NatTrans.app (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom)) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclLeft A B)
        (Iso.hom (mapCompRight A (𝟭 B) F) ≫
          Functor.whiskerRight (Iso.hom mapPairId) (mapPair (𝟭 A) F) ≫ Iso.hom (Functor.leftUnitor (mapPair (𝟭 A) F))))
      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
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
F : Functor.{v_2, v_3, u_2, u_3} B C
x : B
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_3, u_1, u_3} A C) (obj (inclRight A B ⋙ mapPair (𝟭 A) (𝟭 B ⋙ F)) x)
      (obj (inclRight A B ⋙ mapPair (𝟭 A) F) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom)) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclRight A B)
        (Iso.hom (mapCompRight A (𝟭 B) F) ≫
          Functor.whiskerRight (Iso.hom mapPairId) (mapPair (𝟭 A) F) ≫ Iso.hom (Functor.leftUnitor (mapPair (𝟭 A) F))))
      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
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
F : Functor.{v_1, v_2, u_1, u_2} A B
h₁ :
  Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_2, v_3, u_2, u_3} B C) (inclLeft A C ⋙ mapPair (𝟭 A ⋙ F) (𝟭 C))
      (inclLeft A C ⋙ mapPair F (𝟭 C)))
    (Functor.whiskerLeft (inclLeft A C) (mapWhiskerRight F.leftUnitor.hom (𝟭 C)))
    (Functor.whiskerLeft (inclLeft A C)
      (Iso.hom (mapCompLeft C (𝟭 A) F) ≫
        Functor.whiskerRight (Iso.hom mapPairId) (mapPair F (𝟭 C)) ≫ Iso.hom (Functor.leftUnitor (mapPair F (𝟭 C)))))
h₂ :
  Eq (α :=
    Quiver.Hom (V := C ⥤ Join.{v_2, v_3, u_2, u_3} B C) (inclRight A C ⋙ mapPair (𝟭 A ⋙ F) (𝟭 C))
      (inclRight A C ⋙ mapPair F (𝟭 C)))
    (Functor.whiskerLeft (inclRight A C) (mapWhiskerRight F.leftUnitor.hom (𝟭 C)))
    (Functor.whiskerLeft (inclRight A C)
      (Iso.hom (mapCompLeft C (𝟭 A) F) ≫
        Functor.whiskerRight (Iso.hom mapPairId) (mapPair F (𝟭 C)) ≫ Iso.hom (Functor.leftUnitor (mapPair F (𝟭 C)))))
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_3, u_1, u_3} A C ⥤ Join.{v_2, v_3, u_2, u_3} B C) (mapPair (𝟭 A ⋙ F) (𝟭 C))
      (mapPair F (𝟭 C)))
    (mapWhiskerRight F.leftUnitor.hom (𝟭 C))
    (Iso.hom (mapCompLeft C (𝟭 A) F) ≫
      Functor.whiskerRight (Iso.hom mapPairId) (mapPair F (𝟭 C)) ≫ Iso.hom (Functor.leftUnitor (mapPair F (𝟭 C))))

Tactic:
apply natTrans_ext

Premises used: CategoryTheory.Join.natTrans_ext