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
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₁ :
  ∀ (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)
⊢ 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:
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_1, v_2, u_1, u_2} A B
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)
⊢ 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:
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_1, v_2, u_1, u_2} A B
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:
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_1, v_2, u_1, u_2} A B
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:
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) (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))))
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))))
⊢ 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)))

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) (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)
⊢ 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:
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) (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)
⊢ 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:
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) (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:
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) (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:
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 (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)))))
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)))))
⊢ 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))))

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_1, v_2, u_1, u_2} A B
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)
⊢ 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:
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_1, v_2, u_1, u_2} A B
h₂ :
  ∀ (x : C),
    Eq (α :=
      Quiver.Hom (V := Join.{v_2, v_3, u_2, u_3} B C) (obj (inclRight A C ⋙ mapPair (F ⋙ 𝟭 B) (𝟭 C)) x)
        (obj (inclRight A C ⋙ mapPair F (𝟭 C)) x))
      (NatTrans.app (Functor.whiskerLeft (inclRight A C) (mapWhiskerRight F.rightUnitor.hom (𝟭 C))) x)
      (NatTrans.app
        (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)))))
        x)
⊢ 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:
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_1, v_2, u_1, u_2} A B
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:
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_1, v_2, u_1, u_2} A B
x : C
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_2, v_3, u_2, u_3} B C) (obj (inclRight A C ⋙ mapPair (F ⋙ 𝟭 B) (𝟭 C)) x)
      (obj (inclRight A C ⋙ mapPair F (𝟭 C)) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A C) (mapWhiskerRight F.rightUnitor.hom (𝟭 C))) x)
    (NatTrans.app
      (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)))))
      x)

Tactic:
simp [mapCompLeft]

Premises used: CategoryTheory.Join.mapCompLeft
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
a b c : Cat
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ Eq (α :=
    Quiver.Hom (V := Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑a : Type u₂)) ⟶ Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑c : Type u₂)))
      (toCatHom (mapPair (𝟭 C) (f ≫ g).toFunctor)) (toCatHom (mapPair (𝟭 C) (f ≫ h).toFunctor)))
    (NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (f ◁ η).toNatTrans))
    (Iso.hom (Cat.Hom.isoMk (mapCompRight C f.toFunctor g.toFunctor)) ≫
      toCatHom (mapPair (𝟭 C) f.toFunctor) ◁ NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η.toNatTrans) ≫
        Iso.inv (Cat.Hom.isoMk (mapCompRight C f.toFunctor h.toFunctor)))

Tactic:
congr($(mapWhiskerLeft_whiskerLeft C _ _).toCatHom₂)

Premises used: congrArg, CategoryTheory.Join.mapWhiskerLeft_whiskerLeft, id, CategoryTheory.NatTrans.toCatHom₂, CategoryTheory.Cat.Hom₂.toNatTrans, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
a b c : Cat
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ Eq (α :=
    Quiver.Hom (V := Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑a : Type u₂)) ⟶ Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑c : Type u₂)))
      (toCatHom (mapPair (𝟭 C) (f ≫ g).toFunctor)) (toCatHom (mapPair (𝟭 C) (f ≫ h).toFunctor)))
    (NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (f ◁ η).toNatTrans))
    (Iso.hom (Cat.Hom.isoMk (mapCompRight C f.toFunctor g.toFunctor)) ≫
      toCatHom (mapPair (𝟭 C) f.toFunctor) ◁ NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η.toNatTrans) ≫
        Iso.inv (Cat.Hom.isoMk (mapCompRight C f.toFunctor h.toFunctor)))

Tactic:
exact congr($(mapWhiskerLeft_whiskerLeft C _ _).toCatHom₂)
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
a b c : Cat
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
⊢ Eq (α :=
    Quiver.Hom (V := Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑a : Type u₂)) ⟶ Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑c : Type u₂)))
      (toCatHom (mapPair (𝟭 C) (f ≫ h).toFunctor)) (toCatHom (mapPair (𝟭 C) (g ≫ h).toFunctor)))
    (NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (η ▷ h).toNatTrans))
    (Iso.hom (Cat.Hom.isoMk (mapCompRight C f.toFunctor h.toFunctor)) ≫
      NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η.toNatTrans) ▷ toCatHom (mapPair (𝟭 C) h.toFunctor) ≫
        Iso.inv (Cat.Hom.isoMk (mapCompRight C g.toFunctor h.toFunctor)))

