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')
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 ≫ Quiver.Hom.op ((U a).infLELeft (U a_1))) :
      F.obj (Opposite.op (iSup U)) ⟶ 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.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)))

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')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a a_1 : ι
⊢ Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))) : F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
    (F.map ((leSupr U a).op ≫ Quiver.Hom.op ((U a).infLELeft (U a_1))) : F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))

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)
x : CategoryTheory.Pairwise ι
⊢ Eq (α := (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op x))
    (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (op x))
    ((Functor.mapCone F (Cocone.op (cocone 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.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
      (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
        (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.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op x))
⊢ 𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        x =
    (Functor.mapCone F (Cocone.op (cocone 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.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a)))
      (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
        (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)))
      ((Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op (single a)))
op₁ :
  ∀ (a a_1 : ι),
    Eq (α :=
      (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
      (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
        (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)))
      ((Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op (Pairwise.pair a a_1)))
⊢ Eq (α := (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
    (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (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.mapCone F (Cocone.op (cocone 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 (leSupr U a).op = F.map (Quiver.Hom.op (coconeιApp U (single a)))
⊢ Eq (α := (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a)))
    (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (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)))
    ((Functor.mapCone F (Cocone.op (cocone 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 (leSupr U a).op = F.map (Quiver.Hom.op (coconeιApp U (single a)))

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.{v + 1} (α := F.obj (Opposite.op (iSup U)) ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (𝟙 (F.obj (Opposite.op (iSup U))) ≫
        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)))
    (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)))
⊢ Eq (α :=
    (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
    (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (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)))
    ((Functor.mapCone F (Cocone.op (cocone 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 (leSupr U a).op ≫ F.map (Quiver.Hom.op ((U a).infLELeft (U a_1))))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))))
⊢ Eq.{v + 1} (α := F.obj (Opposite.op (iSup U)) ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (𝟙 (F.obj (Opposite.op (iSup U))) ≫
        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)))
    (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)))

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
-- 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 ((leSupr U a).op ≫ Quiver.Hom.op ((U a).infLELeft (U a_1))))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))))
⊢ Eq (α := 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))))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))))

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')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a a_1 : ι
⊢ Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
    (F.map ((leSupr U a).op ≫ Quiver.Hom.op ((U a).infLELeft (U a_1))))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))))

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')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
zero :
  Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.res F U)
    (Pi.lift fun (i : ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (single i))))
⊢ Eq.{v + 1} (α :=
    Cone.pt (F :=
        parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
          (SheafConditionEqualizerProducts.rightRes F U))
        (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U)))) ⟶
      (parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U)).obj
        WalkingParallelPair.zero)
    (𝟙
        (Cone.pt (F :=
          parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U))
          (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U))))) ≫
      NatTrans.app (Cone.π (SheafConditionEqualizerProducts.fork F U)) WalkingParallelPair.zero)
    (NatTrans.app
      (Cone.π (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U)))))
      WalkingParallelPair.zero)

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')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
⊢ Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.res F U)
    (Pi.lift fun (i : ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (single i))))

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')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
one :
  Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piInters F U)
    (𝟙 (F.obj (op (iSup U))) ≫ SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U)
    (Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
⊢ Eq.{v + 1} (α :=
    Cone.pt (F :=
        parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
          (SheafConditionEqualizerProducts.rightRes F U))
        (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U)))) ⟶
      (parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U)).obj
        WalkingParallelPair.one)
    (𝟙
        (Cone.pt (F :=
          parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U))
          (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U))))) ≫
      NatTrans.app (Cone.π (SheafConditionEqualizerProducts.fork F U)) WalkingParallelPair.one)
    (NatTrans.app
      (Cone.π (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U)))))
      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')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
one :
  ∀ (j : Discrete (ι × ι)),
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 (F.obj (op (iSup U))) ≫
          SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U)
        (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 : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
⊢ Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piInters F U)
    (𝟙 (F.obj (op (iSup U))) ≫ SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U)
    (Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (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')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
j : Discrete (ι × ι)
one :
  Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 (F.obj (op (iSup 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 (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) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 (F.obj (op (iSup U))) ≫ SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U)
      (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 : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)

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')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
j : Discrete (ι × ι)
one :
  Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (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 (coconeιApp U (Pairwise.pair j.as.1 j.as.2))))
⊢ Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 (F.obj (op (iSup 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 (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) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))

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
-- 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')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
j : Discrete (ι × ι)
one :
  Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (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 (coconeιApp U (Pairwise.pair j.as.1 j.as.2))))
⊢ Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (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 (coconeιApp U (Pairwise.pair j.as.1 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')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
j : Discrete (ι × ι)
⊢ Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (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 (coconeιApp U (Pairwise.pair j.as.1 j.as.2))))

Tactic:
rfl