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)
i j : ι
h :
  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 ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj 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))))
      (Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))

Tactic:
have h' := h =≫ Pi.π _ (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 j : ι
h :
  c.π.app WalkingParallelPair.one =
    Fork.ι c ≫
      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)))
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j) =
    CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
      (Fork.ι c ≫
        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))) (i, j))
op :
  Eq (α := c.pt ⟶ F.obj (Opposite.op (U i ⊓ U j)))
    (CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
        (Fork.ι c ≫
          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))) (i, j)) :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
        F.obj (Opposite.op (U (i, j).1 ⊓ U (i, j).2)))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i ≫ F.map (homOfLE ⋯).op :
      c.pt ⟶ F.obj (Opposite.op (U i ⊓ U j)))
⊢ 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:
rw [h']
-- 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.π.app WalkingParallelPair.one =
    Fork.ι c ≫
      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)))
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j) =
    CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
      (Fork.ι c ≫
        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))) (i, j))
op :
  Eq (α := c.pt ⟶ F.obj (Opposite.op (U i ⊓ U j)))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i ≫ F.map (Quiver.Hom.op ((U i).infLELeft (U j))))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i ≫ F.map (homOfLE ⋯).op)
⊢ Eq (α := c.pt ⟶ F.obj (Opposite.op (U i ⊓ U j)))
    (CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
        (Fork.ι c ≫
          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))) (i, j)) :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
        F.obj (Opposite.op (U (i, j).1 ⊓ U (i, j).2)))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i ≫ F.map (homOfLE ⋯).op :
      c.pt ⟶ F.obj (Opposite.op (U i ⊓ U j)))

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  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)))
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj 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))))
      (Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
⊢ Eq (α := c.pt ⟶ F.obj (op (U i ⊓ U j)))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (Quiver.Hom.op ((U i).infLELeft (U j))))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).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')
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))) (j, i) =
    (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 j i)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (Pairwise.pair j i)))
      (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Quiver.Hom.op (right j 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 (Pairwise.pair j 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 (right j 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 j : ι
op :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (j, i) =
    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))) (j, i) =
    (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.right ≫
      c.π.app WalkingParallelPair.one =
    c.π.app WalkingParallelPair.zero ≫ (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.right

Tactic:
have h := c.π.naturality WalkingParallelPairHom.right
-- 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.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))
⊢ c.π.app WalkingParallelPair.one =
    Fork.ι c ≫
      Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))

Tactic:
simp only [Category.id_comp] at h

Premises used: 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 : ι
h :
  c.π.app WalkingParallelPair.one =
    Fork.ι c ≫
      Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))
⊢ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
      (Fork.ι c ≫
        Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2))))
      (Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i))

Tactic:
have h' := h =≫ Pi.π _ (j, i)
-- 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.π.app WalkingParallelPair.one =
    Fork.ι c ≫
      Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (j, i) =
    CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
      (Fork.ι c ≫
        Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2))))
      (Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (j, i))
op :
  Eq (α := c.pt ⟶ F.obj (Opposite.op (U j ⊓ U i)))
    (CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
        (Fork.ι c ≫
          Pi.lift fun (p : ι × ι) ↦
            Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2))))
        (Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (j, i)) :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
        F.obj (Opposite.op (U (j, i).1 ⊓ U (j, i).2)))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i ≫ F.map (homOfLE ⋯).op :
      c.pt ⟶ F.obj (Opposite.op (U j ⊓ U i)))
⊢ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (j, i) =
    Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i ≫ F.map (homOfLE ⋯).op

Tactic:
rw [h']
-- 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.π.app WalkingParallelPair.one =
    Fork.ι c ≫
      Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (j, i) =
    CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
      (Fork.ι c ≫
        Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2))))
      (Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (j, i))
op :
  Eq (α := c.pt ⟶ F.obj (Opposite.op (U j ⊓ U i)))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i ≫ F.map (Quiver.Hom.op ((U j).infLERight (U i))))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i ≫ F.map (homOfLE ⋯).op)
⊢ Eq (α := c.pt ⟶ F.obj (Opposite.op (U j ⊓ U i)))
    (CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
        (Fork.ι c ≫
          Pi.lift fun (p : ι × ι) ↦
            Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2))))
        (Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (j, i)) :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
        F.obj (Opposite.op (U (j, i).1 ⊓ U (j, i).2)))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i ≫ F.map (homOfLE ⋯).op :
      c.pt ⟶ F.obj (Opposite.op (U j ⊓ 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 : ι
h :
  c.π.app WalkingParallelPair.one =
    Fork.ι c ≫
      Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
      (Fork.ι c ≫
        Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2))))
      (Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i))
⊢ Eq (α := c.pt ⟶ F.obj (op (U j ⊓ U i)))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (Quiver.Hom.op ((U j).infLERight (U i))))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a a_1 : ι
op :
  𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (a, a_1) =
    (c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (a, a_1)) ≫
      F.map (𝟙 (Opposite.op (U a ⊓ U a_1)))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (Pairwise.pair a a_1)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (Pairwise.pair a a_1)))
      (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Quiver.Hom.op (id_pair a a_1)))
      (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 a a_1))))
    (CategoryStruct.comp (Y := (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
      (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 a a_1)))
      ((Functor.op (diagram U) ⋙ F).map (Quiver.Hom.op (id_pair a a_1))))

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

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

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 (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
x : CategoryTheory.Pairwise ι
⊢ Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op x))
    (f.hom ≫ (coneEquivInverseObj F U c').π.app (op x)) ((coneEquivInverseObj F U c).π.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')
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
x : (CategoryTheory.Pairwise ι)ᵒᵖ
op :
  ∀ (x : CategoryTheory.Pairwise ι),
    Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
      (f.hom ≫ (coneEquivInverseObj F U c').π.app (Opposite.op x)) ((coneEquivInverseObj F U c).π.app (Opposite.op x))
⊢ f.hom ≫ (coneEquivInverseObj F U c').π.app x = (coneEquivInverseObj F U c).π.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')
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
x : CategoryTheory.Pairwise ι
op :
  ∀ (i : ι),
    Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single i)))
      (f.hom ≫ (coneEquivInverseObj F U c').π.app (Opposite.op (single i)))
      ((coneEquivInverseObj F U c).π.app (Opposite.op (single i)))
op₁ :
  ∀ (i j : ι),
    Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair i j)))
      (f.hom ≫ (coneEquivInverseObj F U c').π.app (Opposite.op (Pairwise.pair i j)))
      ((coneEquivInverseObj F U c).π.app (Opposite.op (Pairwise.pair i j)))
⊢ Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
    (f.hom ≫ (coneEquivInverseObj F U c').π.app (Opposite.op x)) ((coneEquivInverseObj F U c).π.app (Opposite.op x))

Tactic:
rcases x with (⟨i⟩ | ⟨i, j⟩)