Tactic:
congr($(mapWhiskerLeft_whiskerRight C _ _).toCatHom₂)

Premises used: CategoryTheory.Join.mapWhiskerLeft_whiskerRight, congrArg, id, CategoryTheory.NatTrans.toCatHom₂, CategoryTheory.Cat.Hom₂.toNatTrans, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
a b c : Cat
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
⊢ Eq (α :=
    Quiver.Hom (V := Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑a : Type u₂)) ⟶ Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑c : Type u₂)))
      (toCatHom (mapPair (𝟭 C) (f ≫ h).toFunctor)) (toCatHom (mapPair (𝟭 C) (g ≫ h).toFunctor)))
    (NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (η ▷ h).toNatTrans))
    (Iso.hom (Cat.Hom.isoMk (mapCompRight C f.toFunctor h.toFunctor)) ≫
      NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η.toNatTrans) ▷ toCatHom (mapPair (𝟭 C) h.toFunctor) ≫
        Iso.inv (Cat.Hom.isoMk (mapCompRight C g.toFunctor h.toFunctor)))

Tactic:
exact congr($(mapWhiskerLeft_whiskerRight C _ _).toCatHom₂)
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ Eq (α :=
    Quiver.Hom (V := Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑a : Type u₂)) ⟶ Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑d : Type u₂)))
      (toCatHom (mapPair (𝟭 C) ((f ≫ g) ≫ h).toFunctor)) (toCatHom (mapPair (𝟭 C) (f ≫ g ≫ h).toFunctor)))
    (NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (α_ f g h).hom.toNatTrans))
    (Iso.hom (Cat.Hom.isoMk (mapCompRight C (f ≫ g).toFunctor h.toFunctor)) ≫
      Iso.hom (Cat.Hom.isoMk (mapCompRight C f.toFunctor g.toFunctor)) ▷ toCatHom (mapPair (𝟭 C) h.toFunctor) ≫
        Iso.hom
            (α_ (toCatHom (mapPair (𝟭 C) f.toFunctor)) (toCatHom (mapPair (𝟭 C) g.toFunctor))
              (toCatHom (mapPair (𝟭 C) h.toFunctor))) ≫
          toCatHom (mapPair (𝟭 C) f.toFunctor) ◁ Iso.inv (Cat.Hom.isoMk (mapCompRight C g.toFunctor h.toFunctor)) ≫
            Iso.inv (Cat.Hom.isoMk (mapCompRight C f.toFunctor (g ≫ h).toFunctor)))

Tactic:
congr($(mapWhiskerLeft_associator_hom C _ _ _).toCatHom₂)

Premises used: congrArg, id, CategoryTheory.Join.mapWhiskerLeft_associator_hom, CategoryTheory.NatTrans.toCatHom₂, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ Eq (α :=
    Quiver.Hom (V := Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑a : Type u₂)) ⟶ Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑d : Type u₂)))
      (toCatHom (mapPair (𝟭 C) ((f ≫ g) ≫ h).toFunctor)) (toCatHom (mapPair (𝟭 C) (f ≫ g ≫ h).toFunctor)))
    (NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (α_ f g h).hom.toNatTrans))
    (Iso.hom (Cat.Hom.isoMk (mapCompRight C (f ≫ g).toFunctor h.toFunctor)) ≫
      Iso.hom (Cat.Hom.isoMk (mapCompRight C f.toFunctor g.toFunctor)) ▷ toCatHom (mapPair (𝟭 C) h.toFunctor) ≫
        Iso.hom
            (α_ (toCatHom (mapPair (𝟭 C) f.toFunctor)) (toCatHom (mapPair (𝟭 C) g.toFunctor))
              (toCatHom (mapPair (𝟭 C) h.toFunctor))) ≫
          toCatHom (mapPair (𝟭 C) f.toFunctor) ◁ Iso.inv (Cat.Hom.isoMk (mapCompRight C g.toFunctor h.toFunctor)) ≫
            Iso.inv (Cat.Hom.isoMk (mapCompRight C f.toFunctor (g ≫ h).toFunctor)))

