awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a a_1 : D
g : Hom (Join.right a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)
right :
  ∀ (a_2 : C) (h : Hom (left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (Join.right a_1) (left a_2)),
    comp (comp f g) h = comp f (comp g h)
right₁ :
  ∀ (a_2 : D) (h : Hom (Join.right a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a_1) (Join.right a_2)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases c
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)
a_2 : C
h : Hom (Join.left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a_1) (Join.left a_2)
left :
  ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a_2) (Join.left a_3)), comp (comp f g) h = comp f (comp g h)
left₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (Join.left a_2) (right a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)
a_2 : D
h : Hom (right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (Join.left a_1) (right a_2)
left : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (right a_2) (Join.left a_3)), comp (comp f g) h = comp f (comp g h)
left₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_2) (right a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : C
a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)
a_2 : C
h : Hom (Join.left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (right a_1) (Join.left a_2)
left :
  ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a_2) (Join.left a_3)), comp (comp f g) h = comp f (comp g h)
left₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (Join.left a_2) (right a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : C
a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)
a_2 : D
h : Hom (right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_1) (right a_2)
left : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (right a_2) (Join.left a_3)), comp (comp f g) h = comp f (comp g h)
left₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_2) (right a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)
a_2 : C
h : Hom (left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_1) (left a_2)
right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
right₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (left a_2) (Join.right a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)
a_2 : D
h : Hom (Join.right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (left a_1) (Join.right a_2)
right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (Join.right a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
right₁ :
  ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a_2) (Join.right a_3)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)
a_2 : C
h : Hom (left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (Join.right a_1) (left a_2)
right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
right₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (left a_2) (Join.right a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)
a_2 : D
h : Hom (Join.right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a_1) (Join.right a_2)
right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (Join.right a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
right₁ :
  ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a_2) (Join.right a_3)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)
a_2 : C
g : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_1) (left a_2)
a_3 : C
h : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_2) (left a_3)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Join.comp, CategoryTheory.Join.Hom
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)
a_2 : C
g : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_1) (left a_2)
a_3 : D
h : Hom.{v₁, v₂, u₁, u₂} (left a_2) (right a_3)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Join.comp, CategoryTheory.Join.Hom
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)
a_2 : D
g : Hom.{v₁, v₂, u₁, u₂} (left a_1) (right a_2)
a_3 : D
h : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_2) (right a_3)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Join.comp, CategoryTheory.Join.Hom
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a : C
a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (left a) (right a_1)
a_2 : C
g : Hom.{v₁, v₂, u₁, u₂} (right a_1) (left a_2)
a_3 : D
h : Hom.{v₁, v₂, u₁, u₂} (left a_2) (right a_3)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Join.comp, CategoryTheory.Join.Hom
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a : C
a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (left a) (right a_1)
a_2 : D
g : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_1) (right a_2)
a_3 : D
h : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_2) (right a_3)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Join.comp, CategoryTheory.Join.Hom
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a) (right a_1)
a_2 : D
g : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_1) (right a_2)
a_3 : D
h : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_2) (right a_3)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Join.comp, CategoryTheory.Join.Hom
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : D
Y : C
f : Quiver.Hom (V := Join.{v₁, v₂, u₁, u₂} C D) (right X) (left Y)
⊢ False

Tactic:
(f : PEmpty).elim

Premises used: PEmpty.elim
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P : {x y : Join.{v₁, v₂, u₁, u₂} C D} → (x ⟶ y) → Sort u_1
left : (x y : C) → (f : x ⟶ y) → P (x := obj (inclLeft C D) x) (map (inclLeft C D) f)
right : (x y : D) → (f : x ⟶ y) → P (x := obj (inclRight C D) x) (map (inclRight C D) f)
edge : (c : C) → (d : D) → P (Join.edge c d)
x y : C
f : x ⟶ y
⊢ homInduction (P := fun (x x_1 : Join.{v₁, v₂, u₁, u₂} C D) (x_2 : x ⟶ x_1) ↦ P x_2) left right edge
      (map (inclLeft C D) f) =
    left x y f

Tactic:
rfl

