-- 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₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
inst_6 :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ Y₂ : GradedObject I₂ C₂
φ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
ψ : X₃ ⟶ Y₃
⊢ Eq (α :=
    Quiver.Hom (V := GradedObject J C₄)
      (Functor.obj
        { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
          map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ, map_id := ⋯,
          map_comp := ⋯ }
        X₃)
      (Functor.obj
        { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
          map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ, map_id := ⋯,
          map_comp := ⋯ }
        Y₃))
    (Functor.map
        { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
          map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ, map_id := ⋯,
          map_comp := ⋯ : GradedObject I₃ C₃ ⥤ GradedObject J C₄ }
        ψ ≫
      mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 Y₃))
    (CategoryStruct.comp (Y :=
      Functor.obj
        { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
          map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ, map_id := ⋯,
          map_comp := ⋯ }
        X₃)
      (mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃))
      (Functor.map
        { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
          map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ, map_id := ⋯,
          map_comp := ⋯ }
        ψ))
have h : ∀ (j : J) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
  Eq (α :=
    ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶
      Functor.obj
        { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
          map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ, map_id := sorry,
          map_comp := sorry }
        Y₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((Functor.map
            { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
              map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ,
              map_id := sorry, map_comp := sorry : GradedObject I₃ C₃ ⥤ GradedObject J C₄ }
            ψ ≫
          mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 Y₃))
        j))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryStruct.comp (Y :=
        Functor.obj
          { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
            map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ,
            map_id := sorry, map_comp := sorry }
          X₃)
        (mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃))
        (Functor.map
          { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
            map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ,
            map_id := sorry, map_comp := sorry }
          ψ)
        j))
Tactic: ext j i₁ i₂ i₃ h