awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a a_1 : ι
⊢ Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
    (𝟙 (F.obj (op (iSup U))) ≫ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
          (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
          (Pi.lift fun (p : ι × ι) ↦
            Pi.π (fun (i : ι) ↦ F.obj (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))) (a, a_1)) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
have op : Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
  (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))) : F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
  (F.map (leSupr U a).op ≫ F.map (Quiver.Hom.op ((U a).infLELeft (U a_1))) :
    Cone.pt.{v', v, v', u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ F.obj (op (U i)))
        (Fan.mk (F.obj (op (iSup U))) fun (i : ι) ↦ F.map (leSupr U i).op) ⟶
      F.obj (op (U a ⊓ U a_1)))
Tactic: simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
                Category.assoc]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a a_1 : ι
⊢ Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))) : F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
    (F.map (leSupr U a).op ≫ F.map (Quiver.Hom.op ((U a).infLELeft (U a_1))) :
      Cone.pt.{v', v, v', u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ F.obj (op (U i)))
          (Fan.mk (F.obj (op (iSup U))) fun (i : ι) ↦ F.map (leSupr U i).op) ⟶
        F.obj (op (U a ⊓ U a_1)))
have op : Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
  (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))) : F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
  (F.map ((leSupr U a).op ≫ Quiver.Hom.op ((U a).infLELeft (U a_1))) : F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
Tactic: rw [← F.map_comp]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
x : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ 𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        x =
    (Functor.mapCone F (Cocone.op (cocone U))).π.app x
have op : ∀ (x : CategoryTheory.Pairwise ι),
  Eq (α := (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op x))
    (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (op x))
    ((Functor.mapCone F (Cocone.op (cocone U))).π.app (op x))
Tactic: induction x with | op x => ?_
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
x : CategoryTheory.Pairwise ι
⊢ Eq (α := (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op x))
    (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (op x))
    ((Functor.mapCone F (Cocone.op (cocone U))).π.app (op x))
have op : ∀ (a : ι),
  Eq (α := (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op (single a)))
    (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (op (single a)))
    ((Functor.mapCone F (Cocone.op (cocone U))).π.app (op (single a)))
Tactic: rcases x with ⟨⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
x : CategoryTheory.Pairwise ι
op :
  ∀ (a : ι),
    Eq (α := (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a)))
      (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
                (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
                (SheafConditionEqualizerProducts.fork F U)).π.app
          (Opposite.op (single a)))
      ((Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op (single a)))
⊢ Eq (α := (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
    (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (Opposite.op x))
    ((Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op x))
have op₁ : ∀ (a a_1 : ι),
  Eq (α :=
    (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
    (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (Opposite.op (Pairwise.pair a a_1)))
    ((Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op (Pairwise.pair a a_1)))
Tactic: rcases x with ⟨⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a : ι
⊢ Eq (α := (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op (single a)))
    (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (op (single a)))
    ((Functor.mapCone F (Cocone.op (cocone U))).π.app (op (single a)))
have op : F.map (leSupr U a).op = F.map (Quiver.Hom.op (coconeιApp U (single a)))
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a a_1 : ι
⊢ Eq (α := (Functor.mapCone F (Cocone.op (cocone U))).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op (Pairwise.pair a a_1)))
    (𝟙 (Functor.mapCone F (Cocone.op (cocone U))).pt ≫
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (op (Pairwise.pair a a_1)))
    ((Functor.mapCone F (Cocone.op (cocone U))).π.app (op (Pairwise.pair a a_1)))
have op : Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
  (𝟙 (F.obj (op (iSup U))) ≫
      CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
          (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
          (Pi.lift fun (p : ι × ι) ↦
            Pi.π (fun (i : ι) ↦ F.obj (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))) (a, a_1)) :
    F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
  (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))) : F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
Tactic: dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                SheafConditionEqualizerProducts.leftRes]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a a_1 : ι
⊢ Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
    (𝟙 (F.obj (op (iSup U))) ≫
        CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
          (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
            (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
            (Pi.lift fun (p : ι × ι) ↦
              Pi.π (fun (i : ι) ↦ F.obj (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))) (a, a_1)) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))) : F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
