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

Tactic:
cases f