awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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)))
⊢ 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))
have 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)))
Tactic: apply natTrans_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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)))
have 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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)))
have 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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))
have 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)))
Tactic: apply natTrans_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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)))
⊢ 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))
have 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)))
Tactic: apply natTrans_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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))
have 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)))
Tactic: apply natTrans_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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)))
⊢ 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))
have 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)))
Tactic: apply natTrans_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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)))
have 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))))
Tactic: apply natTrans_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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))))
⊢ 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)))
have 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))))
Tactic: apply natTrans_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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))))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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))))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
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
⊢ 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)))
have 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))))
Tactic: apply natTrans_ext