awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens (↑X : Type w)
F : Presheaf.{w, v, u} C X
F' : Sheaf.{w, v, u} C X
h : Opens.IsBasis (Set.range B)
α :
  Functor.op (inducedFunctor B) ⋙ F ⟶
    Functor.op (inducedFunctor B) ⋙
      F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))
i : ι
nth_rw :
  NatTrans.app
      ((restrictHomEquivHom F F' h : (a : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj) → F ⟶ F'.obj) α)
      (op (B i)) =
    ((restrictHomEquivHom F F' h).invFun ((restrictHomEquivHom F F' h).toFun α)).app (op i)
⊢ NatTrans.app
      ((restrictHomEquivHom F F' h : (a : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj) → F ⟶ F'.obj) α)
      (op (B i)) =
    α.app (op i)

Tactic:
nth_rw 2 [← (restrictHomEquivHom F F' h).left_inv α]

Premises used: TopCat.Sheaf.restrictHomEquivHom, Equiv.left_inv
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens (↑X : Type w)
F : Presheaf.{w, v, u} C X
F' : Sheaf.{w, v, u} C X
h : Opens.IsBasis (Set.range B)
α :
  Functor.op (inducedFunctor B) ⋙ F ⟶
    Functor.op (inducedFunctor B) ⋙
      F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))
i : ι
⊢ NatTrans.app
      ((restrictHomEquivHom F F' h : (a : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj) → F ⟶ F'.obj) α)
      (op (B i)) =
    ((restrictHomEquivHom F F' h).invFun ((restrictHomEquivHom F F' h).toFun α)).app (op i)

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens (↑X : Type w)
F : Presheaf.{w, v, u} C X
F' : Sheaf.{w, v, u} C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))
he :
  ∀ (i : ι),
    Eq (α :=
      F.obj (op (B i)) ⟶
        F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (B i)))
      (α.app (op (B i))) (β.app (op (B i)))
a :
  Eq (α :=
    Functor.op (inducedFunctor B) ⋙ F ⟶
      Functor.op (inducedFunctor B) ⋙
        F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))
    (((restrictHomEquivHom F F' h).symm : (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        α :
      Functor.op (inducedFunctor B) ⋙ F ⟶
        Functor.op (inducedFunctor B) ⋙
          F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))
    (((restrictHomEquivHom F F' h).symm : (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        β :
      Functor.op (inducedFunctor B) ⋙ F ⟶
        Functor.op (inducedFunctor B) ⋙
          F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))
⊢ α = β

Tactic:
apply (restrictHomEquivHom F F' h).symm.injective

Premises used: TopCat.Sheaf.restrictHomEquivHom, Equiv.injective, Equiv.symm
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens (↑X : Type w)
F : Presheaf.{w, v, u} C X
F' : Sheaf.{w, v, u} C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))
he :
  ∀ (i : ι),
    Eq (α :=
      F.obj (op (B i)) ⟶
        F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (B i)))
      (α.app (op (B i))) (β.app (op (B i)))
a :
  ∀ (i : (InducedCategory (Opens (↑X : Type w)) B)ᵒᵖ),
    Eq.{v + 1} (α :=
      (Functor.op (inducedFunctor B) ⋙ F).obj i ⟶
        (Functor.op (inducedFunctor B) ⋙
              F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))).obj
          i)
      (NatTrans.app
        (((restrictHomEquivHom F F' h).symm :
            (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
          α)
        i)
      (NatTrans.app
        (((restrictHomEquivHom F F' h).symm :
            (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
          β)
        i)
⊢ Eq (α :=
    Functor.op (inducedFunctor B) ⋙ F ⟶
      Functor.op (inducedFunctor B) ⋙
        F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))
    (((restrictHomEquivHom F F' h).symm : (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        α :
      Functor.op (inducedFunctor B) ⋙ F ⟶
        Functor.op (inducedFunctor B) ⋙
          F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))
    (((restrictHomEquivHom F F' h).symm : (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        β :
      Functor.op (inducedFunctor B) ⋙ F ⟶
        Functor.op (inducedFunctor B) ⋙
          F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))

Tactic:
ext i
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens (↑X : Type w)
F : Presheaf.{w, v, u} C X
F' : Sheaf.{w, v, u} C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))
he :
  ∀ (i : ι),
    Eq (α :=
      F.obj (op (B i)) ⟶
        F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (B i)))
      (α.app (op (B i))) (β.app (op (B i)))
i : (InducedCategory (Opens (↑X : Type w)) B)ᵒᵖ
⊢ Eq.{v + 1} (α :=
    (Functor.op (inducedFunctor B) ⋙ F).obj i ⟶
      (Functor.op (inducedFunctor B) ⋙
            F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))).obj
        i)
    (NatTrans.app
      (((restrictHomEquivHom F F' h).symm :
          (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        α)
      i)
    (NatTrans.app
      (((restrictHomEquivHom F F' h).symm :
          (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        β)
      i)

Tactic:
he i.unop

Premises used: Opposite.unop
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens (↑X : Type w)
F : Presheaf.{w, v, u} C X
F' : Sheaf.{w, v, u} C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))
he :
  ∀ (i : ι),
    Eq (α :=
      F.obj (op (B i)) ⟶
        F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (B i)))
      (α.app (op (B i))) (β.app (op (B i)))
i : (InducedCategory (Opens (↑X : Type w)) B)ᵒᵖ
⊢ Eq.{v + 1} (α :=
    (Functor.op (inducedFunctor B) ⋙ F).obj i ⟶
      (Functor.op (inducedFunctor B) ⋙
            F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))).obj
        i)
    (NatTrans.app
      (((restrictHomEquivHom F F' h).symm :
          (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        α)
      i)
    (NatTrans.app
      (((restrictHomEquivHom F F' h).symm :
          (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        β)
      i)

Tactic:
exact he i.unop

Premises used: Opposite.unop
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
F : CategoryTheory.Functor.{u_1, u_2, u_1, u_2} (Opens X) (Opens Y)
G : CategoryTheory.Functor.{u_2, u_3, u_2, u_3} (Opens Y) (Opens Z)
inst_3 : F.IsContinuous (Opens.grothendieckTopology X) (Opens.grothendieckTopology Y)
inst_4 : G.IsContinuous (Opens.grothendieckTopology Y) (Opens.grothendieckTopology Z)
⊢ (F ⋙ G).IsContinuous (Opens.grothendieckTopology X) (Opens.grothendieckTopology Z)

Tactic:
Functor.isContinuous_comp _ _ _ (Opens.grothendieckTopology _) _

Premises used: Opens.grothendieckTopology, CategoryTheory.Functor.isContinuous_comp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
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)
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
h : F.IsCompatible (FC := TypeCat.Fun) U sf
refine : objPairwiseOfFamily sf ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections
⊢ (↑(Functor.op (Pairwise.diagram U) ⋙ F).sections : Type (max u_4 u_5))

Tactic:
refine ⟨objPairwiseOfFamily sf, ?_⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
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)
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
h : F.IsCompatible (FC := TypeCat.Fun) U sf
G : CategoryTheory.Functor.{u_5, u_4, u_5, u_4 + 1} (CategoryTheory.Pairwise ι)ᵒᵖ (Type u_4) :=
  Functor.op (Pairwise.diagram U) ⋙ F
i : ι
⊢ Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.single i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.op (Pairwise.diagram U) ⋙ F).map (op (Pairwise.Hom.id_single i))) :
          (a : (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.single i)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.single i))))
        (objPairwiseOfFamily sf (op (Pairwise.single i))) :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.single i))))
    (objPairwiseOfFamily sf (op (Pairwise.single i)) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.single i)))

