-- 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_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} 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 G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_7 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
c₂₃ : (i₂₃ : ρ₂₃.I₂₃) → (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).CofanMapObjFun ρ₂₃.p i₂₃ :=
  fun (i₂₃ : ρ₂₃.I₂₃) ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q
  j :=
  (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
hc : IsColimit c
c₂₃' : (i : (↑(ρ₂₃.q ⁻¹' {j}) : Type (max u_7 u_11))) →
  Cocone (J := Discrete (↑(ρ₂₃.p ⁻¹' {(↑i : I₁ × ρ₂₃.I₂₃).2}) : Type (max u_8 u_9)))
    (Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (↑i : I₁ × ρ₂₃.I₂₃).2) ⋙
      F.obj (X₁ (↑i : I₁ × ρ₂₃.I₂₃).1)) :=
  fun (i : (↑(ρ₂₃.q ⁻¹' {j}) : Type (max u_7 u_11))) ↦
    (F.obj (X₁ (↑i : I₁ × ρ₂₃.I₂₃).1)).mapCocone (c₂₃ (↑i : I₁ × ρ₂₃.I₂₃).2)
hc₂₃' : (i : (↑(ρ₂₃.q ⁻¹' {j}) : Type (max u_7 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_7, u_11} I₁ ρ₂₃.I₂₃ :=
  fun (x : I₁ × I₂ × I₃) ↦
    match (motive := I₁ × I₂ × I₃ → Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) x with
    | (i₁, i₂, i₃) => (i₁, ρ₂₃.p (i₂, i₃))
e : (i₁ : I₁) →
  (i₂₃ : ρ₂₃.I₂₃) →
    (↑(p' ⁻¹' {(i₁, i₂₃)}) : Type (max (max u_7 u_8) u_9)) ≃ (↑(ρ₂₃.p ⁻¹' {i₂₃}) : Type (max u_8 u_9)) :=
  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_8 u_9))) 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_8 u_9))) ↦
        match (motive :=
          (↑(ρ₂₃.p ⁻¹' {i₂₃}) : Type (max u_8 u_9)) → (↑(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_7 u_11))) →
  Z.CofanMapObjFun p' ((↑i : I₁ × ρ₂₃.I₂₃).1, (↑i : I₁ × ρ₂₃.I₂₃).2) :=
  fun (x : (↑(ρ₂₃.q ⁻¹' {j}) : Type (max u_7 u_11))) ↦
    match (motive :=
      (x : (↑(ρ₂₃.q ⁻¹' {j}) : Type (max u_7 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 G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p
                  (↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, i₂₃) hi) :
                      I₁ × ρ₂₃.I₂₃).2) ⋙
              F.obj
                (X₁
                  (↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, i₂₃) hi) :
                      I₁ × ρ₂₃.I₂₃).1)))
        (Cocone.precompose
          (Iso.hom
            (Discrete.natIso
              fun
                (x :
                  Discrete
                    (↑(p' ⁻¹'
                          {((↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, i₂₃)
                                      hi) :
                                  I₁ × ρ₂₃.I₂₃).1,
                              (↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} 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_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, i₂₃)
                                        hi) :
                                    I₁ × ρ₂₃.I₂₃).1,
                                (↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} 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_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, i₂₃)
                                    hi) :
                                I₁ × ρ₂₃.I₂₃).1,
                            (↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, i₂₃)
                                    hi) :
                                I₁ × ρ₂₃.I₂₃).2)))
                      x ≅
                    ((Discrete.equivalence (e i₁ i₂₃)).functor ⋙
                          Discrete.functor
                              ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p
                                (↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, i₂₃)
                                        hi) :
                                    I₁ × ρ₂₃.I₂₃).2) ⋙
                            F.obj
                              (X₁
                                (↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, i₂₃)
                                        hi) :
                                    I₁ × ρ₂₃.I₂₃).1)).obj
                      x)
                x with
              | { as := ⟨(i₁', i₂, i₃), hi_1⟩ } => eqToIso ⋯)))
        (Functor.obj (Equivalence.functor (Cocone.whiskeringEquivalence (Discrete.equivalence (e i₁ i₂₃))))
          (c₂₃' (Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, i₂₃) hi)))
h₂₃'' : (i : (↑(ρ₂₃.q ⁻¹' {j}) : Type (max u_7 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}
rw :
  Eq (α :=
    (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j).pt)
    (CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (↑(ρ₂₃.p ⁻¹' {ρ₂₃.p (i₂, i₃)}) : Type (max u_8 u_9))) (F :=
          (Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (ρ₂₃.p (i₂, i₃))) ⋙
              F.obj (X₁ i₁) :
            Discrete (↑(ρ₂₃.p ⁻¹' {ρ₂₃.p (i₂, i₃)}) : Type (max u_8 u_9)) ⥤ C₄))
          (c₂₃' (Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, ρ₂₃.p (i₂, i₃)) ⋯) :
            Cocone (J :=
              Discrete
                (↑(ρ₂₃.p ⁻¹'
                      {(↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j})
                                (i₁, ρ₂₃.p (i₂, i₃)) ⋯) :
                            I₁ × ρ₂₃.I₂₃).2}) :
                  Type (max u_8 u_9)))
              (Discrete.functor
                  ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p
                    (↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, ρ₂₃.p (i₂, i₃))
                            ⋯) :
                        I₁ × ρ₂₃.I₂₃).2) ⋙
                F.obj
                  (X₁
                    (↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, ρ₂₃.p (i₂, i₃))
                            ⋯) :
                        I₁ × ρ₂₃.I₂₃).1))))
        (NatTrans.app
          (Cocone.ι
            (c₂₃' (Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, ρ₂₃.p (i₂, i₃)) ⋯)))
          { as := Subtype.mk (p := fun (x : I₂ × I₃) ↦ x ∈ ρ₂₃.p ⁻¹' {ρ₂₃.p (i₂, i₃)}) (i₂, i₃) ⋯ })
        (c.ι.app
          {
            as :=
              Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, ρ₂₃.p (i₂, i₃)) ⋯ }) :
      (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ c.pt)
    ((cofan₃MapBifunctorBifunctor₂₃MapObj 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₃MapBifunctorBifunctor₂₃MapObj 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)) })
⊢ CategoryStruct.comp (Y := c.pt)
      (CategoryStruct.comp (Y :=
          Cocone.pt (J := Discrete (↑(ρ₂₃.p ⁻¹' {ρ₂₃.p (i₂, i₃)}) : Type (max u_8 u_9))) (F :=
            (Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (ρ₂₃.p (i₂, i₃))) ⋙
                F.obj (X₁ i₁) :
              Discrete (↑(ρ₂₃.p ⁻¹' {ρ₂₃.p (i₂, i₃)}) : Type (max u_8 u_9)) ⥤ C₄))
            (c₂₃' (Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, ρ₂₃.p (i₂, i₃)) ⋯) :
              Cocone (J :=
                Discrete
                  (↑(ρ₂₃.p ⁻¹'
                        {(↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j})
                                  (i₁, ρ₂₃.p (i₂, i₃)) ⋯) :
                              I₁ × ρ₂₃.I₂₃).2}) :
                    Type (max u_8 u_9)))
                (Discrete.functor
                    ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p
                      (↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j})
                              (i₁, ρ₂₃.p (i₂, i₃)) ⋯) :
                          I₁ × ρ₂₃.I₂₃).2) ⋙
                  F.obj
                    (X₁
                      (↑(Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j})
                              (i₁, ρ₂₃.p (i₂, i₃)) ⋯) :
                          I₁ × ρ₂₃.I₂₃).1))))
          (𝟙 ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃))) ≫
            NatTrans.app
              (Cocone.ι
                (c₂₃'
                  (Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, ρ₂₃.p (i₂, i₃)) ⋯)))
              { as := Subtype.mk (p := fun (x : I₂ × I₃) ↦ x ∈ ρ₂₃.p ⁻¹' {ρ₂₃.p (i₂, i₃)}) (i₂, i₃) ⋯ :
                Discrete (↑(ρ₂₃.p ⁻¹' {ρ₂₃.p (i₂, i₃)}) : Type (max u_8 u_9)) })
          (c.ι.app
            { as := Subtype.mk (p := fun (x : Prod.{u_7, u_11} I₁ ρ₂₃.I₂₃) ↦ x ∈ ρ₂₃.q ⁻¹' {j}) (i₁, ρ₂₃.p (i₂, i₃)) ⋯ :
              Discrete (↑(ρ₂₃.q ⁻¹' {j}) : Type (max u_7 u_11)) }) :
        (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ c.pt)
      (𝟙 c.pt : c.pt ⟶ c.pt) =
    (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j).ι.app
      { as := Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ r ⁻¹' {j}) (i₁, i₂, i₃) h }

Tactic:
rw [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp