-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_6 : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_7 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun (i₁₂ : ρ₁₂.I₁₂) ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
hc : IsColimit c
c₁₂' : (i : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) →
  Cocone (J := Discrete (↑(ρ₁₂.p ⁻¹' {(↑i : ρ₁₂.I₁₂ × I₃).1}) : Type (max u_7 u_8)))
    (Discrete.functor ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p (↑i : ρ₁₂.I₁₂ × I₃).1) ⋙
      G.flip.obj (X₃ (↑i : ρ₁₂.I₁₂ × I₃).2)) :=
  fun (i : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) ↦
    (G.flip.obj (X₃ (↑i : ρ₁₂.I₁₂ × I₃).2)).mapCocone (c₁₂ (↑i : ρ₁₂.I₁₂ × I₃).1)
hc₁₂' : (i : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) → IsColimit (c₁₂' i)
Z : GradedObject (I₁ × I₂ × I₃) C₄ := (((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃
p' : I₁ × I₂ × I₃ → Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃ :=
  fun (x : I₁ × I₂ × I₃) ↦
    match (motive := I₁ × I₂ × I₃ → Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) x with
    | (i₁, i₂, i₃) => (ρ₁₂.p (i₁, i₂), i₃)
e : (i₁₂ : ρ₁₂.I₁₂) →
  (i₃ : I₃) → (↑(p' ⁻¹' {(i₁₂, i₃)}) : Type (max (max u_7 u_8) u_9)) ≃ (↑(ρ₁₂.p ⁻¹' {i₁₂}) : Type (max u_7 u_8)) :=
  fun (i₁₂ : ρ₁₂.I₁₂) (i₃ : I₃) ↦
    {
      toFun := fun (x : (↑(p' ⁻¹' {(i₁₂, i₃)}) : Type (max (max u_7 u_8) u_9))) ↦
        match (motive :=
          (↑(p' ⁻¹' {(i₁₂, i₃)}) : Type (max (max u_7 u_8) u_9)) → (↑(ρ₁₂.p ⁻¹' {i₁₂}) : Type (max u_7 u_8))) x with
        | ⟨(i₁, i₂, i₃'), hi⟩ => Subtype.mk (p := fun (x : I₁ × I₂) ↦ x ∈ ρ₁₂.p ⁻¹' {i₁₂}) (i₁, i₂) ⋯,
      invFun := fun (x : (↑(ρ₁₂.p ⁻¹' {i₁₂}) : Type (max u_7 u_8))) ↦
        match (motive :=
          (↑(ρ₁₂.p ⁻¹' {i₁₂}) : Type (max u_7 u_8)) → (↑(p' ⁻¹' {(i₁₂, i₃)}) : Type (max (max u_7 u_8) u_9))) x with
        | ⟨(i₁, i₂), hi⟩ => Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ p' ⁻¹' {(i₁₂, i₃)}) (i₁, i₂, i₃) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
c₁₂'' : (i : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) →
  Z.CofanMapObjFun p' ((↑i : ρ₁₂.I₁₂ × I₃).1, (↑i : ρ₁₂.I₁₂ × I₃).2) :=
  fun (x : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) ↦
    match (motive :=
      (x : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) →
        Z.CofanMapObjFun p' ((↑x : ρ₁₂.I₁₂ × I₃).1, (↑x : ρ₁₂.I₁₂ × I₃).2))
      x with
    | ⟨(i₁₂, i₃), hi⟩ =>
      Functor.obj (C :=
        Cocone
          ((Discrete.equivalence (e i₁₂ i₃)).functor ⋙
            Discrete.functor
                ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p
                  (↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (i₁₂, i₃) hi) :
                      ρ₁₂.I₁₂ × I₃).1) ⋙
              G.flip.obj
                (X₃
                  (↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (i₁₂, i₃) hi) :
                      ρ₁₂.I₁₂ × I₃).2)))
        (Cocone.precompose
          (Iso.hom
            (Discrete.natIso
              fun
                (x :
                  Discrete
                    (↑(p' ⁻¹'
                          {((↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (i₁₂, i₃)
                                      hi) :
                                  ρ₁₂.I₁₂ × I₃).1,
                              (↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (i₁₂, i₃)
                                      hi) :
                                  ρ₁₂.I₁₂ × I₃).2)}) :
                      Type (max (max u_7 u_8) u_9))) ↦
              match (motive :=
                (x :
                    Discrete
                      (↑(p' ⁻¹'
                            {((↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (i₁₂, i₃)
                                        hi) :
                                    ρ₁₂.I₁₂ × I₃).1,
                                (↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (i₁₂, i₃)
                                        hi) :
                                    ρ₁₂.I₁₂ × I₃).2)}) :
                        Type (max (max u_7 u_8) u_9))) →
                  Functor.obj
                      (Discrete.functor
                        (Z.mapObjFun p'
                          ((↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (i₁₂, i₃)
                                    hi) :
                                ρ₁₂.I₁₂ × I₃).1,
                            (↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (i₁₂, i₃)
                                    hi) :
                                ρ₁₂.I₁₂ × I₃).2)))
                      x ≅
                    ((Discrete.equivalence (e i₁₂ i₃)).functor ⋙
                          Discrete.functor
                              ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p
                                (↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (i₁₂, i₃)
                                        hi) :
                                    ρ₁₂.I₁₂ × I₃).1) ⋙
                            G.flip.obj
                              (X₃
                                (↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (i₁₂, i₃)
                                        hi) :
                                    ρ₁₂.I₁₂ × I₃).2)).obj
                      x)
                x with
              | { as := ⟨(i₁, i₂, i₃'), hi_1⟩ } => (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).mapIso (eqToIso ⋯))))
        (Functor.obj (Equivalence.functor (Cocone.whiskeringEquivalence (Discrete.equivalence (e i₁₂ i₃))))
          (c₁₂' (Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (i₁₂, i₃) hi)))
h₁₂'' : (i : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) → IsColimit (c₁₂'' i)
x : Discrete (↑(r ⁻¹' {j}) : Type (max (max u_7 u_8) u_9))
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : (i₁, i₂, i₃) ∈ r ⁻¹' {j}
⊢ Eq (α :=
    (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j).pt)
    (CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (↑(ρ₁₂.p ⁻¹' {ρ₁₂.p (i₁, i₂)}) : Type (max u_7 u_8))) (F :=
          (Discrete.functor ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p (ρ₁₂.p (i₁, i₂))) ⋙
              G.flip.obj (X₃ i₃) :
            Discrete (↑(ρ₁₂.p ⁻¹' {ρ₁₂.p (i₁, i₂)}) : Type (max u_7 u_8)) ⥤ C₄))
          (c₁₂' (Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (ρ₁₂.p (i₁, i₂), i₃) ⋯) :
            Cocone (J :=
              Discrete
                (↑(ρ₁₂.p ⁻¹'
                      {(↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j})
                                (ρ₁₂.p (i₁, i₂), i₃) ⋯) :
                            ρ₁₂.I₁₂ × I₃).1}) :
                  Type (max u_7 u_8)))
              (Discrete.functor
                  ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p
                    (↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (ρ₁₂.p (i₁, i₂), i₃)
                            ⋯) :
                        ρ₁₂.I₁₂ × I₃).1) ⋙
                G.flip.obj
                  (X₃
                    (↑(Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (ρ₁₂.p (i₁, i₂), i₃)
                            ⋯) :
                        ρ₁₂.I₁₂ × I₃).2))))
        (NatTrans.app
          (Cocone.ι
            (c₁₂' (Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (ρ₁₂.p (i₁, i₂), i₃) ⋯)))
          {
            as :=
              (e (ρ₁₂.p (i₁, i₂)) i₃ :
                  (a :
                      (↑((fun (x : I₁ × I₂ × I₃) ↦ (ρ₁₂.p (x.1, x.2.1), x.2.2)) ⁻¹' {(ρ₁₂.p (i₁, i₂), i₃)}) :
                        Type (max (max u_7 u_8) u_9))) →
                    (↑(ρ₁₂.p ⁻¹' {ρ₁₂.p (i₁, i₂)}) : Type (max u_7 u_8)))
                (Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦
                  Membership.mem (γ := Set (I₁ × I₂ × I₃))
                    (Set.preimage (β := Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃)
                      (fun (x : I₁ × I₂ × I₃) ↦ (ρ₁₂.p (x.1, x.2.1), x.2.2)) {(ρ₁₂.p (i₁, i₂), i₃)})
                    x)
                  (i₁, i₂, i₃) ⋯) })
        (c.ι.app
          {
            as :=
              Subtype.mk (p := fun (x : Prod.{u_11, u_9} ρ₁₂.I₁₂ I₃) ↦ x ∈ ρ₁₂.q ⁻¹' {j}) (ρ₁₂.p (i₁, i₂), i₃) ⋯ }) :
      (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ c.pt)
    ((cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j).ι.app
        { as := Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ r ⁻¹' {j}) (i₁, i₂, i₃) h } :
      Functor.obj
          (Discrete.functor ((((mapTrifunctorObj (bifunctorComp₁₂ F₁₂ G) X₁ I₂ I₃).obj X₂).obj X₃).mapObjFun r j))
          { as := Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ r ⁻¹' {j}) (i₁, i₂, i₃) h :
            Discrete (↑(r ⁻¹' {j}) : Type (max (max u_7 u_8) u_9)) } ⟶
        Functor.obj
          (Functor.obj (Functor.const (Discrete (↑(r ⁻¹' {j}) : Type (max (max u_7 u_8) u_9))))
            (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j).pt)
          { as := Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ r ⁻¹' {j}) (i₁, i₂, i₃) h :
            Discrete (↑(r ⁻¹' {j}) : Type (max (max u_7 u_8) u_9)) })

Tactic:
rfl