-- Module: Mathlib.CategoryTheory.Limits.Types.Images
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
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)))
⊢ 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)))

Tactic:
erw [CategoryTheory.Functor.map_comp (f := (homOfLE (Nat.le_succ p)).op) (g := (homOfLE h').op),
      comp_apply, (hF p _).choose_spec]

Premises used: Exists.choose_spec, Quiver.Hom.op, Nat.le_succ, CategoryTheory.comp_apply, CategoryTheory.homOfLE, CategoryTheory.Functor.map_comp