-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this_2 : ∀ (i : J'), Finite (F'.obj i)
h_1 : Nonempty J
this : IsCofiltered.{w, u} J
u : (j : J') → F'.obj j
hu : u ∈ F'.sections
j j' : J
f : j ⟶ j'
h :
  Eq (α :=
    ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := ⋯,
            map_comp := ⋯ : AsSmall J ⥤ J } ⋙
          F ⋙ uliftFunctor.{max u w, v}).obj
      { down := j' })
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (x : ULift.{max u w, v} (F.obj j)) ↦
              { down := (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj j) → F.obj j') x.down :
                ULift.{max u w, v} (F.obj j') }) :
          (a :
              ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := ⋯,
                      map_comp := ⋯ } ⋙
                    F ⋙ uliftFunctor.{max u w, v}).obj
                { down := j }) →
            ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := ⋯,
                    map_comp := ⋯ } ⋙
                  F ⋙ uliftFunctor.{max u w, v}).obj
              { down := j' })
        (u { down := j }) :
      ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := ⋯,
              map_comp := ⋯ : AsSmall J ⥤ J } ⋙
            F ⋙ uliftFunctor.{max u w, v}).obj
        { down := j' })
    (u { down := j' } : F'.obj { down := j' })
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj j'))
        ((fun (j : J) ↦ (ULift.down (u { down := j }) : F.obj (down.obj { down := j }))) j) :
      (fun (X : Type v) ↦ X) (F.obj j'))
    ((fun (j : J) ↦ (ULift.down (u { down := j }) : F.obj (down.obj { down := j }))) j' :
      F.obj (down.obj { down := j' }))
have h₁ : Eq (α := F.obj j')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj j) → F.obj j') (ULift.down (u { down := j })) :
    F.obj j')
  (ULift.down
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (x : ULift.{max u w, v} (F.obj j)) ↦
              { down := (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj j) → F.obj j') x.down :
                ULift.{max u w, v} (F.obj j') }) :
          (a :
              ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := sorry,
                      map_comp := sorry } ⋙
                    F ⋙ uliftFunctor.{max u w, v}).obj
                { down := j }) →
            ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := sorry,
                    map_comp := sorry } ⋙
                  F ⋙ uliftFunctor.{max u w, v}).obj
              { down := j' })
        (u { down := j })) :
    F.obj (down.obj { down := j' }))
Tactic: simp_rw [← h]