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 (Functor.op (diagram U) ⋙ F)
f : WalkingParallelPair.one ⟶ WalkingParallelPair.zero
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.zero)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) f ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.zero (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map f)

Tactic:
cases f
-- 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 (Functor.op (diagram U) ⋙ F)
f : WalkingParallelPair.one ⟶ WalkingParallelPair.one
one :
  Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt)
        (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) f ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map f)

Tactic:
cases f
-- 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 (Functor.op (diagram U) ⋙ F)
zero :
  (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) =
    (Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.zero)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.zero)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt)
        (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.zero (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.zero (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id 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 (Functor.op (diagram U) ⋙ F)
zero :
  ∀ (j : Discrete ι),
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
        (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j) =
      ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫
          (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.zero)) ≫
        limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j
⊢ (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) =
    (Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.zero)

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 (Functor.op (diagram U) ⋙ F)
j : Discrete ι
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
      (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j) =
    ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫
        (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.zero)) ≫
      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 (Functor.op (diagram U) ⋙ F)
zero :
  Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)) :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPairHom.left ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.zero (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.left)

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 (Functor.op (diagram U) ⋙ F)
zero :
  ∀ (ij : Discrete (ι × ι)),
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij) =
      CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U)
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij)
⊢ Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)) :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)

Tactic:
ext ij
-- 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 (Functor.op (diagram U) ⋙ F)
ij : Discrete (ι × ι)
zero :
  ∀ (i j : ι),
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) }) =
      CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U)
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) : Discrete (ι × ι) })
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij)

Tactic:
rcases ij with ⟨i, j⟩
-- 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 (Functor.op (diagram U) ⋙ F)
i j : ι
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) }) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) : Discrete (ι × ι) })

Tactic:
simpa [SheafConditionEqualizerProducts.leftRes]
            using c.π.naturality (Quiver.Hom.op (Hom.left i j))

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Pairwise.Hom.left, Quiver.Hom.op, CategoryTheory.NatTrans.naturality, TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes
-- 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 (Functor.op (diagram U) ⋙ F)
zero :
  Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)) :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPairHom.right ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.zero (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.right)

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 (Functor.op (diagram U) ⋙ F)
zero :
  ∀ (ij : Discrete (ι × ι)),
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij) =
      CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U)
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij)
⊢ Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)) :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)

Tactic:
ext ij
-- 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 (Functor.op (diagram U) ⋙ F)
ij : Discrete (ι × ι)
zero :
  ∀ (i j : ι),
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) }) =
      CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U)
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) : Discrete (ι × ι) })
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij)

Tactic:
rcases ij with ⟨i, j⟩
-- 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 (Functor.op (diagram U) ⋙ F)
i j : ι
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) }) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) : Discrete (ι × ι) })

Tactic:
simpa [SheafConditionEqualizerProducts.rightRes]
            using c.π.naturality (Quiver.Hom.op (Hom.right i j))

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Pairwise.Hom.right, Quiver.Hom.op, CategoryTheory.NatTrans.naturality, TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes
-- 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 (Functor.op (diagram U) ⋙ F)
one :
  (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.one)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt)
        (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id 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 (Functor.op (diagram U) ⋙ F)
one :
  ∀ (j : Discrete (ι × ι)),
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) =
      ((Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
          (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.one)) ≫
        limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j
⊢ (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (𝟙 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 (Functor.op (diagram U) ⋙ F)
j : Discrete (ι × ι)
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) =
    ((Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
        (SheafConditionEqualizerProducts.diagram F U).map (𝟙 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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
j : WalkingParallelPair
zero :
  Eq (α :=
    Cone.pt (F := SheafConditionEqualizerProducts.diagram F U) (coneEquivFunctorObj F U c) ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.zero)
    (f.hom ≫ NatTrans.app (Cone.π (coneEquivFunctorObj F U c')) WalkingParallelPair.zero)
    (NatTrans.app (Cone.π (coneEquivFunctorObj F U c)) WalkingParallelPair.zero)
one :
  Eq (α :=
    Cone.pt (F := SheafConditionEqualizerProducts.diagram F U) (coneEquivFunctorObj F U c) ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (f.hom ≫ NatTrans.app (Cone.π (coneEquivFunctorObj F U c')) WalkingParallelPair.one)
    (NatTrans.app (Cone.π (coneEquivFunctorObj F U c)) WalkingParallelPair.one)
⊢ Eq (α :=
    Cone.pt (F := SheafConditionEqualizerProducts.diagram F U) (coneEquivFunctorObj F U c) ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj j)
    (f.hom ≫ NatTrans.app (Cone.π (coneEquivFunctorObj F U c')) j) (NatTrans.app (Cone.π (coneEquivFunctorObj F U c)) j)

Tactic:
cases j
-- 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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
zero :
  Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piOpens F U) (f.hom ≫ Pi.lift fun (i : ι) ↦ c'.π.app (op (single i)))
    (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
⊢ Eq (α :=
    Cone.pt (F := SheafConditionEqualizerProducts.diagram F U) (coneEquivFunctorObj F U c) ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.zero)
    (f.hom ≫ NatTrans.app (Cone.π (coneEquivFunctorObj F U c')) WalkingParallelPair.zero)
    (NatTrans.app (Cone.π (coneEquivFunctorObj F U c)) WalkingParallelPair.zero)

Tactic:
dsimp