-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
Goal:
F : ℕᵒᵖ ⥤ Type u
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (Opposite.op
                { down := { down := h : PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op p))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
        ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          (Opposite.op p)) :
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((fun (x : ℕᵒᵖ) ↦
          (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
            | Opposite.op n => preimage hF a n :
            F.obj x))
        (Opposite.op m) :
      F.obj (Opposite.op m))
h' : m ≤ p
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (Opposite.op
                { down := { down := ⋯ : PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p.succ)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p.succ))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op p.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
        ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          (Opposite.op p.succ)) :
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (Opposite.op
                { down := { down := h : PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op p))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
        ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          (Opposite.op p)) :
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
have step : Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE h').op) :
        (a : F.obj (Opposite.op p)) → F.obj (Opposite.op m))
      (preimage hF a p) :
    F.obj (Opposite.op m))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (Opposite.op
              { down := { down := h : PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p)) } :
                ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p))) })) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op p))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
      ((fun (x : ℕᵒᵖ) ↦
          (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
            | Opposite.op n => preimage hF a n :
            F.obj x))
        (Opposite.op p)) :
    (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
Tactic: erw [CategoryTheory.Functor.map_comp (f := (homOfLE (Nat.le_succ p)).op) (g := (homOfLE h').op),
      comp_apply, (hF p _).choose_spec]