Premises used: CategoryTheory.Join.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P : {x y : Join.{v₁, v₂, u₁, u₂} C D} → (x ⟶ y) → Sort u_1
left : (x y : C) → (f : x ⟶ y) → P (x := obj (inclLeft C D) x) (map (inclLeft C D) f)
right : (x y : D) → (f : x ⟶ y) → P (x := obj (inclRight C D) x) (map (inclRight C D) f)
edge : (c : C) → (d : D) → P (Join.edge c d)
x y : D
f : x ⟶ y
⊢ homInduction (P := fun (x x_1 : Join.{v₁, v₂, u₁, u₂} C D) (x_2 : x ⟶ x_1) ↦ P x_2) left right edge
      (map (inclRight C D) f) =
    right x y f

Tactic:
rfl

Premises used: CategoryTheory.Join.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P : {x y : Join.{v₁, v₂, u₁, u₂} C D} → (x ⟶ y) → Sort u_1
left : (x y : C) → (f : x ⟶ y) → P (x := obj (inclLeft C D) x) (map (inclLeft C D) f)
right : (x y : D) → (f : x ⟶ y) → P (x := obj (inclRight C D) x) (map (inclRight C D) f)
edge : (c : C) → (d : D) → P (Join.edge c d)
c : C
d : D
⊢ homInduction (P := fun (x x_1 : Join.{v₁, v₂, u₁, u₂} C D) (x_2 : x ⟶ x_1) ↦ P x_2) left right edge (Join.edge c d) =
    edge c d

Tactic:
rfl

Premises used: CategoryTheory.Join.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
⊢ Full (D := Join.{v₁, v₂, u₁, u₂} C D) (inclLeft C D)

Tactic:
inclLeftFullyFaithful C D |>.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.Join.inclLeftFullyFaithful
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
⊢ Full (D := Join.{v₁, v₂, u₁, u₂} C D) (inclRight C D)

Tactic:
inclRightFullyFaithful C D |>.full

Premises used: CategoryTheory.Join.inclRightFullyFaithful, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
⊢ Faithful (D := Join.{v₁, v₂, u₁, u₂} C D) (inclLeft C D)

Tactic:
inclLeftFullyFaithful C D |>.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.Join.inclLeftFullyFaithful
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
⊢ Faithful (D := Join.{v₁, v₂, u₁, u₂} C D) (inclRight C D)

Tactic:
inclRightFullyFaithful C D |>.faithful

Premises used: CategoryTheory.Join.inclRightFullyFaithful, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c : C
⊢ Eq (α := Quiver.Hom (V := Join.{v₁, v₂, u₁, u₂} C D) (left c) (left c))
    (𝟙 (left c) : Quiver.Hom (V := Join.{v₁, v₂, u₁, u₂} C D) (left c) (left c))
    (map (inclLeft C D) (𝟙 c) :
      Quiver.Hom (V := Join.{v₁, v₂, u₁, u₂} C D) (obj (inclLeft C D) c) (obj (inclLeft C D) c))

Tactic:
rfl

Premises used: CategoryTheory.Join.id, rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : D
⊢ Eq (α := Quiver.Hom (V := Join.{v₁, v₂, u₁, u₂} C D) (right d) (right d))
    (𝟙 (right d) : Quiver.Hom (V := Join.{v₁, v₂, u₁, u₂} C D) (right d) (right d))
    (map (inclRight C D) (𝟙 d) :
      Quiver.Hom (V := Join.{v₁, v₂, u₁, u₂} C D) (obj (inclRight C D) d) (obj (inclRight C D) d))

Tactic:
rfl

Premises used: CategoryTheory.Join.id, rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
a : C
left : F.map (𝟙 a) = 𝟙 (F.obj a)
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
        | Join.left x => F.obj x
        | right x => G.obj x :
        E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
        | Join.left x => F.obj x
        | right x => G.obj x :
        E))
    (homInduction (P := fun (x x_1 : Join.{v₁, v₂, u₁, u₂} C D) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
            | Join.left x => F.obj x
            | right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
            | Join.left x => F.obj x
            | right x => G.obj x :
            E))
        (fun (x x_1 : C) (f : x ⟶ x_1) ↦ F.map f) (fun (x x_1 : D) (g : x ⟶ x_1) ↦ G.map g) fun (c : C) (d : D) ↦
        α.app (c, d) (x := Join.left a) (𝟙 (Join.left a)) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E))
    (𝟙
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
        | Join.left x => F.obj x
        | right x => G.obj x) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E))

Tactic:
dsimp only [id_left, homInduction_left]

