-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (Join.right 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) (Join.right a_3)
right :
  Eq (α := ULift.{v₁, v₂} (a ⟶ a_3))
    (match (motive :=
        (x x_1 x_2 : Join.{v₁, v₂, u₁, u₂} C D) →
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_1 with
            | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
            | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, Join.right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | Join.right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
            (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x_1, x_2 with
              | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
              | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
              | left a, Join.right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
              | Join.right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
              match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_2 with
              | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
              | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
              | left a, Join.right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
              | Join.right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
        Join.right a, left a_2, Join.right a_3,
        match (motive :=
          (x x_1 x_2 : Join.{v₁, v₂, u₁, u₂} C D) →
            (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_1 with
              | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
              | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
              | left a, Join.right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
              | Join.right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
              (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x_1, x_2 with
                | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
                | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
                | left a, Join.right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
                | Join.right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
                match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_2 with
                | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
                | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
                | left a, Join.right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
                | Join.right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
          Join.right a, left a_1, left a_2, f, g with
        | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
        | left _x, left _y, Join.right _z, x, x_1 => PUnit.unit
        | left _x, Join.right _y, Join.right _z, x, x_1 => PUnit.unit
        | Join.right _x, Join.right _y, Join.right _z, f, g => { down := f.down ≫ g.down },
        h with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, Join.right _z, x, x_1 => PUnit.unit
      | left _x, Join.right _y, Join.right _z, x, x_1 => PUnit.unit
      | Join.right _x, Join.right _y, Join.right _z, f, g => { down := f.down ≫ g.down } :
      match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) Join.right a,
        Join.right a_3 with
      | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
      | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
      | left a, Join.right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
      | Join.right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
    (match (motive :=
        (x x_1 x_2 : Join.{v₁, v₂, u₁, u₂} C D) →
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_1 with
            | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
            | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, Join.right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | Join.right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
            (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x_1, x_2 with
              | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
              | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
              | left a, Join.right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
              | Join.right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
              match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_2 with
              | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
              | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
              | left a, Join.right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
              | Join.right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
        Join.right a, left a_1, Join.right a_3, f, PUnit.unit with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, Join.right _z, x, x_1 => PUnit.unit
      | left _x, Join.right _y, Join.right _z, x, x_1 => PUnit.unit
      | Join.right _x, Join.right _y, Join.right _z, f, g => { down := f.down ≫ g.down } :
      match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) Join.right a,
        Join.right a_3 with
      | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
      | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
      | left a, Join.right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
      | Join.right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
⊢ 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