-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J_1 : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := (j : K) → C (g (f j)))
      (obj
        (comp (D := (j : J) → C (g j))
          { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
            map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ }
          { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
            map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ })
        X)
      fun (i : K) ↦ Y (g (f i)))
    (map
        (comp (D := (j : J) → C (g j))
          { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
            map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ :
            ((i : I) → C i) ⥤ ((j : J) → C (g j)) }
          { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
            map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ :
            ((i : J) → C (g i)) ⥤ ((j : K) → C (g (f j))) })
        f' ≫
      fun (b : K) ↦ 𝟙 (Y (g (f b))))
    (CategoryStruct.comp (Y := fun (i : K) ↦ X (g (f i))) (fun (b : K) ↦ 𝟙 (X (g (f b)))) fun (i : K) ↦ f' (g (f i)))
have h : ∀ (x : K),
  Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x)
      (obj
        (comp (D := (j : J) → C (g j))
          { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
            map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := sorry, map_comp := sorry }
          { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
            map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := sorry, map_comp := sorry })
        X x)
      ((fun (i : K) ↦ (Y (g (f i)) : C (g (f i)))) x))
    ((map
            (comp (D := (j : J) → C (g j))
              { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
                map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := sorry, map_comp := sorry :
                ((i : I) → C i) ⥤ ((j : J) → C (g j)) }
              { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
                map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := sorry, map_comp := sorry :
                ((i : J) → C (g i)) ⥤ ((j : K) → C (g (f j))) })
            f' ≫
          fun (b : K) ↦ 𝟙 (Y (g (f b))))
        x :
      Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x)
        (obj
          (comp (D := (j : J) → C (g j))
            { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
              map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := sorry, map_comp := sorry }
            { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
              map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := sorry, map_comp := sorry })
          X x)
        ((fun (i : K) ↦ (Y (g (f i)) : C (g (f i)))) x))
    (CategoryStruct.comp (Y := fun (i : K) ↦ X (g (f i))) (fun (b : K) ↦ 𝟙 (X (g (f b)))) (fun (i : K) ↦ f' (g (f i)))
        x :
      Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x)
        (obj
          (comp (D := (j : J) → C (g j))
            { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
              map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := sorry, map_comp := sorry }
            { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
              map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := sorry, map_comp := sorry })
          X x)
        ((fun (i : K) ↦ (Y (g (f i)) : C (g (f i)))) x))
Tactic: funext