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')
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))
have 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 (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 (op (single a)))
    (((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).π.app
      (op (single a)))
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- 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')
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)))
⊢ 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))
have 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)))
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- 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')
c : Cone (Functor.op (diagram U) ⋙ F)
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 (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 (op (single a)))
    (((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).π.app
      (op (single a)))
have op : 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: dsimp [coneEquivInverse]
-- 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')
c : Cone (Functor.op (diagram U) ⋙ F)
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 (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 (op (Pairwise.pair a a_1)))
    (((Functor.comp (D := Cone (SheafConditionEqualizerProducts.diagram F U)) (coneEquivFunctor F U)
                (coneEquivInverse F U)).obj
            c).π.app
      (op (Pairwise.pair a a_1)))
have op : 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: dsimp [coneEquivInverse]
-- 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙
        (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
have zero : 𝟙 c.pt ≫ Fork.ι c = Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i))
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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 c.pt ≫ Fork.ι c = Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i))
have zero : ∀ (j : Discrete ι),
  (𝟙 c.pt ≫ Fork.ι c) ≫ limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
      (Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i)))
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙
        (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.one =
    NatTrans.app (Cone.π (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)) WalkingParallelPair.one
have one : 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one =
  Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one =
    Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.2))
have one : ∀ (j : Discrete (ι × ι)),
  (𝟙 c.pt ≫ c.π.app WalkingParallelPair.one) ≫
      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 : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) 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: 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt ≫
      NatTrans.app (Cone.π (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)) WalkingParallelPair.zero =
    (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).π.app WalkingParallelPair.zero
have zero : (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i))) = Fork.ι c
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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i))) = Fork.ι c
have zero : ∀ (j : Discrete ι),
  CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
      (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (single i)))
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j) =
    Fork.ι c ≫ limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) 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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt ≫
      NatTrans.app (Cone.π (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)) WalkingParallelPair.one =
    (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).π.app WalkingParallelPair.one
have one : (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.2))) =
  c.π.app WalkingParallelPair.one
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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.2))) =
    c.π.app WalkingParallelPair.one
have one : ∀ (j : Discrete (ι × ι)),
  CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ (Functor.obj (coneEquivInverse F U) c).π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) =
    c.π.app WalkingParallelPair.one ≫ 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')
c d : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ d
⊢ Eq (α :=
    Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
        (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c) ⟶
      (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) d).pt)
    (ConeMorphism.hom
      (CategoryTheory.Functor.map (coneEquivInverse F U ⋙ coneEquivFunctor F U) f ≫
        Iso.hom
          ((fun (c : Cone (SheafConditionEqualizerProducts.diagram F U)) ↦
              {
                hom :=
                  {
                    hom :=
                      𝟙
                        (Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
                          (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)),
                    w := ⋯ },
                inv := { hom := 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt, w := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ :
                Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c ≅
                  Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c })
            d)))
    (ConeMorphism.hom
      (Iso.hom
          ((fun (c : Cone (SheafConditionEqualizerProducts.diagram F U)) ↦
              {
                hom :=
                  {
                    hom :=
                      𝟙
                        (Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
                          (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)),
                    w := ⋯ },
                inv := { hom := 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt, w := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ :
                Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c ≅
                  Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c })
            c) ≫
        CategoryTheory.Functor.map (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) f))
have w : f.hom ≫ 𝟙 d.pt = 𝟙 c.pt ≫ f.hom
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')
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.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app x =
    (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).π.app
      x
have op : ∀ (x : CategoryTheory.Pairwise ι),
  Eq (α :=
    (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
          (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
          (SheafConditionEqualizerProducts.fork F U)).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (op x))
    (𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app (op x))
    ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F 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.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
          (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
          (SheafConditionEqualizerProducts.fork F U)).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (op x))
    (𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app (op x))
    ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).π.app
      (op x))
have op : ∀ (a : ι),
  Eq (α :=
    (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
          (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
          (SheafConditionEqualizerProducts.fork F U)).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (op (single a)))
    (𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app (op (single a)))
    ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F 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)
a : ι
⊢ Eq (α :=
    (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
          (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
          (SheafConditionEqualizerProducts.fork F U)).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (op (single a)))
    (𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app (op (single a)))
    ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).π.app
      (op (single a)))
have op : F.map (Quiver.Hom.op (coconeιApp U (single a))) = F.map (leSupr U a).op
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.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
          (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
          (SheafConditionEqualizerProducts.fork F U)).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (op (Pairwise.pair a a_1)))
    (𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app (op (Pairwise.pair a a_1)))
    ((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)))
have op : 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)))
Tactic: dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                SheafConditionEqualizerProducts.leftRes]