-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
hinj :
  ∀ x ∈ U,
    Function.Injective.{v + 1, v + 1} (α :=
      CC
        (obj (stalkFunctor C x)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (β :=
      CC
        (obj (stalkFunctor C x)
          (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f.hom)) :
        (a : CC ((stalkFunctor C x).obj F.obj)) → CC ((stalkFunctor C x).obj G.obj))
hsurj :
  ∀ (t : CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
    (x : ↥U),
    ∃ (V : Opens (↑X : Type v)) (_ : (↑x : (↑X : Type v)) ∈ V) (iVU : V ⟶ U) (s :
      ToType (FC := FC) (CC := CC)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V))),
      Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op V)) :
              (a : CC (F.obj.obj (op V))) → CC (G.obj.obj (op V)))
            s :
          CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC)
                (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map iVU.op) :
              (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op V)))
            t :
          CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V)))
t : CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
V : (x : ↥U) → Opens (↑X : Type v)
mV : ∀ (x : ↥U), (↑x : (↑X : Type v)) ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf :
  (x : ↥U) →
    ToType (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x)))
heq :
  ∀ (x : ↥U),
    Eq (α :=
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op (V x))) :
            (a : CC (F.obj.obj (op (V x)))) → CC (G.obj.obj (op (V x))))
          (sf x) :
        CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU x).op) :
            (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op (V x))))
          t :
        CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
V_cover : U ≤ iSup V
this :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))) V sf
s :
  ToType (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
s_spec :
  ∀ (i : ↥U),
    (ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU i).op) :
          (a : CC (F.obj.obj (op U))) → CC (F.obj.obj (op (V i))))
        s =
      sf i
x : ↥U
h :
  Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (f.hom.app (op U) ≫
              G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU x).op) :
          (a : CC (F.obj.obj (op U))) → CC (G.obj.obj (op (V x))))
        s :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU x).op) :
          (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op (V x))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
h₁ :
  Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU x).op ≫
              f.hom.app (op (V x))) :
          (a : CC (F.obj.obj (op U))) → CC (G.obj.obj (op (V x))))
        s :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU x).op) :
          (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op (V x))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
h₂ :
  Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op (V x))) :
          (a : CC (F.obj.obj (op (V x)))) → CC (G.obj.obj (op (V x))))
        ((ConcreteCategory.hom (FC := FC) (CC := CC)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map
                  (iVU x).op) :
              (a : CC (F.obj.obj (op U))) → CC (F.obj.obj (op (V x))))
            s :
          CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x)))) :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU x).op) :
          (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op (V x))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
h₃ :
  Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op (V x))) :
          (a : CC (F.obj.obj (op (V x)))) → CC (G.obj.obj (op (V x))))
        (sf x) :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU x).op) :
          (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op (V x))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
h₄ h₅ :
  Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU x).op) :
          (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op (V x))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU x).op) :
          (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op (V x))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
⊢ Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU x).op) :
          (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op (V x))))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op U)) :
              (a : CC (F.obj.obj (op U))) → CC (G.obj.obj (op U)))
            s :
          CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))) :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (iVU x).op) :
          (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op (V x))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))

Tactic:
rw [← ConcreteCategory.comp_apply, ← f.1.naturality, ConcreteCategory.comp_apply, s_spec, heq]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.NatTrans.naturality, CategoryTheory.InducedCategory.Hom.hom