-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
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)
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 (iSup U)))
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
                (leSupr U i).op) :
            (a : CC (F.obj.obj (op (iSup U)))) → 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
                (leSupr U i).op) :
            (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op (U i))))
          t :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
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))) :=
  fun (i : ι) ↦
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
            (leSupr U i).op) :
        (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op (U i))))
      s
sf_compatible :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
⊢ s = t
have obtain : ∀
  (gl :
    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))))
  (gl_uniq :
    ∀
      (y :
        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)))),
      (fun
              (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)))) ↦
            IsGluing (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s)
          y →
        y = gl),
  s = t
Tactic: obtain ⟨gl, -, gl_uniq⟩ := F.existsUnique_gluing U sf sf_compatible