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
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))))
⊢ 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 := 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: 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_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 := 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))))
have 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)
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 := 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))))
have 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)
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
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
⊢ 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)))
have 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))))
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
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))))
⊢ 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)))
have 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))))
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
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
⊢ 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))))
have 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)
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
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
⊢ 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))))
have 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)
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
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
⊢ 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))))
have 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)))))
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
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)))))
⊢ 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))))
have 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)))))
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
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
⊢ 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)))))
have h₁ : ∀ (x : A),
  Eq (α :=
    Quiver.Hom (V := Join.{v_2, v_3, u_2, u_3} B C) (obj (inclLeft A C ⋙ mapPair (𝟭 A ⋙ F) (𝟭 C)) x)
      (obj (inclLeft A C ⋙ mapPair F (𝟭 C)) x))
    (NatTrans.app (Functor.whiskerLeft (inclLeft A C) (mapWhiskerRight F.leftUnitor.hom (𝟭 C))) x)
    (NatTrans.app
      (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)))))
      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
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
⊢ 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)))))
have h₂ : ∀ (x : C),
  Eq (α :=
    Quiver.Hom (V := Join.{v_2, v_3, u_2, u_3} B C) (obj (inclRight A C ⋙ mapPair (𝟭 A ⋙ F) (𝟭 C)) x)
      (obj (inclRight A C ⋙ mapPair F (𝟭 C)) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A C) (mapWhiskerRight F.leftUnitor.hom (𝟭 C))) x)
    (NatTrans.app
      (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)))))
      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
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
⊢ 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) (F ⋙ 𝟭 C))
      (mapPair (𝟭 A) F))
    (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)
    (Iso.hom (mapCompRight A F (𝟭 C)) ≫
      Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair (𝟭 A) F)))
have h₁ : Eq (α :=
  Quiver.Hom (V := A ⥤ Join.{v_1, v_3, u_1, u_3} A C) (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ 𝟭 C))
    (inclLeft A B ⋙ mapPair (𝟭 A) F))
  (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom))
  (Functor.whiskerLeft (inclLeft A B)
    (Iso.hom (mapCompRight A F (𝟭 C)) ≫
      Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair (𝟭 A) F))))
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
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) (F ⋙ 𝟭 C))
      (inclLeft A B ⋙ mapPair (𝟭 A) F))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A F (𝟭 C)) ≫
        Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (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) (F ⋙ 𝟭 C))
      (mapPair (𝟭 A) F))
    (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)
    (Iso.hom (mapCompRight A F (𝟭 C)) ≫
      Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair (𝟭 A) F)))
have h₂ : Eq (α :=
  Quiver.Hom (V := B ⥤ Join.{v_1, v_3, u_1, u_3} A C) (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ 𝟭 C))
    (inclRight A B ⋙ mapPair (𝟭 A) F))
  (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom))
  (Functor.whiskerLeft (inclRight A B)
    (Iso.hom (mapCompRight A F (𝟭 C)) ≫
      Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair (𝟭 A) F))))
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
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
⊢ Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_1, v_3, u_1, u_3} A C) (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ 𝟭 C))
      (inclLeft A B ⋙ mapPair (𝟭 A) F))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A F (𝟭 C)) ≫
        Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair (𝟭 A) F))))
have h₁ : ∀ (x : A),
  Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_3, u_1, u_3} A C) (obj (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ 𝟭 C)) x)
      (obj (inclLeft A B ⋙ mapPair (𝟭 A) F) x))
    (NatTrans.app (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclLeft A B)
        (Iso.hom (mapCompRight A F (𝟭 C)) ≫
          Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair (𝟭 A) F))))
      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
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
⊢ Eq (α :=
    Quiver.Hom (V := B ⥤ Join.{v_1, v_3, u_1, u_3} A C) (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ 𝟭 C))
      (inclRight A B ⋙ mapPair (𝟭 A) F))
    (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom))
    (Functor.whiskerLeft (inclRight A B)
      (Iso.hom (mapCompRight A F (𝟭 C)) ≫
        Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair (𝟭 A) F))))
