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 (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i : ι
op :
  f.hom ≫ Fork.ι c' ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i =
    Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) 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)))

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 (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i : ι
op :
  f.hom ≫ c'.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i =
    c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i
⊢ f.hom ≫ Fork.ι c' ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i =
    Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i

Tactic:
dsimp only [Fork.ι]

Premises used: CategoryTheory.Limits.Fork.ι
-- 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'
i : ι
op :
  f.hom ≫ c'.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i =
    (f.hom ≫ c'.π.app WalkingParallelPair.zero) ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i
op₁ op₂ :
  f.hom ≫ c'.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i =
    f.hom ≫ c'.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i
⊢ f.hom ≫ c'.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i =
    c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i

Tactic:
rw [← f.w WalkingParallelPair.zero, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.ConeMorphism.w, 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 c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i j : ι
op :
  f.hom ≫ c'.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j) =
    c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (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)))

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 (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i j : ι
op :
  f.hom ≫ c'.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j) =
    (f.hom ≫ c'.π.app WalkingParallelPair.one) ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j)
op₁ op₂ :
  f.hom ≫ c'.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j) =
    f.hom ≫ c'.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j)
⊢ f.hom ≫ c'.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j) =
    c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j)

Tactic:
rw [← f.w WalkingParallelPair.one, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.ConeMorphism.w, CategoryTheory.Limits.WalkingParallelPair.one
-- 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 : CategoryTheory.Pairwise ι
⊢ Eq (α := (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op j))
    (𝟙 (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ≫
      ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                  (coneEquivInverse F U)).obj
              c).π.app
        (op j))
    ((Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (op j))

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 (Functor.op (diagram U) ⋙ F)
j : (CategoryTheory.Pairwise ι)ᵒᵖ
op :
  ∀ (j : CategoryTheory.Pairwise ι),
    Eq (α :=
      (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op j))
      (𝟙 (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ≫
        ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                    (coneEquivInverse F U)).obj
                c).π.app
          (Opposite.op j))
      ((Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op j))
⊢ 𝟙 (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ≫
      ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                  (coneEquivInverse F U)).obj
              c).π.app
        j =
    (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app j

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

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 (Functor.op (diagram U) ⋙ F)
j : CategoryTheory.Pairwise ι
op :
  ∀ (a : ι),
    Eq (α :=
      (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a)))
      (𝟙 (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ≫
        ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                    (coneEquivInverse F U)).obj
                c).π.app
          (Opposite.op (single a)))
      ((Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op (single a)))
op₁ :
  ∀ (a a_1 : ι),
    Eq (α :=
      (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
      (𝟙 (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ≫
        ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                    (coneEquivInverse F U)).obj
                c).π.app
          (Opposite.op (Pairwise.pair a a_1)))
      ((Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op (Pairwise.pair a a_1)))
⊢ Eq (α :=
    (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op j))
    (𝟙 (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ≫
      ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                  (coneEquivInverse F U)).obj
              c).π.app
        (Opposite.op j))
    ((Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op j))

Tactic:
rcases j 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 (Functor.op (diagram U) ⋙ F)
a : ι
op :
  Eq.{v + 1} (α := c.pt ⟶ F.obj (Opposite.op (U a)))
    (𝟙 c.pt ≫
        CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
          (Pi.lift fun (i : ι) ↦ c.π.app (Opposite.op (single i))) (Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) a) :
      c.pt ⟶ F.obj (Opposite.op (U a)))
    (c.π.app (Opposite.op (single a)) :
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
          (Opposite.op (single a)) ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a)))
⊢ Eq (α :=
    (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a)))
    (𝟙 (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ≫
      ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                  (coneEquivInverse F U)).obj
              c).π.app
        (Opposite.op (single a)))
    ((Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op (single a)))

Tactic:
dsimp [coneEquivInverse]

Premises used: TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse
-- 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)
a : ι
⊢ Eq.{v + 1} (α := c.pt ⟶ F.obj (op (U a)))
    (𝟙 c.pt ≫
        CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
          (Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) (Pi.π (fun (i : ι) ↦ F.obj (op (U i))) a) :
      c.pt ⟶ F.obj (op (U a)))
    (c.π.app (op (single a)) :
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op (single a)) ⟶
        (Functor.op (diagram U) ⋙ F).obj (op (single a)))

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

