-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
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
⊢ (∀ ⦃ι : 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
have 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
Tactic: refine forall₂_congr fun ι U ↦ ⟨fun h sf cpt ↦ ?_, fun h s hs ↦ ?_⟩