have h₂ : ∀ (x : B),
  Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_3, u_1, u_3} A C) (obj (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ 𝟭 C)) x)
      (obj (inclRight A B ⋙ mapPair (𝟭 A) F) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclRight A B)
        (Iso.hom (mapCompRight A F (𝟭 C)) ≫
          Functor.whiskerLeft (mapPair (𝟭 A) F) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair (𝟭 A) F))))
      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
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
⊢ 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 (F ⋙ 𝟭 B) (𝟭 C))
      (mapPair F (𝟭 C)))
    (mapWhiskerRight F.rightUnitor.hom (𝟭 C))
    (Iso.hom (mapCompLeft C F (𝟭 B)) ≫
      Functor.whiskerLeft (mapPair F (𝟭 C)) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair F (𝟭 C))))
have h₁ : Eq (α :=
  Quiver.Hom (V := A ⥤ Join.{v_2, v_3, u_2, u_3} B C) (inclLeft A C ⋙ mapPair (F ⋙ 𝟭 B) (𝟭 C))
    (inclLeft A C ⋙ mapPair F (𝟭 C)))
  (Functor.whiskerLeft (inclLeft A C) (mapWhiskerRight F.rightUnitor.hom (𝟭 C)))
  (Functor.whiskerLeft (inclLeft A C)
    (Iso.hom (mapCompLeft C F (𝟭 B)) ≫
      Functor.whiskerLeft (mapPair F (𝟭 C)) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair F (𝟭 C)))))
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
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 (F ⋙ 𝟭 B) (𝟭 C))
      (inclLeft A C ⋙ mapPair F (𝟭 C)))
    (Functor.whiskerLeft (inclLeft A C) (mapWhiskerRight F.rightUnitor.hom (𝟭 C)))
    (Functor.whiskerLeft (inclLeft A C)
      (Iso.hom (mapCompLeft C F (𝟭 B)) ≫
        Functor.whiskerLeft (mapPair F (𝟭 C)) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (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 (F ⋙ 𝟭 B) (𝟭 C))
      (mapPair F (𝟭 C)))
    (mapWhiskerRight F.rightUnitor.hom (𝟭 C))
    (Iso.hom (mapCompLeft C F (𝟭 B)) ≫
      Functor.whiskerLeft (mapPair F (𝟭 C)) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair F (𝟭 C))))
have h₂ : Eq (α :=
  Quiver.Hom (V := C ⥤ Join.{v_2, v_3, u_2, u_3} B C) (inclRight A C ⋙ mapPair (F ⋙ 𝟭 B) (𝟭 C))
    (inclRight A C ⋙ mapPair F (𝟭 C)))
  (Functor.whiskerLeft (inclRight A C) (mapWhiskerRight F.rightUnitor.hom (𝟭 C)))
  (Functor.whiskerLeft (inclRight A C)
    (Iso.hom (mapCompLeft C F (𝟭 B)) ≫
      Functor.whiskerLeft (mapPair F (𝟭 C)) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair F (𝟭 C)))))
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
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
⊢ Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_2, v_3, u_2, u_3} B C) (inclLeft A C ⋙ mapPair (F ⋙ 𝟭 B) (𝟭 C))
      (inclLeft A C ⋙ mapPair F (𝟭 C)))
    (Functor.whiskerLeft (inclLeft A C) (mapWhiskerRight F.rightUnitor.hom (𝟭 C)))
    (Functor.whiskerLeft (inclLeft A C)
      (Iso.hom (mapCompLeft C F (𝟭 B)) ≫
        Functor.whiskerLeft (mapPair F (𝟭 C)) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair F (𝟭 C)))))
have h₁ : ∀ (x : A),
  Eq (α :=
    Quiver.Hom (V := Join.{v_2, v_3, u_2, u_3} B C) (obj (inclLeft A C ⋙ mapPair (F ⋙ 𝟭 B) (𝟭 C)) x)
      (obj (inclLeft A C ⋙ mapPair F (𝟭 C)) x))
    (NatTrans.app (Functor.whiskerLeft (inclLeft A C) (mapWhiskerRight F.rightUnitor.hom (𝟭 C))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclLeft A C)
        (Iso.hom (mapCompLeft C F (𝟭 B)) ≫
          Functor.whiskerLeft (mapPair F (𝟭 C)) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair F (𝟭 C)))))
      x)
Tactic: ext