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 := ⋯ }
x✝ : ↑(ρ₂₃.q ⁻¹' {j})
i₁ : I₁
i₂₃ : ρ₂₃.I₂₃
hi : (i₁, i₂₃) ∈ ρ₂₃.q ⁻¹' {j}
⊢ Discrete.functor (Z.mapObjFun p' ((↑⟨(i₁, i₂₃), hi⟩).1, (↑⟨(i₁, i₂₃), hi⟩).2)) ≅
    (Discrete.equivalence (e i₁ i₂₃)).functor ⋙
      Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (↑⟨(i₁, i₂₃), hi⟩).2) ⋙
        F.obj (X₁ (↑⟨(i₁, i₂₃), hi⟩).1)

Tactic:
refine Discrete.natIso (fun ⟨⟨i₁', i₂, i₃⟩, hi⟩ => eqToIso ?_)

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 := ⋯ }
x✝¹ : ↑(ρ₂₃.q ⁻¹' {j})
i₁ : I₁
i₂₃ : ρ₂₃.I₂₃
hi✝ : (i₁, i₂₃) ∈ ρ₂₃.q ⁻¹' {j}
x✝ : Discrete ↑(p' ⁻¹' {((↑⟨(i₁, i₂₃), hi✝⟩).1, (↑⟨(i₁, i₂₃), hi✝⟩).2)})
i₁' : I₁
i₂ : I₂
i₃ : I₃
hi : (i₁', i₂, i₃) ∈ p' ⁻¹' {((↑⟨(i₁, i₂₃), hi✝⟩).1, (↑⟨(i₁, i₂₃), hi✝⟩).2)}
⊢ (Discrete.functor (Z.mapObjFun p' ((↑⟨(i₁, i₂₃), hi✝⟩).1, (↑⟨(i₁, i₂₃), hi✝⟩).2))).obj { as := ⟨(i₁', i₂, i₃), hi⟩ } =
    ((Discrete.equivalence (e i₁ i₂₃)).functor ⋙
          Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (↑⟨(i₁, i₂₃), hi✝⟩).2) ⋙
            F.obj (X₁ (↑⟨(i₁, i₂₃), hi✝⟩).1)).obj
      { as := ⟨(i₁', i₂, i₃), hi⟩ }