-- 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 : ℕ
h : m ≤ n
refl :
  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 m)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op m))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op m))) → (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)) :
      (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))
step :
  ∀ {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))),
    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)))
      ((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))
⊢ 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 n)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op n))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n))) → (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 n)) :
      (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))

Tactic:
induction h with
  | refl =>
    erw [CategoryTheory.Functor.map_id, id_apply]
  | @step p h ih =>
    rw [← ih]
    have h' : m ≤ p := h
    erw [CategoryTheory.Functor.map_comp (f := (homOfLE (Nat.le_succ p)).op) (g := (homOfLE h').op),
      comp_apply, (hF p _).choose_spec]
    rfl

Premises used: CategoryTheory.id_apply, CategoryTheory.comp_apply, CategoryTheory.Functor.map_id, refl