-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
X : C
y : (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X)
n : ℕ
⊢ Eq (α :=
    Functor.obj
        (Functor.obj (Functor.const ℕᵒᵖ)
          (Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) (limit (preimageDiagram hF X y))))
        (op (n + 1)) ⟶
      F.obj (op n))
    (Functor.map
        (Functor.obj (Functor.const ℕᵒᵖ)
          (Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) (limit (preimageDiagram hF X y))))
        (Quiver.Hom.op (homOfLE ⋯)) ≫
      (fun (n : ℕ) ↦
          (CategoryStruct.comp (Y :=
              Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) ((preimageDiagram hF X y).obj (op n)))
              (Functor.map (GrothendieckTopology.yoneda (coherentTopology C)) (limit.π (preimageDiagram hF X y) (op n)))
              ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology C)) :
                  (a : (F.obj (op n)).obj.obj (op ((preimageDiagram hF X y).obj (op n)))) →
                    (coherentTopology C).yoneda.obj ((preimageDiagram hF X y).obj (op n)) ⟶ F.obj (op n))
                (struct.x (preimageStruct hF X y) n)) :
            Functor.obj
                (Functor.obj (Functor.const ℕᵒᵖ)
                  (Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) (limit (preimageDiagram hF X y))))
                (op n) ⟶
              F.obj (op n)))
        n)
    (CategoryStruct.comp (Y := F.obj (op (n + 1)))
      ((fun (n : ℕ) ↦
          (CategoryStruct.comp (Y :=
              Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) ((preimageDiagram hF X y).obj (op n)))
              (Functor.map (GrothendieckTopology.yoneda (coherentTopology C)) (limit.π (preimageDiagram hF X y) (op n)))
              ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology C)) :
                  (a : (F.obj (op n)).obj.obj (op ((preimageDiagram hF X y).obj (op n)))) →
                    (coherentTopology C).yoneda.obj ((preimageDiagram hF X y).obj (op n)) ⟶ F.obj (op n))
                (struct.x (preimageStruct hF X y) n)) :
            Functor.obj
                (Functor.obj (Functor.const ℕᵒᵖ)
                  (Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) (limit (preimageDiagram hF X y))))
                (op n) ⟶
              F.obj (op n)))
        (n + 1))
      (F.map (Quiver.Hom.op (homOfLE ⋯))))
have simp : Eq (α := Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) (limit (preimageDiagram hF X y)) ⟶ F.obj (op n))
  (CategoryStruct.comp (Y :=
    Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) ((preimageDiagram hF X y).obj (op (n + 1))))
    (Functor.map (GrothendieckTopology.yoneda (coherentTopology C)) (limit.π (preimageDiagram hF X y) (op (n + 1))))
    (Functor.map (GrothendieckTopology.yoneda (coherentTopology C))
        ((preimageDiagram hF X y).map (Quiver.Hom.op (homOfLE sorry))) ≫
      (Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology C)) :
          (a : (F.obj (op n)).obj.obj (op ((preimageDiagram hF X y).obj (op n)))) →
            (coherentTopology C).yoneda.obj ((preimageDiagram hF X y).obj (op n)) ⟶ F.obj (op n))
        (struct.x (preimageStruct hF X y) n)))
  (CategoryStruct.comp (Y :=
    Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) ((preimageDiagram hF X y).obj (op (n + 1))))
    (Functor.map (GrothendieckTopology.yoneda (coherentTopology C)) (limit.π (preimageDiagram hF X y) (op (n + 1))))
    (CategoryStruct.comp (Y := F.obj (op (n + 1)))
      ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology C)) :
          (a : (F.obj (op (n + 1))).obj.obj (op ((preimageDiagram hF X y).obj (op (n + 1))))) →
            (coherentTopology C).yoneda.obj ((preimageDiagram hF X y).obj (op (n + 1))) ⟶ F.obj (op (n + 1)))
        (struct.x (preimageStruct hF X y) (n + 1)))
      (F.map (Quiver.Hom.op (homOfLE sorry)))))
Tactic: simp only [Functor.const_obj_obj, homOfLE_leOfHom, Functor.const_obj_map, Category.id_comp,
      Category.assoc, ← limit.w (preimageDiagram hF X y) (homOfLE (n.le_add_right 1)).op,
      homOfLE_leOfHom, Functor.map_comp]