awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
zero :
  ∀ (j : Discrete ι),
    (𝟙 c.pt ≫ Fork.ι c) ≫ limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j =
      CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
        (Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i)))
        (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j)
⊢ 𝟙 c.pt ≫ Fork.ι c = Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i))

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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j : Discrete ι
⊢ (𝟙 c.pt ≫ Fork.ι c) ≫ limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
      (Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i)))
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j)

Tactic:
simp
-- 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
one :
  𝟙 c.pt ≫ c.π.app WalkingParallelPair.one =
    Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.2))
⊢ 𝟙
        (Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
          (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)) ≫
      (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).π.app WalkingParallelPair.one =
    NatTrans.app (Cone.π (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)) WalkingParallelPair.one

Tactic:
dsimp
-- 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
one :
  ∀ (j : Discrete (ι × ι)),
    (𝟙 c.pt ≫ c.π.app WalkingParallelPair.one) ≫
        limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j =
      CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.2)))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one =
    Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j : Discrete (ι × ι)
⊢ (𝟙 c.pt ≫ c.π.app WalkingParallelPair.one) ≫
      limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)

Tactic:
simp
-- 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
zero : (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i))) = Fork.ι c
⊢ 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt ≫
      NatTrans.app (Cone.π (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)) WalkingParallelPair.zero =
    (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).π.app WalkingParallelPair.zero

Tactic:
dsimp
-- 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
zero :
  ∀ (j : Discrete ι),
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
        (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i)))
        (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j) =
      Fork.ι c ≫ limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j
⊢ (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i))) = Fork.ι c

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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j : Discrete ι
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
      (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i)))
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j) =
    Fork.ι c ≫ limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j

Tactic:
simp
-- 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
one :
  (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.2))) =
    c.π.app WalkingParallelPair.one
⊢ 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt ≫
      NatTrans.app (Cone.π (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)) WalkingParallelPair.one =
    (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).π.app WalkingParallelPair.one

Tactic:
dsimp
-- 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
one :
  ∀ (j : Discrete (ι × ι)),
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.2)))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) =
      c.π.app WalkingParallelPair.one ≫ limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j
⊢ (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.2))) =
    c.π.app WalkingParallelPair.one

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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j : Discrete (ι × ι)
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) =
    c.π.app WalkingParallelPair.one ≫ limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j

Tactic:
simp
-- 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')
c d : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ d
w : f.hom ≫ 𝟙 d.pt = 𝟙 c.pt ≫ f.hom
⊢ Eq (α :=
    Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
        (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c) ⟶
      (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) d).pt)
    (ConeMorphism.hom
      (CategoryTheory.Functor.map (coneEquivInverse F U ⋙ coneEquivFunctor F U) f ≫
        Iso.hom
          ((fun (c : Cone (SheafConditionEqualizerProducts.diagram F U)) ↦
              {
                hom :=
                  {
                    hom :=
                      𝟙
                        (Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
                          (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)),
                    w := ⋯ },
                inv := { hom := 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt, w := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ :
                Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c ≅
                  Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c })
            d)))
    (ConeMorphism.hom
      (Iso.hom
          ((fun (c : Cone (SheafConditionEqualizerProducts.diagram F U)) ↦
              {
                hom :=
                  {
                    hom :=
                      𝟙
                        (Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
                          (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)),
                    w := ⋯ },
                inv := { hom := 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt, w := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ :
                Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c ≅
                  Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c })
            c) ≫
        CategoryTheory.Functor.map (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) f))

Tactic:
dsimp
-- 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')
c d : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ d
⊢ f.hom ≫ 𝟙 d.pt = 𝟙 c.pt ≫ f.hom

Tactic:
simp only [Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_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')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
x : CategoryTheory.Pairwise ι
⊢ Eq (α :=
    (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
          (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
          (SheafConditionEqualizerProducts.fork F U)).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (op x))
    (𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app (op x))
    ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).π.app
      (op x))

Tactic:
?_
-- 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')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
x : (CategoryTheory.Pairwise ι)ᵒᵖ
op :
  ∀ (x : CategoryTheory.Pairwise ι),
    Eq (α :=
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
      (𝟙
          (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).pt ≫
        (Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op x))
      ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (Opposite.op x))
⊢ 𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app x =
    (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).π.app
      x

Tactic:
induction x with | op x => ?_

Premises used: Opposite.op
-- 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')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
x : CategoryTheory.Pairwise ι
op :
  ∀ (a : ι),
    Eq (α :=
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a)))
      (𝟙
          (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).pt ≫
        (Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op (single a)))
      ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (Opposite.op (single a)))
op₁ :
  ∀ (a a_1 : ι),
    Eq (α :=
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
      (𝟙
          (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).pt ≫
        (Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op (Pairwise.pair a a_1)))
      ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (Opposite.op (Pairwise.pair a a_1)))
⊢ Eq (α :=
    (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
          (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
          (SheafConditionEqualizerProducts.fork F U)).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
    (𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op x))
    ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).π.app
      (Opposite.op x))

Tactic:
rcases x with ⟨⟩
-- 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')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a : ι
op : F.map (Quiver.Hom.op (coconeιApp U (single a))) = F.map (leSupr U a).op
⊢ Eq (α :=
    (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
          (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
          (SheafConditionEqualizerProducts.fork F U)).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a)))
    (𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op (single a)))
    ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).π.app
      (Opposite.op (single a)))

Tactic:
simp
-- 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')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a : ι
⊢ F.map (Quiver.Hom.op (coconeιApp U (single a))) = F.map (leSupr U a).op

Tactic:
rfl
-- 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')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a a_1 : ι
op :
  Eq (α := F.obj (Opposite.op (iSup U)) ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (𝟙 (F.obj (Opposite.op (iSup U))) ≫ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))) :
      F.obj (Opposite.op (iSup U)) ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
          (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
          (Pi.lift fun (p : ι × ι) ↦
            Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
        (Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (a, a_1)) :
      F.obj (Opposite.op (iSup U)) ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
⊢ Eq (α :=
    (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
          (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
          (SheafConditionEqualizerProducts.fork F U)).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
    (𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op (Pairwise.pair a a_1)))
    ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).π.app
      (Opposite.op (Pairwise.pair a a_1)))

Tactic:
dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                SheafConditionEqualizerProducts.leftRes]

Premises used: TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse, 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')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a a_1 : ι
op :
  Eq (α := F.obj (Opposite.op (iSup U)) ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))) :
      F.obj (Opposite.op (iSup U)) ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (F.map (leSupr U a).op ≫ F.map (Quiver.Hom.op ((U a).infLELeft (U a_1))) :
      Cone.pt.{v', v, v', u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ F.obj (Opposite.op (U i)))
          (Fan.mk (F.obj (Opposite.op (iSup U))) fun (i : ι) ↦ F.map (leSupr U i).op) ⟶
        F.obj (Opposite.op (U a ⊓ U a_1)))
⊢ Eq (α := F.obj (Opposite.op (iSup U)) ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (𝟙 (F.obj (Opposite.op (iSup U))) ≫ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))) :
      F.obj (Opposite.op (iSup U)) ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
          (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
          (Pi.lift fun (p : ι × ι) ↦
            Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
        (Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (a, a_1)) :
      F.obj (Opposite.op (iSup U)) ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app, CategoryTheory.Category.id_comp