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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
zero :
  ∀ (j : Discrete ι),
    Eq (α := c.pt ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j)
      (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
        (f.hom ≫ Pi.lift fun (i : ι) ↦ c'.π.app (op (single i)))
        (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j))
      (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
        (Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j))
⊢ 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)))

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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
j : Discrete ι
⊢ Eq (α := c.pt ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j)
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
      (f.hom ≫ Pi.lift fun (i : ι) ↦ c'.π.app (op (single i)))
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
      (Pi.lift fun (i : ι) ↦ 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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
one :
  Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    (f.hom ≫ 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)))
⊢ 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)

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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
one :
  ∀ (j : Discrete (ι × ι)),
    Eq (α := c.pt ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
      (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (f.hom ≫ 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))
      (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (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))
⊢ Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    (f.hom ≫ 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)))

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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
j : Discrete (ι × ι)
⊢ Eq (α := c.pt ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (f.hom ≫ 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))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (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))

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)
x : (CategoryTheory.Pairwise ι)ᵒᵖ
op :
  (x : CategoryTheory.Pairwise ι) →
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (Opposite.op x) ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op x)
⊢ Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
    (Functor.op (diagram U) ⋙ F).obj 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x : CategoryTheory.Pairwise ι
op :
  (i : ι) →
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (single i)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single i))
op₁ :
  (i j : ι) →
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (Pairwise.pair i j)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair i j))
⊢ Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (Opposite.op x) ⟶
    (Functor.op (diagram U) ⋙ F).obj (Opposite.op x)

Tactic:
rcases x with (⟨i⟩ | ⟨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 (SheafConditionEqualizerProducts.diagram F U)
i : ι
⊢ Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op (single i)) ⟶
    (Functor.op (diagram U) ⋙ F).obj (op (single i))

Tactic:
exact c.π.app WalkingParallelPair.zero ≫ Pi.π _ i

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.Pi.π, CategoryTheory.NatTrans.app, CategoryTheory.Limits.WalkingParallelPair.zero
-- 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)
i j : ι
⊢ Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op (Pairwise.pair i j)) ⟶
    (Functor.op (diagram U) ⋙ F).obj (op (Pairwise.pair i j))

Tactic:
exact c.π.app WalkingParallelPair.one ≫ Pi.π _ (i, j)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.Pi.π, Prod.mk, CategoryTheory.NatTrans.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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
y : (CategoryTheory.Pairwise ι)ᵒᵖ
x : CategoryTheory.Pairwise ι
f : op x ⟶ y
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
      (Functor.op (diagram U) ⋙ F).obj y)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) f ≫
      Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        y)
    (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op x) ≫
      (Functor.op (diagram U) ⋙ F).map f)

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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
      (Functor.op (diagram U) ⋙ F).obj (op y))
    (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) f ≫
      Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op y))
    (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op x) ≫
      (Functor.op (diagram U) ⋙ F).map f)

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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
⊢ f = f.unop.op

Tactic:
have ef : f = f.unop.op := 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a a_1 a_2 : ι
f' : unop (op (single a_2)) ⟶ unop (op (Pairwise.pair a a_1))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (op (Pairwise.pair a a_1)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (op (single a_2)))
    (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) f'.op ≫
      Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (single a_2)))
    (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (Pairwise.pair a a_1)) ≫
      (Functor.op (diagram U) ⋙ F).map f'.op)

Tactic:
rcases f' 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i : ι
op :
  𝟙 c.pt ≫ Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i =
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i) ≫ F.map (𝟙 (Opposite.op (U i)))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (single i)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single i)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (single i)))
      (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Quiver.Hom.op (id_single i)))
      (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
                (Opposite.op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i)
            fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j))
        (Opposite.op (single i))))
    (CategoryStruct.comp (Y := (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single i)))
      (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
                (Opposite.op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i)
            fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j))
        (Opposite.op (single i)))
      ((Functor.op (diagram U) ⋙ F).map (Quiver.Hom.op (id_single i))))

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)
i : ι
op :
  𝟙 c.pt ≫ Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i =
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i) ≫ 𝟙 (F.obj (Opposite.op (U i)))
⊢ 𝟙 c.pt ≫ Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i =
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i) ≫ F.map (𝟙 (Opposite.op (U i)))

Tactic:
rw [F.map_id]

Premises used: CategoryTheory.Functor.map_id
-- 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)
i : ι
⊢ 𝟙 c.pt ≫ Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i =
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) ≫ 𝟙 (F.obj (op (U i)))

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)
i j : ι
op :
  𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j) =
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i) ≫ F.map (homOfLE ⋯).op
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (single i)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair i j)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (Pairwise.pair i j)))
      (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Quiver.Hom.op (left i j)))
      (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
                (Opposite.op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i)
            fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j))
        (Opposite.op (Pairwise.pair i j))))
    (CategoryStruct.comp (Y := (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single i)))
      (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
                (Opposite.op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i)
            fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j))
        (Opposite.op (single i)))
      ((Functor.op (diagram U) ⋙ F).map (Quiver.Hom.op (left i j))))

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)
i j : ι
op :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j) =
    Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i ≫ F.map (homOfLE ⋯).op
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j) =
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i) ≫ F.map (homOfLE ⋯).op

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

Premises used: CategoryTheory.Category.assoc, 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPairHom.left ≫
      c.π.app WalkingParallelPair.one =
    c.π.app WalkingParallelPair.zero ≫ (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.left

Tactic:
have h := c.π.naturality WalkingParallelPairHom.left
-- 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)
i j : ι
h :
  𝟙 c.pt ≫ c.π.app WalkingParallelPair.one =
    Fork.ι c ≫
      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)))
⊢ c.π.app WalkingParallelPair.one =
    Fork.ι c ≫
      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)))

Tactic:
simp only [Category.id_comp] at h

Premises used: CategoryTheory.Category.id_comp