have op : Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
  (F.map (leSupr U a).op ≫ F.map (Quiver.Hom.op ((U a).infLELeft (U a_1))))
  (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))))
Tactic: simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
                Category.assoc]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
a a_1 : ι
⊢ Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
    (F.map (leSupr U a).op ≫ F.map (Quiver.Hom.op ((U a).infLELeft (U a_1))))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))))
have op : Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U a ⊓ U a_1)))
  (F.map ((leSupr U a).op ≫ Quiver.Hom.op ((U a).infLELeft (U a_1))))
  (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair a a_1))))
Tactic: rw [← F.map_comp]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
⊢ Eq.{v + 1} (α :=
    Cone.pt (F :=
        parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
          (SheafConditionEqualizerProducts.rightRes F U))
        (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U)))) ⟶
      (parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U)).obj
        WalkingParallelPair.zero)
    (𝟙
        (Cone.pt (F :=
          parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U))
          (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U))))) ≫
      NatTrans.app (Cone.π (SheafConditionEqualizerProducts.fork F U)) WalkingParallelPair.zero)
    (NatTrans.app
      (Cone.π (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U)))))
      WalkingParallelPair.zero)
have zero : Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.res F U)
  (Pi.lift fun (i : ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (single i))))
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
⊢ Eq.{v + 1} (α :=
    Cone.pt (F :=
        parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
          (SheafConditionEqualizerProducts.rightRes F U))
        (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U)))) ⟶
      (parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U)).obj
        WalkingParallelPair.one)
    (𝟙
        (Cone.pt (F :=
          parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U))
          (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U))))) ≫
      NatTrans.app (Cone.π (SheafConditionEqualizerProducts.fork F U)) WalkingParallelPair.one)
    (NatTrans.app
      (Cone.π (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U)))))
      WalkingParallelPair.one)
have one : Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piInters F U)
  (𝟙 (F.obj (op (iSup U))) ≫ SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U)
  (Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
⊢ Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piInters F U)
    (𝟙 (F.obj (op (iSup U))) ≫ SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U)
    (Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
have one : ∀ (j : Discrete (ι × ι)),
  CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 (F.obj (op (iSup U))) ≫ SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
j : Discrete (ι × ι)
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 (F.obj (op (iSup U))) ≫ SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
have one : Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
  (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 (F.obj (op (iSup U))) ≫
        CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
          (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
          (Pi.lift fun (p : ι × ι) ↦
            Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) :
    F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
  (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) :
    F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
Tactic: dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                SheafConditionEqualizerProducts.leftRes]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
j : Discrete (ι × ι)
⊢ Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 (F.obj (op (iSup U))) ≫
          CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
            (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
            (Pi.lift fun (p : ι × ι) ↦
              Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
have one : Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
  (F.map (Quiver.Hom.op (leSupr U j.as.1)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
  (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair j.as.1 j.as.2))))
Tactic: simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
                Category.assoc]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
j : Discrete (ι × ι)
⊢ Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (F.map (Quiver.Hom.op (leSupr U j.as.1)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair j.as.1 j.as.2))))
have one : Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
  (F.map (Quiver.Hom.op (leSupr U j.as.1) ≫ Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))))
  (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair j.as.1 j.as.2))))
Tactic: rw [← F.map_comp]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
⊢ Eq.{v + 1} (α :=
    Cone.pt (F :=
        parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
          (SheafConditionEqualizerProducts.rightRes F U))
        (SheafConditionEqualizerProducts.fork F U) ⟶
      (parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U)).obj
        WalkingParallelPair.zero)
    (𝟙
        (Cone.pt (F :=
          parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U))
          (SheafConditionEqualizerProducts.fork F U)) ≫
      NatTrans.app
        (Cone.π (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U)))))
        WalkingParallelPair.zero)
    (NatTrans.app (Cone.π (SheafConditionEqualizerProducts.fork F U)) WalkingParallelPair.zero)
have zero : Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piOpens F U)
  (Pi.lift fun (i : ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (single i))) :
    F.obj (op (iSup U)) ⟶ piObj.{v', v, u} fun (i : ι) ↦ F.obj (op (U i)))
  (SheafConditionEqualizerProducts.res F U : F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piOpens F U)
Tactic: simp