-- Mathlib.CategoryTheory.Sums.Basic
_private.Mathlib.CategoryTheory.Sums.Basic.0.CategoryTheory.sum.match_5.eq_1 : ∀ (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)
  (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))
  (h_1 :
    (val val_3 val_4 : C) →
      (f :
          match Sum.inl val, Sum.inl val_3 with
          | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
          | Sum.inl val, Sum.inr val_5 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
          | Sum.inr val, Sum.inl val_5 => 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_3, Sum.inl val_4 with
            | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
            | Sum.inl val, Sum.inr val_5 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
            | Sum.inr val, Sum.inl val_5 => 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_3) (Sum.inl val_4) f g)
  (h_2 :
    (val val_3 val_4 : D) →
      (f :
          match Sum.inr val, Sum.inr val_3 with
          | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
          | Sum.inl val, Sum.inr val_5 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
          | Sum.inr val, Sum.inl val_5 => 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_3, Sum.inr val_4 with
            | Sum.inl X, Sum.inl Y => ULift.{max u_3 u_4, u_3} (X ⟶ Y)
            | Sum.inl val, Sum.inr val_5 => PEmpty.{max (u_3 + 1) (u_4 + 1)}
            | Sum.inr val, Sum.inl val_5 => 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_3) (Sum.inr val_4) f g),
  (match Sum.inl val, Sum.inl val_1, Sum.inl val_2, f, g with
    | Sum.inl val, Sum.inl val_3, Sum.inl val_4, f, g => h_1 val val_3 val_4 f g
    | Sum.inr val, Sum.inr val_3, Sum.inr val_4, f, g => h_2 val val_3 val_4 f g) =
    h_1 val val_1 val_2 f g