awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
this : Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))
V : (x : ↥(unop U)) → Opens (↑X : Type u)
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), (↑x : (↑X : Type u)) ∈ V x
H :
  ∀ (x : ↥(unop U)),
    Eq (α := CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          s :
        CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          t :
        CC (F.obj (op (V x))))
⊢ s = t

Tactic:
(this.isSheafFor (.ofArrows V fun x ↦ homOfLE (hV x)) ?_).isSeparatedFor.ext ?_

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.homOfLE, CategoryTheory.Presieve.IsSheaf.isSheafFor, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
this : Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))
V : (x : ↥(unop U)) → Opens (↑X : Type u)
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), (↑x : (↑X : Type u)) ∈ V x
H :
  ∀ (x : ↥(unop U)),
    Eq (α := CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          s :
        CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          t :
        CC (F.obj (op (V x))))
refine_1 :
  Membership.mem (γ := Set (Sieve (unop U)))
    ((Opens.grothendieckTopology (↑X : Type u) : (a : Opens (↑X : Type u)) → Set (Sieve a)) (unop U))
    (Sieve.generate (Presieve.ofArrows V fun (x : ↥(unop U)) ↦ homOfLE ⋯))
refine_2 :
  ∀ ⦃Y : Opens (↑X : Type u)⦄ ⦃f : Y ⟶ unop U⦄,
    Presieve.ofArrows V (fun (x : ↥(unop U)) ↦ homOfLE ⋯) f →
      Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget A (FC := FC) (CC := CC)).map f.op) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (unop U)))) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op Y)))
            s :
          (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget A (FC := FC) (CC := CC)).map f.op) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (unop U)))) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op Y)))
            t :
          (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op Y)))
⊢ s = t

Tactic:
refine (this.isSheafFor (.ofArrows V fun x ↦ homOfLE (hV x)) ?_).isSeparatedFor.ext ?_

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.homOfLE, CategoryTheory.Presieve.IsSheaf.isSheafFor, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
this : Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))
V : (x : ↥(unop U)) → Opens (↑X : Type u)
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), (↑x : (↑X : Type u)) ∈ V x
H :
  ∀ (x : ↥(unop U)),
    Eq (α := CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          s :
        CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          t :
        CC (F.obj (op (V x))))
⊢ Membership.mem (γ := Set (Sieve (unop U)))
    ((Opens.grothendieckTopology (↑X : Type u) : (a : Opens (↑X : Type u)) → Set (Sieve a)) (unop U))
    (Sieve.generate (Presieve.ofArrows V fun (x : ↥(unop U)) ↦ homOfLE ⋯))

Tactic:
fun x hx ↦ ⟨V ⟨x, hx⟩, homOfLE (hV _), Sieve.ofArrows_mk _ _ _, hxV _⟩

Premises used: Set.Mem, CategoryTheory.Sieve.ofArrows_mk, setOf, Subtype.mk, CategoryTheory.homOfLE, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
this : Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))
V : (x : ↥(unop U)) → Opens (↑X : Type u)
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), (↑x : (↑X : Type u)) ∈ V x
H :
  ∀ (x : ↥(unop U)),
    Eq (α := CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          s :
        CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          t :
        CC (F.obj (op (V x))))
⊢ Membership.mem (γ := Set (Sieve (unop U)))
    ((Opens.grothendieckTopology (↑X : Type u) : (a : Opens (↑X : Type u)) → Set (Sieve a)) (unop U))
    (Sieve.generate (Presieve.ofArrows V fun (x : ↥(unop U)) ↦ homOfLE ⋯))

Tactic:
exact fun x hx ↦ ⟨V ⟨x, hx⟩, homOfLE (hV _), Sieve.ofArrows_mk _ _ _, hxV _⟩
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
this : Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))
V : (x : ↥(unop U)) → Opens (↑X : Type u)
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), (↑x : (↑X : Type u)) ∈ V x
H :
  ∀ (x : ↥(unop U)),
    Eq (α := CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          s :
        CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          t :
        CC (F.obj (op (V x))))
Y : Opens (↑X : Type u)
x : ↥(unop U)
⊢ Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op (V x))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget A (FC := FC) (CC := CC)).map (homOfLE ⋯).op) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (unop U)))) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (V x))))
        s :
      (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op (V x))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget A (FC := FC) (CC := CC)).map (homOfLE ⋯).op) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (unop U)))) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (V x))))
        t :
      (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op (V x))))

Tactic:
H x
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
this : Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))
V : (x : ↥(unop U)) → Opens (↑X : Type u)
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), (↑x : (↑X : Type u)) ∈ V x
H :
  ∀ (x : ↥(unop U)),
    Eq (α := CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          s :
        CC (F.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
            (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
          t :
        CC (F.obj (op (V x))))
Y : Opens (↑X : Type u)
x : ↥(unop U)
⊢ Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op (V x))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget A (FC := FC) (CC := CC)).map (homOfLE ⋯).op) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (unop U)))) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (V x))))
        s :
      (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op (V x))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget A (FC := FC) (CC := CC)).map (homOfLE ⋯).op) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (unop U)))) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget A).obj (op (V x))))
        t :
      (fun (X : Type u) ↦ X) ((F ⋙ forget A (FC := FC) (CC := CC)).obj (op (V x))))

