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 F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (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₁₂ ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
hc : IsColimit c
c₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) →
  Cocone
    (Discrete.functor ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p (↑i).1) ⋙ G.flip.obj (X₃ (↑i).2)) :=
  fun i ↦ (G.flip.obj (X₃ (↑i).2)).mapCocone (c₁₂ (↑i).1)
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₃) => (ρ₁₂.p (i₁, 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⟩ } =>
                  (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).mapIso (eqToIso ⋯)).hom).obj
        ((Cocone.whiskeringEquivalence (Discrete.equivalence (e i₁₂ i₃))).functor.obj (c₁₂' ⟨(i₁₂, i₃), hi⟩))
h₁₂'' : (i : ↑(ρ₁₂.q ⁻¹' {j})) → IsColimit (c₁₂'' i)
⊢ IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)

Tactic:
refine IsColimit.ofIsoColimit (isColimitCofanMapObjComp Z p' ρ₁₂.q r ρ₁₂.hpq j
    (fun ⟨i₁₂, i₃⟩ h => c₁₂'' ⟨⟨i₁₂, i₃⟩, h⟩) (fun ⟨i₁₂, i₃⟩ h => h₁₂'' ⟨⟨i₁₂, i₃⟩, h⟩) c hc)
    (Cocone.ext (Iso.refl _) (fun ⟨⟨i₁, i₂, i₃⟩, h⟩ => ?_))

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 F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (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₁₂ ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
hc : IsColimit c
c₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) →
  Cocone
    (Discrete.functor ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p (↑i).1) ⋙ G.flip.obj (X₃ (↑i).2)) :=
  fun i ↦ (G.flip.obj (X₃ (↑i).2)).mapCocone (c₁₂ (↑i).1)
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₃) => (ρ₁₂.p (i₁, 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⟩ } =>
                  (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).mapIso (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}
⊢ (Z.cofanMapObjComp p' ρ₁₂.q r ⋯ j
              (fun x h ↦
                match x, h with
                | (i₁₂, i₃), h => c₁₂'' ⟨(i₁₂, i₃), h⟩)
              c).ι.app
        { as := ⟨(i₁, i₂, i₃), h⟩ } ≫
      (Iso.refl
          (Z.cofanMapObjComp p' ρ₁₂.q r ⋯ j
              (fun x h ↦
                match x, h with
                | (i₁₂, i₃), h => c₁₂'' ⟨(i₁₂, i₃), h⟩)
              c).pt).hom =
    (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j).ι.app { as := ⟨(i₁, i₂, i₃), h⟩ }