Tactic:
ConcreteCategory.congr_hom (G.map_id <| op <| Pairwise.single i) _

Premises used: Quiver.Hom.op, CategoryTheory.Pairwise.single, Opposite.op, CategoryTheory.Functor.map_id, CategoryTheory.Pairwise.id, CategoryTheory.ConcreteCategory.congr_hom, TopCat.Presheaf.objPairwiseOfFamily
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
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)
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
h : F.IsCompatible (FC := TypeCat.Fun) U sf
G : CategoryTheory.Functor.{u_5, u_4, u_5, u_4 + 1} (CategoryTheory.Pairwise ι)ᵒᵖ (Type u_4) :=
  Functor.op (Pairwise.diagram U) ⋙ F
i : ι
⊢ Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.single i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.op (Pairwise.diagram U) ⋙ F).map (op (Pairwise.Hom.id_single i))) :
          (a : (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.single i)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.single i))))
        (objPairwiseOfFamily sf (op (Pairwise.single i))) :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.single i))))
    (objPairwiseOfFamily sf (op (Pairwise.single i)) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.single i)))

Tactic:
exact ConcreteCategory.congr_hom (G.map_id <| op <| Pairwise.single i) _

Premises used: CategoryTheory.Pairwise.single, Opposite.op, CategoryTheory.Functor.map_id, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
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)
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
h : F.IsCompatible (FC := TypeCat.Fun) U sf
G : CategoryTheory.Functor.{u_5, u_4, u_5, u_4 + 1} (CategoryTheory.Pairwise ι)ᵒᵖ (Type u_4) :=
  Functor.op (Pairwise.diagram U) ⋙ F
i j' : ι
⊢ Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j'))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.op (Pairwise.diagram U) ⋙ F).map (op (Pairwise.Hom.left i j'))) :
          (a : (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.single i)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i j'))))
        (objPairwiseOfFamily sf (op (Pairwise.single i))) :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j'))))
    (objPairwiseOfFamily sf (op (Pairwise.pair i j')) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j')))

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
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)
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
h : F.IsCompatible (FC := TypeCat.Fun) U sf
G : CategoryTheory.Functor.{u_5, u_4, u_5, u_4 + 1} (CategoryTheory.Pairwise ι)ᵒᵖ (Type u_4) :=
  Functor.op (Pairwise.diagram U) ⋙ F
