-- 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)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t :
  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 V))
h :
  ∀ (i : ι),
    Eq (α :=
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
          s :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
          t :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
V_eq_supr_U : V = iSup U
this :
  Eq (α :=
    CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
              (Quiver.Hom.op (eqToHom ⋯))) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (iSup U))))
        s :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
              (Quiver.Hom.op (eqToHom ⋯))) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (iSup U))))
        t :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))
h₁ :
  s =
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
              (Quiver.Hom.op (eqToHom ⋯)) ≫
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
              (Quiver.Hom.op (eqToHom V_eq_supr_U))) :
        (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op V)))
      s
h₂ :
  s =
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
            (Quiver.Hom.op (eqToHom ⋯) ≫ Quiver.Hom.op (eqToHom V_eq_supr_U))) :
        (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op V)))
      s
h₃ :
  s =
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
            (eqToHom ⋯ ≫ Quiver.Hom.op (eqToHom V_eq_supr_U))) :
        (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op V)))
      s
h₄ :
  s =
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
            (eqToHom ⋯ ≫ eqToHom ⋯)) :
        (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op V)))
      s
h₅ :
  s =
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (eqToHom ⋯)) :
        (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op V)))
      s
h₆ :
  s =
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (𝟙 (op V))) :
        (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op V)))
      s
h₇ :
  s =
    (@ConcreteCategory.hom.{u_3, v_1, u_1, u_2} _ inst FC CC _ _ _ _
          (𝟙 (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V))) :
        (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op V)))
      s
h₈ h₉ : s = s
⊢ s =
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
            (Quiver.Hom.op (eqToHom V_eq_supr_U))) :
        (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op V)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
                (Quiver.Hom.op (eqToHom ⋯))) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (iSup U))))
          s :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))

Tactic:
rw [← ConcreteCategory.comp_apply, ← F.1.map_comp, eqToHom_op, eqToHom_op, eqToHom_trans,
      eqToHom_refl, F.1.map_id, ConcreteCategory.id_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.eqToHom_refl, CategoryTheory.eqToHom_op, CategoryTheory.ConcreteCategory.id_apply, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.eqToHom_trans