Premises used: CategoryTheory.Join.homInduction_left, CategoryTheory.Join.id_left
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
a : C
⊢ F.map (𝟙 a) = 𝟙 (F.obj a)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
a : D
right : G.map (𝟙 a) = 𝟙 (G.obj a)
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.right a with
        | left x => F.obj x
        | Join.right x => G.obj x :
        E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.right a with
        | left x => F.obj x
        | Join.right x => G.obj x :
        E))
    (homInduction (P := fun (x x_1 : Join.{v₁, v₂, u₁, u₂} C D) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
            | left x => F.obj x
            | Join.right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
            | left x => F.obj x
            | Join.right x => G.obj x :
            E))
        (fun (x x_1 : C) (f : x ⟶ x_1) ↦ F.map f) (fun (x x_1 : D) (g : x ⟶ x_1) ↦ G.map g) fun (c : C) (d : D) ↦
        α.app (c, d) (x := Join.right a) (𝟙 (Join.right a)) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.right a with
          | left x => F.obj x
          | Join.right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.right a with
          | left x => F.obj x
          | Join.right x => G.obj x :
          E))
    (𝟙
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.right a with
        | left x => F.obj x
        | Join.right x => G.obj x) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.right a with
          | left x => F.obj x
          | Join.right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.right a with
          | left x => F.obj x
          | Join.right x => G.obj x :
          E))

Tactic:
dsimp only [id_right, homInduction_right]

Premises used: CategoryTheory.Join.id_right, CategoryTheory.Join.homInduction_right
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
a : D
⊢ G.map (𝟙 a) = 𝟙 (G.obj a)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
c : C
⊢ (mkFunctor F G α).obj (left c) = F.obj c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
d : D
⊢ (mkFunctor F G α).obj (right d) = G.obj d

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
c c' : C
f : c ⟶ c'
⊢ (mkFunctor F G α).map (map (inclLeft C D) f) = F.map f

Tactic:
rfl

Premises used: CategoryTheory.Join.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
d d' : D
f : d ⟶ d'
⊢ (mkFunctor F G α).map (map (inclRight C D) f) = G.map f

Tactic:
rfl

Premises used: CategoryTheory.Join.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
w : ∀ (x : C × D), (whiskerRight (edgeTransform C D) (mkFunctor F G α)).app x = α.app x
⊢ whiskerRight (edgeTransform C D) (mkFunctor F G α) = α

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
x : C × D
⊢ (whiskerRight (edgeTransform C D) (mkFunctor F G α)).app x = α.app x

Tactic:
simp [mkFunctor]

Premises used: CategoryTheory.Join.mkFunctor
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
c : C
d : D
⊢ (mkFunctor F G α).map (edge c d) = α.app (c, d)

Tactic:
rfl

Premises used: CategoryTheory.Join.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
x y : C
f : x ⟶ y
⊢ Eq (α := F.obj (obj (inclLeft C D) x) ⟶ F'.obj (obj (inclLeft C D) y))
    (F.map (map (inclLeft C D) f) ≫
      match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) obj (inclLeft C D) y with
      | left x => αₗ.app x
      | right x => αᵣ.app x)
    ((match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) obj (inclLeft C D) x with
      | left x => αₗ.app x
      | right x => αᵣ.app x) ≫
      F'.map (map (inclLeft C D) f))

Tactic:
simpa using αₗ.naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
x y : D
f : x ⟶ y
⊢ Eq (α := F.obj (obj (inclRight C D) x) ⟶ F'.obj (obj (inclRight C D) y))
    (F.map (map (inclRight C D) f) ≫
      match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) obj (inclRight C D) y with
      | left x => αₗ.app x
      | right x => αᵣ.app x)
    ((match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) obj (inclRight C D) x with
      | left x => αₗ.app x
      | right x => αᵣ.app x) ≫
      F'.map (map (inclRight C D) f))

Tactic:
simpa using αᵣ.naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
c : C
d : D
⊢ Eq (α := F.obj (left c) ⟶ F'.obj (right d))
    (F.map (edge c d) ≫
      match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) right d with
      | left x => αₗ.app x
      | right x => αᵣ.app x)
    ((match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) left c with
      | left x => αₗ.app x
      | right x => αᵣ.app x) ≫
      F'.map (edge c d))

Tactic:
funext_iff.mp (NatTrans.ext_iff.mp h) (c, d)

Premises used: funext_iff, Prod.mk, Iff.mp, CategoryTheory.NatTrans.ext_iff, CategoryTheory.Join.edge