Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: 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✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ 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 r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (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₂₃ ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q j :=
  (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
hc : IsColimit c
c₂₃' : (i : ↑(ρ₂₃.q ⁻¹' {j})) →
  Cocone (Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (↑i).2) ⋙ F.obj (X₁ (↑i).1)) :=
  fun i ↦ (F.obj (X₁ (↑i).1)).mapCocone (c₂₃ (↑i).2)
hc₂₃' : (i : ↑(ρ₂₃.q ⁻¹' {j})) → 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₃ → I₁ × ρ₂₃.I₂₃ :=
  fun x ↦
    match x with
    | (i₁, i₂, i₃) => (i₁, ρ₂₃.p (i₂, i₃))
e : (i₁ : I₁) → (i₂₃ : ρ₂₃.I₂₃) → ↑(p' ⁻¹' {(i₁, i₂₃)}) ≃ ↑(ρ₂₃.p ⁻¹' {i₂₃}) :=
  fun i₁ i₂₃ ↦
    {
      toFun := fun x ↦
        match x with
        | ⟨(i₁', i₂, i₃), hi⟩ => ⟨(i₂, i₃), ⋯⟩,
      invFun := fun x ↦
        match x with
        | ⟨(i₂, i₃), hi⟩ => ⟨(i₁, i₂, i₃), ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
c₂₃'' : (i : ↑(ρ₂₃.q ⁻¹' {j})) → Z.CofanMapObjFun p' ((↑i).1, (↑i).2) :=
  fun x ↦
    match x with
    | ⟨(i₁, i₂₃), hi⟩ =>
      (Cocone.precompose
            (Discrete.natIso fun x ↦
                match x with
                | { as := ⟨(i₁', i₂, i₃), hi_1⟩ } => eqToIso ⋯).hom).obj
        ((Cocone.whiskeringEquivalence (Discrete.equivalence (e i₁ i₂₃))).functor.obj (c₂₃' ⟨(i₁, i₂₃), hi⟩))
h₂₃'' : (i : ↑(ρ₂₃.q ⁻¹' {j})) → IsColimit (c₂₃'' i)
x✝ : Discrete ↑(r ⁻¹' {j})
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : (i₁, i₂, i₃) ∈ r ⁻¹' {j}
⊢ ((𝟙 ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃))) ≫
          (c₂₃' ⟨(i₁, ρ₂₃.p (i₂, i₃)), ⋯⟩).ι.app { as := ⟨(i₂, i₃), ⋯⟩ }) ≫
        c.ι.app { as := ⟨(i₁, ρ₂₃.p (i₂, i₃)), ⋯⟩ }) ≫
      𝟙 c.pt =
    (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j).ι.app { as := ⟨(i₁, i₂, i₃), h⟩ }

Tactic:
rw [comp_id, id_comp]

Goal state after:
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✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ 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 r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (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₂₃ ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q j :=
  (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
hc : IsColimit c
c₂₃' : (i : ↑(ρ₂₃.q ⁻¹' {j})) →
  Cocone (Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (↑i).2) ⋙ F.obj (X₁ (↑i).1)) :=
  fun i ↦ (F.obj (X₁ (↑i).1)).mapCocone (c₂₃ (↑i).2)
hc₂₃' : (i : ↑(ρ₂₃.q ⁻¹' {j})) → 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₃ → I₁ × ρ₂₃.I₂₃ :=
  fun x ↦
    match x with
    | (i₁, i₂, i₃) => (i₁, ρ₂₃.p (i₂, i₃))
e : (i₁ : I₁) → (i₂₃ : ρ₂₃.I₂₃) → ↑(p' ⁻¹' {(i₁, i₂₃)}) ≃ ↑(ρ₂₃.p ⁻¹' {i₂₃}) :=
  fun i₁ i₂₃ ↦
    {
      toFun := fun x ↦
        match x with
        | ⟨(i₁', i₂, i₃), hi⟩ => ⟨(i₂, i₃), ⋯⟩,
      invFun := fun x ↦
        match x with
        | ⟨(i₂, i₃), hi⟩ => ⟨(i₁, i₂, i₃), ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
c₂₃'' : (i : ↑(ρ₂₃.q ⁻¹' {j})) → Z.CofanMapObjFun p' ((↑i).1, (↑i).2) :=
  fun x ↦
    match x with
    | ⟨(i₁, i₂₃), hi⟩ =>
      (Cocone.precompose
            (Discrete.natIso fun x ↦
                match x with
                | { as := ⟨(i₁', i₂, i₃), hi_1⟩ } => eqToIso ⋯).hom).obj
        ((Cocone.whiskeringEquivalence (Discrete.equivalence (e i₁ i₂₃))).functor.obj (c₂₃' ⟨(i₁, i₂₃), hi⟩))
h₂₃'' : (i : ↑(ρ₂₃.q ⁻¹' {j})) → IsColimit (c₂₃'' i)
x✝ : Discrete ↑(r ⁻¹' {j})
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : (i₁, i₂, i₃) ∈ r ⁻¹' {j}
⊢ (c₂₃' ⟨(i₁, ρ₂₃.p (i₂, i₃)), ⋯⟩).ι.app { as := ⟨(i₂, i₃), ⋯⟩ } ≫ c.ι.app { as := ⟨(i₁, ρ₂₃.p (i₂, i₃)), ⋯⟩ } =
    (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j).ι.app { as := ⟨(i₁, i₂, i₃), h⟩ }