-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
ℱ : Presheaf C X
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU :
  Membership.mem (α := (↑X : Type v)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (𝟙 X) :
          (a : (↑X : Type v)) → (↑X : Type v))
        x :
      (↑X : Type v))
⊢ Eq (α := (obj (pushforward C (𝟙 X)) ℱ).obj (op U) ⟶ ℱ.stalk x)
    (CategoryStruct.comp (Y :=
        ((OpenNhds.map (𝟙 X) x).op ⋙
              obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) ℱ).obj
          (op
            (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦
              Membership.mem (α := (↑X : Type v)) U
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                        (𝟙 X) :
                      (a : (↑X : Type v)) → (↑X : Type v))
                    x :
                  (↑X : Type v)))
              U hxU)))
        (ℱ.map
          ((NatTrans.op (OpenNhds.inclusionMapIso (𝟙 X) x).inv).app
            (op
              (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦
                Membership.mem (α := (↑X : Type v)) U
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          carrier) (𝟙 X) :
                        (a : (↑X : Type v)) → (↑X : Type v))
                      x :
                    (↑X : Type v)))
                U hxU))))
        (CategoryStruct.comp (Y :=
          colimit
            ((OpenNhds.map (𝟙 X) x).op ⋙
              obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) ℱ))
          (colimit.ι
            ((OpenNhds.map (𝟙 X) x).op ⋙
              obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) ℱ)
            (op
              (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦
                Membership.mem (α := (↑X : Type v)) U
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          carrier) (𝟙 X) :
                        (a : (↑X : Type v)) → (↑X : Type v))
                      x :
                    (↑X : Type v)))
                U hxU)))
          (colimit.pre (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) ℱ)
            (OpenNhds.map (𝟙 X) x).op)) :
      obj (C :=
          (OpenNhds (X := X)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                    (𝟙 X) :
                  (a : (↑X : Type v)) → (↑X : Type v))
                x))ᵒᵖ)
          (Functor.op
              (OpenNhds.inclusion
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                      (𝟙 X) :
                    (a : (↑X : Type v)) → (↑X : Type v))
                  x)) ⋙
            obj (pushforward C (𝟙 X)) ℱ)
          (op
            (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦
              Membership.mem (α := (↑X : Type v)) U
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                        (𝟙 X) :
                      (a : (↑X : Type v)) → (↑X : Type v))
                    x :
                  (↑X : Type v)))
              U hxU)) ⟶
        ℱ.stalk x)
    (colimit.ι
          (Functor.op
              (OpenNhds.inclusion
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                      (𝟙 X) :
                    (a : (↑X : Type v)) → (↑X : Type v))
                  x)) ⋙
            obj (pushforward C (𝟙 X)) ℱ)
          (op
            (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦
              Membership.mem (α := (↑X : Type v)) U
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                        (𝟙 X) :
                      (a : (↑X : Type v)) → (↑X : Type v))
                    x :
                  (↑X : Type v)))
              U hxU)) ≫
        map (stalkFunctor C x) (Pushforward.id ℱ).hom :
      (obj (pushforward C (𝟙 X)) ℱ).obj (op U) ⟶ ℱ.stalk x)
have ih : Eq.{v + 1} (α := (obj (pushforward C (𝟙 X)) ℱ).obj (op U) ⟶ ℱ.stalk x)
  (𝟙
      (ℱ.obj
        (obj (C :=
          (OpenNhds (X := X)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                    (𝟙 X) :
                  (a : (↑X : Type v)) → (↑X : Type v))
                x))ᵒᵖ)
          (Functor.op
            (OpenNhds.inclusion
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                      (𝟙 X) :
                    (a : (↑X : Type v)) → (↑X : Type v))
                  x) ⋙
              Opens.map (𝟙 X)))
          (op
            (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦
              Membership.mem (α := (↑X : Type v)) U
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                        (𝟙 X) :
                      (a : (↑X : Type v)) → (↑X : Type v))
                    x :
                  (↑X : Type v)))
              U hxU)))) ≫
    CategoryStruct.comp (Y :=
      colimit
        ((OpenNhds.map (𝟙 X) x).op ⋙
          obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) ℱ))
      (colimit.ι
        ((OpenNhds.map (𝟙 X) x).op ⋙
          obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) ℱ)
        (op
          (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦
            Membership.mem (α := (↑X : Type v)) U
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                      (𝟙 X) :
                    (a : (↑X : Type v)) → (↑X : Type v))
                  x :
                (↑X : Type v)))
            U hxU)))
      (colimit.pre (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) ℱ)
        (OpenNhds.map (𝟙 X) x).op))
  (colimit.ι
      (Functor.op
          (OpenNhds.inclusion
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                  (𝟙 X) :
                (a : (↑X : Type v)) → (↑X : Type v))
              x)) ⋙
        obj (pushforward C (𝟙 X)) ℱ)
      (op
        (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦
          Membership.mem (α := (↑X : Type v)) U
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                    (𝟙 X) :
                  (a : (↑X : Type v)) → (↑X : Type v))
                x :
              (↑X : Type v)))
          U hxU)) ≫
    map (stalkFunctor C x) (Pushforward.id ℱ).hom)
Tactic: erw [CategoryTheory.Functor.map_id]