Tactic:
exact congr($(mapWhiskerLeft_associator_hom C _ _ _).toCatHom₂)
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
a b : Cat
f : a ⟶ b
⊢ Eq (α :=
    Quiver.Hom (V := Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑a : Type u₂)) ⟶ Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑b : Type u₂)))
      (toCatHom (mapPair (𝟭 C) (𝟙 a ≫ f).toFunctor)) (toCatHom (mapPair (𝟭 C) f.toFunctor)))
    (NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (λ_ f).hom.toNatTrans))
    (Iso.hom (Cat.Hom.isoMk (mapCompRight C (Cat.Hom.toFunctor (𝟙 a)) f.toFunctor)) ≫
      Iso.hom (Cat.Hom.isoMk mapPairId) ▷ toCatHom (mapPair (𝟭 C) f.toFunctor) ≫
        Iso.hom (λ_ (toCatHom (mapPair (𝟭 C) f.toFunctor))))

Tactic:
congr($(mapWhiskerLeft_leftUnitor_hom C _).toCatHom₂)

Premises used: congrArg, id, CategoryTheory.NatTrans.toCatHom₂, CategoryTheory.Join.mapWhiskerLeft_leftUnitor_hom, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
a b : Cat
f : a ⟶ b
⊢ Eq (α :=
    Quiver.Hom (V := Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑a : Type u₂)) ⟶ Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑b : Type u₂)))
      (toCatHom (mapPair (𝟭 C) (𝟙 a ≫ f).toFunctor)) (toCatHom (mapPair (𝟭 C) f.toFunctor)))
    (NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (λ_ f).hom.toNatTrans))
    (Iso.hom (Cat.Hom.isoMk (mapCompRight C (Cat.Hom.toFunctor (𝟙 a)) f.toFunctor)) ≫
      Iso.hom (Cat.Hom.isoMk mapPairId) ▷ toCatHom (mapPair (𝟭 C) f.toFunctor) ≫
        Iso.hom (λ_ (toCatHom (mapPair (𝟭 C) f.toFunctor))))

Tactic:
exact congr($(mapWhiskerLeft_leftUnitor_hom C _).toCatHom₂)
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
a b : Cat
f : a ⟶ b
⊢ Eq (α :=
    Quiver.Hom (V := Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑a : Type u₂)) ⟶ Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑b : Type u₂)))
      (toCatHom (mapPair (𝟭 C) (f ≫ 𝟙 b).toFunctor)) (toCatHom (mapPair (𝟭 C) f.toFunctor)))
    (NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (ρ_ f).hom.toNatTrans))
    (Iso.hom (Cat.Hom.isoMk (mapCompRight C f.toFunctor (Cat.Hom.toFunctor (𝟙 b)))) ≫
      toCatHom (mapPair (𝟭 C) f.toFunctor) ◁ Iso.hom (Cat.Hom.isoMk mapPairId) ≫
        Iso.hom (ρ_ (toCatHom (mapPair (𝟭 C) f.toFunctor))))

Tactic:
congr($(mapWhiskerLeft_rightUnitor_hom C _).toCatHom₂)

Premises used: congrArg, id, CategoryTheory.Join.mapWhiskerLeft_rightUnitor_hom, CategoryTheory.NatTrans.toCatHom₂, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.CategoryTheory.Join.Pseudofunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
a b : Cat
f : a ⟶ b
⊢ Eq (α :=
    Quiver.Hom (V := Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑a : Type u₂)) ⟶ Cat.of (Join.{v₁, v₂, u₁, u₂} C (↑b : Type u₂)))
      (toCatHom (mapPair (𝟭 C) (f ≫ 𝟙 b).toFunctor)) (toCatHom (mapPair (𝟭 C) f.toFunctor)))
    (NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (ρ_ f).hom.toNatTrans))
    (Iso.hom (Cat.Hom.isoMk (mapCompRight C f.toFunctor (Cat.Hom.toFunctor (𝟙 b)))) ≫
      toCatHom (mapPair (𝟭 C) f.toFunctor) ◁ Iso.hom (Cat.Hom.isoMk mapPairId) ≫
        Iso.hom (ρ_ (toCatHom (mapPair (𝟭 C) f.toFunctor))))

Tactic:
exact congr($(mapWhiskerLeft_rightUnitor_hom C _).toCatHom₂)
-- Module: Mathlib.CategoryTheory.Join.Sum
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
c c' : C
f : c ⟶ c'
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (fromSum C D) (Functor.obj (Sum.inl_ C D) c))
      (Functor.obj (fromSum C D) (Functor.obj (Sum.inl_ C D) c')))
    (Functor.map (fromSum C D) (Functor.map (Sum.inl_ C D) f)) (Functor.map (inclLeft C D) f)

Tactic:
rfl

Premises used: CategoryTheory.Sum.homInduction, rfl