-- Mathlib.CategoryTheory.Sums.Basic
_private.Mathlib.CategoryTheory.Sums.Basic.0.CategoryTheory.sum.match_5.splitter : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    (D : Type u_2) →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} D] →
        (motive :
            (X Y Z : C ⊕ D) →
              (match X, Y with
                | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
                | Sum.inl val, Sum.inr val_1 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                | Sum.inr val, Sum.inl val_1 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                | Sum.inr X, Sum.inr Y => ULift.{max u_3 u_4, u_4} (X ⟶ Y)) →
                (match Y, Z with
                  | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
                  | Sum.inl val, Sum.inr val_1 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                  | Sum.inr val, Sum.inl val_1 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                  | Sum.inr X, Sum.inr Y => ULift.{max u_3 u_4, u_4} (X ⟶ Y)) →
                  Sort u_5) →
          (X Y Z : C ⊕ D) →
            (f :
                match X, Y with
                | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
                | Sum.inl val, Sum.inr val_1 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                | Sum.inr val, Sum.inl val_1 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                | Sum.inr X, Sum.inr Y => ULift.{max u_3 u_4, u_4} (X ⟶ Y)) →
              (g :
                  match Y, Z with
                  | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
                  | Sum.inl val, Sum.inr val_1 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                  | Sum.inr val, Sum.inl val_1 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                  | Sum.inr X, Sum.inr Y => ULift.{max u_3 u_4, u_4} (X ⟶ Y)) →
                ((val val_1 val_2 : C) →
                    (f :
                        match Sum.inl val, Sum.inl val_1 with
                        | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
                        | Sum.inl val, Sum.inr val_3 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                        | Sum.inr val, Sum.inl val_3 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                        | Sum.inr X, Sum.inr Y => ULift.{max u_3 u_4, u_4} (X ⟶ Y)) →
                      (g :
                          match Sum.inl val_1, Sum.inl val_2 with
                          | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
                          | Sum.inl val, Sum.inr val_3 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                          | Sum.inr val, Sum.inl val_3 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                          | Sum.inr X, Sum.inr Y => ULift.{max u_3 u_4, u_4} (X ⟶ Y)) →
                        motive (Sum.inl val) (Sum.inl val_1) (Sum.inl val_2) f g) →
                  ((val val_1 val_2 : D) →
                      (f :
                          match Sum.inr val, Sum.inr val_1 with
                          | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
                          | Sum.inl val, Sum.inr val_3 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                          | Sum.inr val, Sum.inl val_3 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                          | Sum.inr X, Sum.inr Y => ULift.{max u_3 u_4, u_4} (X ⟶ Y)) →
                        (g :
                            match Sum.inr val_1, Sum.inr val_2 with
                            | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
                            | Sum.inl val, Sum.inr val_3 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                            | Sum.inr val, Sum.inl val_3 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
                            | Sum.inr X, Sum.inr Y => ULift.{max u_3 u_4, u_4} (X ⟶ Y)) →
                          motive (Sum.inr val) (Sum.inr val_1) (Sum.inr val_2) f g) →
                    motive X Y Z f g