-- 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
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
X : C
y : ToType (FC := TypeCat.Fun) ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))
hh :
  EffectiveEpi (X := (preimageDiagram hF X y).obj (op 0)) (Y := limit (preimageDiagram hF X y))
    (limit.π (preimageDiagram hF X y) (op 0))
⊢ Eq (α :=
    (fun (X : Type v) ↦ X)
      ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op (limit (preimageDiagram hF X y)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (InducedCategory.Hom.hom (c.π.app (op 0))) (op (limit (preimageDiagram hF X y)))) :
          (a :
              (fun (X : Type v) ↦ X)
                ((((Functor.const ℕᵒᵖ).obj c.pt).obj (op 0)).obj.obj (op (limit (preimageDiagram hF X y))))) →
            (fun (X : Type v) ↦ X) ((F.obj (op 0)).obj.obj (op (limit (preimageDiagram hF X y)))))
        ((GrothendieckTopology.yonedaEquiv (coherentTopology C) :
              (a :
                  (coherentTopology C).yoneda.obj (limit (preimageDiagram hF X y)) ⟶
                    ((Functor.const ℕᵒᵖ).obj c.pt).obj (op 0)) →
                (((Functor.const ℕᵒᵖ).obj c.pt).obj (op 0)).obj.obj (op (limit (preimageDiagram hF X y))))
            (hc.lift (cone hF X y)) :
          (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)).obj (P :=
                Presheaf.IsSheaf (coherentTopology C)).obj
            (op (limit (preimageDiagram hF X y)))) :
      (fun (X : Type v) ↦ X)
        ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op (limit (preimageDiagram hF X y)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map
              (op (limit.π (preimageDiagram hF X y) (op 0)))) :
          (a : (F.obj (op 0)).obj.obj (op X)) → (F.obj (op 0)).obj.obj (op (limit (preimageDiagram hF X y))))
        y :
      (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op (limit (preimageDiagram hF X y))))
have simp : Eq (α := (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op (limit (preimageDiagram hF X y))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (InducedCategory.Hom.hom
              ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology C)) :
                  (a : (F.obj (op 0)).obj.obj (op ((preimageDiagram hF X y).obj (op 0)))) →
                    (coherentTopology C).yoneda.obj ((preimageDiagram hF X y).obj (op 0)) ⟶ F.obj (op 0))
                (struct.x (preimageStruct hF X y) 0)))
            (op (limit (preimageDiagram hF X y)))) :
        (a :
            ((coherentTopology C).yoneda.obj ((preimageDiagram hF X y).obj (op 0))).obj.obj
              (op (limit (preimageDiagram hF X y)))) →
          (F.obj (op 0)).obj.obj (op (limit (preimageDiagram hF X y))))
      (limit.π (preimageDiagram hF X y) (op 0)) :
    (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op (limit (preimageDiagram hF X y))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map
            (op (limit.π (preimageDiagram hF X y) (op 0)))) :
        (a : (F.obj (op 0)).obj.obj (op X)) → (F.obj (op 0)).obj.obj (op (limit (preimageDiagram hF X y))))
      y :
    (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op (limit (preimageDiagram hF X y))))
Tactic: simp only [← (coherentTopology C).yonedaEquiv_comp, Functor.const_obj_obj, cone,
    IsLimit.fac, NatTrans.ofOpSequence_app, (coherentTopology C).yonedaEquiv_comp,
    (coherentTopology C).yonedaEquiv_yoneda_map]