-- 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
z : Join.{v₁, v₂, u₁, u₂} C D
c : C
d : D
g : right d ⟶ z
edge :
  ∀ (y : D) (f : d ⟶ y),
    Eq.{v₃ + 1} (α :=
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left c with
          | left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) obj (inclRight C D) y with
          | 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
              | left x => F.obj x
              | right x => G.obj x :
              E)
            (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
              | 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) (y := obj (inclRight C D) y) (Join.edge c d ≫ map (inclRight C D) f) :
        Quiver.Hom.{v₃, u₃} (V := E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left c with
            | left x => F.obj x
            | right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) obj (inclRight C D) y with
            | left x => F.obj x
            | right x => G.obj x :
            E))
      (CategoryStruct.comp (Y :=
          match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right d with
          | left x => F.obj x
          | right x => G.obj x)
          (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
                | right x => G.obj x :
                E)
              (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
                | 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)) (Join.edge c d))
          (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
                | right x => G.obj x :
                E)
              (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
                | 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 := right d) (y := obj (inclRight C D) y) (map (inclRight C D) f)) :
        Quiver.Hom.{v₃, u₃} (V := E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left c with
            | left x => F.obj x
            | right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) obj (inclRight C D) y with
            | left x => F.obj x
            | right x => G.obj x :
            E))
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left c with
        | left x => F.obj x
        | right x => G.obj x :
        E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) z with
        | 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
            | left x => F.obj x
            | right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
            | 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)) (Join.edge c d ≫ g) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left c with
          | left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) z with
          | left x => F.obj x
          | right x => G.obj x :
          E))
    (CategoryStruct.comp (Y :=
        match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right d with
        | left x => F.obj x
        | right x => G.obj x)
        (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
              | right x => G.obj x :
              E)
            (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
              | 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)) (Join.edge c d))
        (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
              | right x => G.obj x :
              E)
            (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
              | 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)) g) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left c with
          | left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) z with
          | left x => F.obj x
          | right x => G.obj x :
          E))

Tactic:
cases g