-- Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
theorem isGluing_iff_pairwise {sf s} : IsGluing F U sf s ↔
    ∀ i, (F.mapCone (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i

Proof state:
case op.pair
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i j : ι
⊢ ((Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.single i)) ≫
        ((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.left i j)))
      s =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))

Tactic:
exact congr_arg _ (h i)

Result:
no goals

Proof state:
case op.single
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i : ι
⊢ (Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.single i)) s =
    objPairwiseOfFamily sf (op (Pairwise.single i))

Tactic:
exact h i

Result:
no goals

Proof state:
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
⊢ F.IsGluing U sf s ↔
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i

Tactic:
refine ⟨fun h ↦ ?_, fun h i ↦ h (op <| Pairwise.single i)⟩

Result:
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
⊢ ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i

Proof state:
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
⊢ ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i

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

Result:
case op.single
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i : ι
⊢ (Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.single i)) s =
    objPairwiseOfFamily sf (op (Pairwise.single i))

case op.pair
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i j : ι
⊢ (Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.pair i j)) s =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))

Proof state:
case op.pair
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i j : ι
⊢ (Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.pair i j)) s =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))

Tactic:
rw [← (F.mapCone (Pairwise.cocone U).op).w (op <| Pairwise.Hom.left i j)]

Result:
case op.pair
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i j : ι
⊢ ((Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.single i)) ≫
        ((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.left i j)))
      s =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))