Tactic:
exact H x
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
i : ι
rw :
  CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) { as := i }) =
    F.map (leSupr U i).op
rw₁ :
  NatTrans.app (Cone.π (Fan.mk (F.obj (op (iSup U))) fun (i : ι) ↦ F.map (leSupr U i).op)) { as := i } =
    F.map (leSupr U i).op
rw₂ rw₃ : F.map (Quiver.Hom.op (leSupr U { as := i }.as)) = F.map (leSupr U i).op
⊢ CategoryStruct.comp (Y := piOpens F U) (res F U)
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) { as := i : Discrete ι }) =
    F.map (leSupr U i).op

Tactic:
rw [res, limit.lift_π, Fan.mk_π_app]

Premises used: CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app, TopCat.Presheaf.SheafConditionEqualizerProducts.res
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X_1 : TopCat
F : Presheaf.{v', v, u} C X_1
ι : Type v'
U : ι → Opens (↑X_1 : Type v')
X : C
f f' : X ⟶ piOpens F U
w :
  ∀ (j : Discrete ι),
    f ≫ limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j =
      f' ≫ limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j
⊢ f = f'

Tactic:
limit.hom_ext w

Premises used: CategoryTheory.Limits.limit.hom_ext, TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X_1 : TopCat
F : Presheaf.{v', v, u} C X_1
ι : Type v'
U : ι → Opens (↑X_1 : Type v')
X : C
f f' : X ⟶ piInters F U
w :
  ∀ (j : Discrete (ι × ι)),
    f ≫ limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j =
      f' ≫ limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j
⊢ f = f'

Tactic:
limit.hom_ext w

Premises used: CategoryTheory.Limits.limit.hom_ext, TopCat.Presheaf.SheafConditionEqualizerProducts.piInters
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
dsimp :
  Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ piInters F U)
    (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
      (Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
    (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
      (Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))))
⊢ Eq (α := F.obj (op (iSup U)) ⟶ piInters F U) (res F U ≫ leftRes F U) (res F U ≫ rightRes F U)

Tactic:
dsimp [res, leftRes, rightRes]

Premises used: TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes, TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes, TopCat.Presheaf.SheafConditionEqualizerProducts.res
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
w₁ :
  ∀ (j : Discrete (ι × ι)),
    Eq.{v + 1} (α :=
      F.obj (op (iSup U)) ⟶
        Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
      (CategoryStruct.comp (Y := piInters F U)
        (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
          (Pi.lift fun (p : ι × ι) ↦
            Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j))
      (CategoryStruct.comp (Y := piInters F U)
        (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
          (Pi.lift fun (p : ι × ι) ↦
            Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j))
⊢ Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ piInters F U)
    (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
      (Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
    (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
      (Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))))

Tactic:
ext
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
j : Discrete (ι × ι)
w₁ :
  Eq (α :=
    F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (F.map (Quiver.Hom.op (leSupr U j.as.1)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
    (F.map (Quiver.Hom.op (leSupr U j.as.2)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLERight (U j.as.2))))
⊢ Eq.{v + 1} (α :=
    F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (CategoryStruct.comp (Y := piInters F U)
      (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
        (Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j))
    (CategoryStruct.comp (Y := piInters F U)
      (CategoryStruct.comp (Y := piOpens F U) (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
        (Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j))

Tactic:
simp only [limit.lift_π, limit.lift_π_assoc, Fan.mk_π_app, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
j : Discrete (ι × ι)
w₁ :
  Eq (α :=
    F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (F.map (Quiver.Hom.op (leSupr U j.as.1) ≫ Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
    (F.map (Quiver.Hom.op (leSupr U j.as.2)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLERight (U j.as.2))))
⊢ Eq (α :=
    F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (F.map (Quiver.Hom.op (leSupr U j.as.1)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
    (F.map (Quiver.Hom.op (leSupr U j.as.2)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLERight (U j.as.2))))

Tactic:
rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
j : Discrete (ι × ι)
w₁ :
  Eq (α :=
    F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (F.map (Quiver.Hom.op (leSupr U j.as.1) ≫ Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
    (F.map (Quiver.Hom.op (leSupr U j.as.2) ≫ Quiver.Hom.op ((U j.as.1).infLERight (U j.as.2))))
⊢ Eq (α :=
    F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (F.map (Quiver.Hom.op (leSupr U j.as.1) ≫ Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
    (F.map (Quiver.Hom.op (leSupr U j.as.2)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLERight (U j.as.2))))

Tactic:
rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
j : Discrete (ι × ι)
⊢ Eq (α :=
    F.obj (op (iSup U)) ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (F.map (Quiver.Hom.op (leSupr U j.as.1) ≫ Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
    (F.map (Quiver.Hom.op (leSupr U j.as.2) ≫ Quiver.Hom.op ((U j.as.1).infLERight (U j.as.2))))

Tactic:
congr 1
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
⊢ Cone.pt (F := parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U)) (fork F U) = F.obj (op (iSup U))

Tactic:
rfl

Premises used: rfl