i i' : ι
⊢ Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i' i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.op (Pairwise.diagram U) ⋙ F).map (op (Pairwise.Hom.right i' i))) :
          (a : (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.single i)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i' i))))
        (objPairwiseOfFamily sf (op (Pairwise.single i))) :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i' i))))
    (objPairwiseOfFamily sf (op (Pairwise.pair i' i)) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i' i)))

Tactic:
(h i' i).symm

Premises used: Set.Mem, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Pairwise.diagramObj, CategoryTheory.homOfLE, Eq.symm, TopologicalSpace.Opens.infLERight, CategoryTheory.Pairwise.diagramMap, TopCat.Presheaf.objPairwiseOfFamily
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
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)
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
h : F.IsCompatible (FC := TypeCat.Fun) U sf
G : CategoryTheory.Functor.{u_5, u_4, u_5, u_4 + 1} (CategoryTheory.Pairwise ι)ᵒᵖ (Type u_4) :=
  Functor.op (Pairwise.diagram U) ⋙ F
i i' : ι
⊢ Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i' i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.op (Pairwise.diagram U) ⋙ F).map (op (Pairwise.Hom.right i' i))) :
          (a : (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.single i)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i' i))))
        (objPairwiseOfFamily sf (op (Pairwise.single i))) :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i' i))))
    (objPairwiseOfFamily sf (op (Pairwise.pair i' i)) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i' i)))

Tactic:
exact (h i' i).symm

Premises used: Eq.symm
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
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)
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
h : F.IsCompatible (FC := TypeCat.Fun) U sf
G : CategoryTheory.Functor.{u_5, u_4, u_5, u_4 + 1} (CategoryTheory.Pairwise ι)ᵒᵖ (Type u_4) :=
  Functor.op (Pairwise.diagram U) ⋙ F
i j : ι
⊢ Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.op (Pairwise.diagram U) ⋙ F).map (op (Pairwise.Hom.id_pair i j))) :
          (a : (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i j)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i j))))
        (objPairwiseOfFamily sf (op (Pairwise.pair i j))) :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    (objPairwiseOfFamily sf (op (Pairwise.pair i j)) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j)))

Tactic:
ConcreteCategory.congr_hom (G.map_id <| op <| Pairwise.pair i j) _

Premises used: Quiver.Hom.op, Opposite.op, CategoryTheory.Functor.map_id, CategoryTheory.Pairwise.id, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Pairwise.pair, TopCat.Presheaf.objPairwiseOfFamily
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
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)
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
h : F.IsCompatible (FC := TypeCat.Fun) U sf
G : CategoryTheory.Functor.{u_5, u_4, u_5, u_4 + 1} (CategoryTheory.Pairwise ι)ᵒᵖ (Type u_4) :=
  Functor.op (Pairwise.diagram U) ⋙ F
i j : ι
⊢ Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.op (Pairwise.diagram U) ⋙ F).map (op (Pairwise.Hom.id_pair i j))) :
          (a : (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i j)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i j))))
        (objPairwiseOfFamily sf (op (Pairwise.pair i j))) :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    (objPairwiseOfFamily sf (op (Pairwise.pair i j)) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j)))

Tactic:
exact ConcreteCategory.congr_hom (G.map_id <| op <| Pairwise.pair i j) _

Premises used: Opposite.op, CategoryTheory.Functor.map_id, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Pairwise.pair
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U)))
⊢ F.IsGluing (FC := TypeCat.Fun) U sf s ↔
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app i) :
            (a :
                (fun (X : Type u_4) ↦ X)
                  (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                    i)) →
              (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj i))
          s =
        objPairwiseOfFamily sf i

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

Premises used: CategoryTheory.Pairwise.single, Opposite.op, Iff.intro
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U)))
refine :
  ∀ (h : F.IsGluing (FC := TypeCat.Fun) U sf s) (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app i) :
          (a :
              (fun (X : Type u_4) ↦ X)
                (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                  i)) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj i))
        s =
      objPairwiseOfFamily sf i
⊢ F.IsGluing (FC := TypeCat.Fun) U sf s ↔
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app i) :
            (a :
                (fun (X : Type u_4) ↦ X)
                  (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                    i)) →
              (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj i))
          s =
        objPairwiseOfFamily sf i

Tactic:
refine ⟨fun h ↦ ?_, fun h i ↦ h (op <| Pairwise.single i)⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U)))
h : F.IsGluing (FC := TypeCat.Fun) U sf s
i : ι
⊢ Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.single i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app (op (Pairwise.single i))) :
          (a :
              (fun (X : Type u_4) ↦ X)
                (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                  (op (Pairwise.single i)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.single i))))
        s :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.single i))))
    (objPairwiseOfFamily sf (op (Pairwise.single i)) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.single i)))

Tactic:
h i

Premises used: Set.Mem, iSup, Quiver.Hom.op, CategoryTheory.Pairwise.diagramObj, TopologicalSpace.Opens.leSupr, CategoryTheory.homOfLE, CategoryTheory.Pairwise.coconeιApp, TopCat.Presheaf.objPairwiseOfFamily