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 := ⋯ }
⊢ IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)

Tactic:
let c₂₃'' : ∀ (i : ρ₂₃.q ⁻¹' {j}), CofanMapObjFun Z p' (i.1.1, i.1.2) :=
    fun ⟨⟨i₁, i₂₃⟩, hi⟩ => by
      refine (Cocone.precompose (Iso.hom ?_)).obj ((Cocone.whiskeringEquivalence
        (Discrete.equivalence (e i₁ i₂₃))).functor.obj (c₂₃' ⟨⟨i₁, i₂₃⟩, hi⟩))
      refine Discrete.natIso (fun ⟨⟨i₁', i₂, i₃⟩, hi⟩ => eqToIso ?_)
      obtain rfl : i₁' = i₁ := congr_arg _root_.Prod.fst hi
      rfl

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⟩))
⊢ IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)