-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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 : 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)
have left : Eq (α := ULift.{v₂, v₁} (a ⟶ a_3))
  {
    down :=
      ULift.down.{v₂, v₁}
          (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)
                | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
                | left a, right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
                | 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)
                  | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
                  | left a, right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
                  | 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)
                  | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
                  | left a, right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
                  | right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
            left a, right 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, right _z, x, x_1 => PUnit.unit
          | left _x, right _y, right _z, x, x_1 => PUnit.unit
          | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) ≫
        h.down }
  (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)
        | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
        | left a, right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
        | 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)
          | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
          | left a, right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
          | 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)
          | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
          | left a, right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
          | right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
    left a, right a_1, left a_3, f,
    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)
          | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
          | left a, right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
          | 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)
            | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | 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)
            | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, right a_4 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | right a, left a_4 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
      right a_1, left a_2, left a_3, g, h with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down } with
  | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
  | left _x, left _y, right _z, x, x_1 => PUnit.unit
  | left _x, right _y, right _z, x, x_1 => PUnit.unit
  | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down })
Tactic: simp only [Hom, comp, Category.assoc]