-- Module: Mathlib.CategoryTheory.Pi.Basic
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
h :
  ∀ (x : K),
    Eq.{v₁ + 1} (α :=
      Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x) ((fun (i : K) ↦ (X (g (f i)) : C (g (f i)))) 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 := ⋯, 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 := ⋯ })
          Y x))
      (CategoryStruct.comp (Y := fun (i : K) ↦ Y (g (f i))) (fun (i : K) ↦ f' (g (f i))) (fun (b : K) ↦ 𝟙 (Y (g (f b))))
          x :
        Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x) ((fun (i : K) ↦ (X (g (f i)) : C (g (f i)))) 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 := ⋯, 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 := ⋯ })
            Y x))
      (((fun (b : K) ↦ 𝟙 (X (g (f b)))) ≫
            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')
          x :
        Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x) ((fun (i : K) ↦ (X (g (f i)) : C (g (f i)))) 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 := ⋯, 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 := ⋯ })
            Y x))
⊢ Eq (α :=
    Quiver.Hom (V := (j : K) → C (g (f j))) (fun (i : K) ↦ X (g (f i)))
      (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 := ⋯ })
        Y))
    (CategoryStruct.comp (Y := fun (i : K) ↦ Y (g (f i))) (fun (i : K) ↦ f' (g (f i))) fun (b : K) ↦ 𝟙 (Y (g (f b))))
    ((fun (b : K) ↦ 𝟙 (X (g (f b)))) ≫
      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')

Tactic:
funext