-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₃))
i₁ : I₁
i₂₃ : ρ₂₃.I₂₃
x : (↑(p' ⁻¹' {(i₁, i₂₃)}) : Type (max (max u_7 u_8) u_9))
i₁' : I₁
i₂ : I₂
i₃ : I₃
hi : (i₁', i₂, i₃) ∈ p' ⁻¹' {(i₁, i₂₃)}
⊢ (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₃) ⋯ :
          (↑(p' ⁻¹' {(i₁, i₂₃)}) : Type (max (max u_7 u_8) u_9))))
      ((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₃) ⋯ :
            (↑(ρ₂₃.p ⁻¹' {i₂₃}) : Type (max u_8 u_9))))
        (Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ p' ⁻¹' {(i₁, i₂₃)}) (i₁', i₂, i₃) hi)) =
    Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ p' ⁻¹' {(i₁, i₂₃)}) (i₁', i₂, i₃) hi
have obtain : ∀ (hi : (i₁, i₂, i₃) ∈ p' ⁻¹' {(i₁, i₂₃)}),
  (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₃) sorry :
          (↑(p' ⁻¹' {(i₁, i₂₃)}) : Type (max (max u_7 u_8) u_9))))
      ((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₃) sorry :
            (↑(ρ₂₃.p ⁻¹' {i₂₃}) : Type (max u_8 u_9))))
        (Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ p' ⁻¹' {(i₁, i₂₃)}) (i₁, i₂, i₃) hi)) =
    Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ p' ⁻¹' {(i₁, i₂₃)}) (i₁, i₂, i₃) hi
Tactic: obtain rfl : i₁ = i₁' := by cat_disch
Cleared hypotheses: i₁', hi