-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
refine_1 :
  ∀ (ι : Type x) (U : ι → Opens (↑X : Type x))
    (h :
      ∀ s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections,
        ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
          ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
                  (a :
                      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj
                            (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                        j) →
                    ((Pairwise.diagram U).op ⋙ F).obj j)
                x =
              s j)
    (sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))) (cpt : F.IsCompatible (FC := TypeCat.Fun) U sf),
    ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
      ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app i) :
              (a :
                  ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                    i) →
                ((Pairwise.diagram U).op ⋙ F).obj i)
            s =
          objPairwiseOfFamily sf i
refine_2 :
  ∀ (ι : Type x) (U : ι → Opens (↑X : Type x))
    (h :
      ∀ (sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))),
        F.IsCompatible (FC := TypeCat.Fun) U sf →
          ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
            ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
              (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app i) :
                    (a :
                        ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj
                              (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                          i) →
                      ((Pairwise.diagram U).op ⋙ F).obj i)
                  s =
                objPairwiseOfFamily sf i)
    (s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → (Functor.op (Pairwise.diagram U) ⋙ F).obj j)
    (hs : s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections),
    ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
      ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
              (a :
                  ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                    j) →
                ((Pairwise.diagram U).op ⋙ F).obj j)
            x =
          s j
⊢ (∀ ⦃ι : Type x⦄ (U : ι → Opens (↑X : Type x)),
      ∀ s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections,
        ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
          ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
                  (a :
                      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj
                            (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                        j) →
                    ((Pairwise.diagram U).op ⋙ F).obj j)
                x =
              s j) ↔
    ∀ ⦃ι : Type x⦄ (U : ι → Opens (↑X : Type x)) (sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))),
      F.IsCompatible (FC := TypeCat.Fun) U sf →
        ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
          ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app i) :
                  (a :
                      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj
                            (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                        i) →
                    ((Pairwise.diagram U).op ⋙ F).obj i)
                s =
              objPairwiseOfFamily sf i

Tactic:
refine forall₂_congr fun ι U ↦ ⟨fun h sf cpt ↦ ?_, fun h s hs ↦ ?_⟩

Premises used: forall₂_congr, Iff.intro