-- Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
theorem isSheaf_iff_isSheafUniqueGluing_types : F.IsSheaf ↔ F.IsSheafUniqueGluing

Proof state:
case refine_2
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
h :
  ∀ (sf : (i : ι) → ToType (F.obj (op (U i)))),
    F.IsCompatible U sf →
      ∃! s,
        ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
⊢ ∃! x, ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app j x = s j

Tactic:
specialize h (fun i ↦ s <| op <| Pairwise.single i) fun i j ↦
  (hs <| op <| Pairwise.Hom.left i j).trans (hs <| op <| Pairwise.Hom.right i j).symm

Result:
case refine_2
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (Functor.mapCone F (Pairwise.cocone U).op).π.app i s_1 =
        objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) i
⊢ ∃! x, ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app j x = s j

Proof state:
case refine_1
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
h :
  ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections,
    ∃! x, ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app j x = s j
sf : (i : ι) → ToType (F.obj (op (U i)))
cpt : F.IsCompatible U sf
⊢ ∃! s,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i

Tactic:
exact h _ cpt.sectionPairwise.prop

Result:
no goals

Proof state:
case h.e'_2.h.h.h.h.e'_3.h.e
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (Functor.mapCone F (Pairwise.cocone U).op).π.app i s_1 =
        objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) i
e_1✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt = ToType (F.obj (op (iSup U)))
x✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt
a✝ : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ s = objPairwiseOfFamily fun i => s (op (Pairwise.single i))

Tactic:
ext (i|⟨i,j⟩)

Result:
case h.e'_2.h.h.h.h.e'_3.h.e.h.op.single
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (Functor.mapCone F (Pairwise.cocone U).op).π.app i s_1 =
        objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) i
e_1✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt = ToType (F.obj (op (iSup U)))
x✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt
a✝ : (CategoryTheory.Pairwise ι)ᵒᵖ
i : ι
⊢ s (op (Pairwise.single i)) = objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) (op (Pairwise.single i))

case h.e'_2.h.h.h.h.e'_3.h.e.h.op.pair
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (Functor.mapCone F (Pairwise.cocone U).op).π.app i s_1 =
        objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) i
e_1✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt = ToType (F.obj (op (iSup U)))
x✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt
a✝ : (CategoryTheory.Pairwise ι)ᵒᵖ
i j : ι
⊢ s (op (Pairwise.pair i j)) = objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) (op (Pairwise.pair i j))

Proof state:
X : TopCat
F : Presheaf (Type u) X
⊢ (∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X),
      ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections,
        ∃! x, ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app j x = s j) ↔
    ∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X) (sf : (i : ι) → ToType (F.obj (op (U i)))),
      F.IsCompatible U sf →
        ∃! s,
          ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i

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

Result:
case refine_1
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
h :
  ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections,
    ∃! x, ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app j x = s j
sf : (i : ι) → ToType (F.obj (op (U i)))
cpt : F.IsCompatible U sf
⊢ ∃! s,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i

case refine_2
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
h :
  ∀ (sf : (i : ι) → ToType (F.obj (op (U i)))),
    F.IsCompatible U sf →
      ∃! s,
        ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
⊢ ∃! x, ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app j x = s j

Proof state:
case h.e'_2.h.h.h.h.e'_3.h.e.h.op.single
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (Functor.mapCone F (Pairwise.cocone U).op).π.app i s_1 =
        objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) i
e_1✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt = ToType (F.obj (op (iSup U)))
x✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt
a✝ : (CategoryTheory.Pairwise ι)ᵒᵖ
i : ι
⊢ s (op (Pairwise.single i)) = objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) (op (Pairwise.single i))

Tactic:
rfl

Result:
no goals

Proof state:
X : TopCat
F : Presheaf (Type u) X
⊢ F.IsSheaf ↔ F.IsSheafUniqueGluing

Tactic:
simp_rw [isSheaf_iff_isSheafPairwiseIntersections, IsSheafPairwiseIntersections,
  Types.isLimit_iff, IsSheafUniqueGluing, isGluing_iff_pairwise]

Result:
X : TopCat
F : Presheaf (Type u) X
⊢ (∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X),
      ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections,
        ∃! x, ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app j x = s j) ↔
    ∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X) (sf : (i : ι) → ToType (F.obj (op (U i)))),
      F.IsCompatible U sf →
        ∃! s,
          ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i