-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
G : Sheaf.{x, v_1, u_1} C X
f : F ⟶ G
s :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))
t :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V))
sf :
  (i : ι) →
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i)))
h :
  IsGluing (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s
hV : ∀ (i : ι), U i ≤ V
ht :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α :=
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op (U i))) :
            (a : CC (F.obj.obj (op (U i)))) → CC (G.obj.obj (op (U i))))
          (sf i) :
        CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
                (homOfLE ⋯).op) :
            (a : CC (G.obj.obj (op V))) → CC (G.obj.obj (op (U i))))
          t :
        CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
x : ι
rw :
  Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
              (homOfLE ⋯).op) :
          (a : CC (G.obj.obj (op V))) → CC (G.obj.obj (op (U x))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
              ((homOfLE ⋯).op ≫ (leSupr U x).op)) :
          (a : CC (G.obj.obj (op V))) → CC (G.obj.obj (op (U x))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U x))))
⊢ Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
              (leSupr U x).op) :
          (a : CC (G.obj.obj (op (iSup U)))) → CC (G.obj.obj (op (U x))))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op (iSup U))) :
              (a : CC (F.obj.obj (op (iSup U)))) → CC (G.obj.obj (op (iSup U))))
            s :
          CC
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj
              (op (iSup U)))) :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
              (leSupr U x).op) :
          (a : CC (G.obj.obj (op (iSup U)))) → CC (G.obj.obj (op (U x))))
        ((ConcreteCategory.hom (FC := FC) (CC := CC)
                (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
                  (homOfLE ⋯).op) :
              (a : CC (G.obj.obj (op V))) → CC (G.obj.obj (op (iSup U))))
            t :
          CC
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj
              (op (iSup U)))) :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U x))))

Tactic:
rw [← NatTrans.naturality_apply, h, ht, ← ConcreteCategory.comp_apply, ← Functor.map_comp]

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Functor.map_comp