-- 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)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
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 :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
V_eq_supr_U : V = iSup U
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_spec :
  IsGluing (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf gl
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
refine_1 :
  (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 V))) ↦
      ∀ (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 =
          sf i)
    ((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)))
      gl)
⊢ ∃! 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 V)),
    ∀ (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 =
        sf i
have refine_2 : ∀
  (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 V))),
  (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 V))) ↦
        ∀ (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 =
            sf i)
      y →
    y =
      (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)))
        gl
Tactic: refine ⟨F.1.map (eqToHom V_eq_supr_U).op gl, ?_, ?_⟩