Premises used: 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')
c : Cone (Functor.op (diagram U) ⋙ F)
a a_1 : ι
op :
  Eq.{v + 1} (α := c.pt ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (𝟙 c.pt ≫
        CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
          (Pi.lift fun (b : ι × ι) ↦ c.π.app (Opposite.op (Pairwise.pair b.1 b.2)))
          (Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (a, a_1)) :
      c.pt ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (c.π.app (Opposite.op (Pairwise.pair a a_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)))
⊢ Eq (α :=
    (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
    (𝟙 (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ≫
      ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                  (coneEquivInverse F U)).obj
              c).π.app
        (Opposite.op (Pairwise.pair a a_1)))
    ((Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op (Pairwise.pair a a_1)))

Tactic:
dsimp [coneEquivInverse]

Premises used: TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse
-- 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)
a a_1 : ι
⊢ Eq.{v + 1} (α := c.pt ⟶ F.obj (op (U a ⊓ U a_1)))
    (𝟙 c.pt ≫
        CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
          (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
          (Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (a, a_1)) :
      c.pt ⟶ F.obj (op (U a ⊓ U a_1)))
    (c.π.app (op (Pairwise.pair a a_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 (Pairwise.pair a a_1)))

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

Premises used: 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')
c : Cone (Functor.op (diagram U) ⋙ F)
j : CategoryTheory.Pairwise ι
⊢ Eq (α :=
    ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
              (coneEquivInverse F U)).obj
          c).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (op j))
    (𝟙
        ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).pt ≫
      (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (op j))
    (((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).π.app
      (op j))

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 (Functor.op (diagram U) ⋙ F)
j : (CategoryTheory.Pairwise ι)ᵒᵖ
op :
  ∀ (j : CategoryTheory.Pairwise ι),
    Eq (α :=
      ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).pt ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op j))
      (𝟙
          ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                  (coneEquivInverse F U)).obj
              c).pt ≫
        (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op j))
      (((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                  (coneEquivInverse F U)).obj
              c).π.app
        (Opposite.op j))
⊢ 𝟙
        ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).pt ≫
      (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app j =
    ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).π.app
      j

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

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 (Functor.op (diagram U) ⋙ F)
j : CategoryTheory.Pairwise ι
op :
  ∀ (a : ι),
    Eq (α :=
      ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).pt ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a)))
      (𝟙
          ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                  (coneEquivInverse F U)).obj
              c).pt ≫
        (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op (single a)))
      (((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                  (coneEquivInverse F U)).obj
              c).π.app
        (Opposite.op (single a)))
op₁ :
  ∀ (a a_1 : ι),
    Eq (α :=
      ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).pt ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
      (𝟙
          ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                  (coneEquivInverse F U)).obj
              c).pt ≫
        (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op (Pairwise.pair a a_1)))
      (((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                  (coneEquivInverse F U)).obj
              c).π.app
        (Opposite.op (Pairwise.pair a a_1)))
⊢ Eq (α :=
    ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
              (coneEquivInverse F U)).obj
          c).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op j))
    (𝟙
        ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).pt ≫
      (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op j))
    (((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).π.app
      (Opposite.op j))

Tactic:
rcases j 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 (Functor.op (diagram U) ⋙ F)
a : ι
op :
  Eq (α := c.pt ⟶ F.obj (Opposite.op (U a)))
    (𝟙 c.pt ≫ c.π.app (Opposite.op (single a)) : c.pt ⟶ F.obj (Opposite.op (U a)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
        (Pi.lift fun (i : ι) ↦ c.π.app (Opposite.op (single i))) (Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) a) :
      c.pt ⟶ F.obj (Opposite.op (U a)))
⊢ Eq (α :=
    ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
              (coneEquivInverse F U)).obj
          c).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a)))
    (𝟙
        ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).pt ≫
      (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op (single a)))
    (((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).π.app
      (Opposite.op (single a)))

Tactic:
dsimp [coneEquivInverse]

Premises used: TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse
-- 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)
a : ι
⊢ Eq (α := c.pt ⟶ F.obj (op (U a))) (𝟙 c.pt ≫ c.π.app (op (single a)) : c.pt ⟶ F.obj (op (U a)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
        (Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) (Pi.π (fun (i : ι) ↦ F.obj (op (U i))) a) :
      c.pt ⟶ F.obj (op (U a)))

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

Premises used: 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')
c : Cone (Functor.op (diagram U) ⋙ F)
a a_1 : ι
op :
  Eq (α := c.pt ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (𝟙 c.pt ≫ c.π.app (Opposite.op (Pairwise.pair a a_1)) : c.pt ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (Opposite.op (Pairwise.pair b.1 b.2)))
        (Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (a, a_1)) :
      c.pt ⟶ F.obj (Opposite.op (U a ⊓ U a_1)))
⊢ Eq (α :=
    ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
              (coneEquivInverse F U)).obj
          c).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
    (𝟙
        ((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).pt ≫
      (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (Opposite.op (Pairwise.pair a a_1)))
    (((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).π.app
      (Opposite.op (Pairwise.pair a a_1)))

Tactic:
dsimp [coneEquivInverse]

Premises used: TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse
-- 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)
a a_1 : ι
⊢ Eq (α := c.pt ⟶ F.obj (op (U a ⊓ U a_1)))
    (𝟙 c.pt ≫ c.π.app (op (Pairwise.pair a a_1)) : c.pt ⟶ F.obj (op (U a ⊓ U a_1)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
        (Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (a, a_1)) :
      c.pt ⟶ F.obj (op (U a ⊓ U a_1)))

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

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

Tactic:
dsimp