-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
x : (F.obj X).obj
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected.{u₁, u₂} (f i)
he : Finite ι
s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)
s' : IsColimit s := isColimitOfPreserves F hl
j : ι
z :
  ToType (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
    ObjectProperty.FullSubcategory.obj) ((Discrete.functor f ⋙ F).obj { as := j : Discrete ι })
h :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          ObjectProperty.FullSubcategory.obj
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _
          (s.ι.app { as := j } :
            (Discrete.functor f ⋙ F).obj { as := j : Discrete ι } ⟶
              obj (obj (const (Discrete ι)) s.pt) { as := j : Discrete ι }) :
        (a : ((Discrete.functor f ⋙ F).obj { as := j }).obj) → (((const (Discrete ι)).obj s.pt).obj { as := j }).obj)
      z =
    x
⊢ (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map (g j)) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (f j))) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      z =
    x
have subst : Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
  ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map (g j)) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (f j))) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      z :
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
  ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          ObjectProperty.FullSubcategory.obj
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _
          (s.ι.app { as := j } :
            (Discrete.functor f ⋙ F).obj { as := j : Discrete ι } ⟶
              obj (obj (const (Discrete ι)) s.pt) { as := j : Discrete ι }) :
        (a : ((Discrete.functor f ⋙ F).obj { as := j }).obj) → (((const (Discrete ι)).obj s.pt).obj { as := j }).obj)
      z :
    (obj (obj (const (Discrete ι)) s.pt) { as := j : Discrete ι }).obj)
Tactic: subst h
Cleared hypotheses: x, h