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 (SheafConditionEqualizerProducts.diagram F U)
x : CategoryTheory.Pairwise ι
⊢ Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
    (Functor.op (diagram U) ⋙ F).obj (op x)
have op : (i : ι) →
  Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op (single i)) ⟶
    (Functor.op (diagram U) ⋙ F).obj (op (single i))
Tactic: rcases x with (⟨i⟩ | ⟨i, j⟩)
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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x : CategoryTheory.Pairwise ι
op :
  (i : ι) →
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (single i)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single i))
⊢ 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)
have op₁ : (i j : ι) →
  Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
      (Opposite.op (Pairwise.pair i j)) ⟶
    (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair i j))
Tactic: rcases x with (⟨i⟩ | ⟨i, j⟩)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
      (Functor.op (diagram U) ⋙ F).obj (op y))
    (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) f ≫
      Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op y))
    (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op x) ≫
      (Functor.op (diagram U) ⋙ F).map f)
have ef : f = f.unop.op
Tactic: have ef : f = f.unop.op := rfl
-- 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)
i : ι
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op (single i)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (op (single i)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op (single i)))
      (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Quiver.Hom.op (id_single i)))
      (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (single i))))
    (CategoryStruct.comp (Y := (Functor.op (diagram U) ⋙ F).obj (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) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (single i)))
      ((Functor.op (diagram U) ⋙ F).map (Quiver.Hom.op (id_single i))))
have op : 𝟙 c.pt ≫ Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i =
  (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) ≫ F.map (𝟙 (op (U 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)
i : ι
⊢ 𝟙 c.pt ≫ Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i =
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) ≫ F.map (𝟙 (op (U i)))
have op : 𝟙 c.pt ≫ Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i =
  (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) ≫ 𝟙 (F.obj (op (U i)))
Tactic: rw [F.map_id]
-- 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)
i j : ι
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op (single i)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (op (Pairwise.pair i j)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (op (Pairwise.pair i j)))
      (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Quiver.Hom.op (left i j)))
      (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (Pairwise.pair i j))))
    (CategoryStruct.comp (Y := (Functor.op (diagram U) ⋙ F).obj (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) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (single i)))
      ((Functor.op (diagram U) ⋙ F).map (Quiver.Hom.op (left i j))))
have op : 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
  (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) ≫ F.map (homOfLE sorry).op
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)
i j : ι
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) ≫ F.map (homOfLE ⋯).op
have op : c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
  Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE sorry).op
Tactic: simp only [Category.id_comp, Category.assoc]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (hypothesis)
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 : ι
⊢ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op
have h : CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPairHom.left ≫
    c.π.app WalkingParallelPair.one =
  c.π.app WalkingParallelPair.zero ≫ (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.left
Tactic: have h := c.π.naturality WalkingParallelPairHom.left
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  𝟙 c.pt ≫ c.π.app WalkingParallelPair.one =
    Fork.ι c ≫
      Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))
⊢ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op
have 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)))
Tactic: simp only [Category.id_comp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (hypothesis)
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) =
    Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op
have 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))
Tactic: have h' := h =≫ Pi.π _ (i, 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 (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))
⊢ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op
have op : Eq (α := c.pt ⟶ F.obj (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 (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)) :
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
      F.obj (op (U (i, j).1 ⊓ U (i, j).2)))
  (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE sorry).op : c.pt ⟶ F.obj (op (U i ⊓ U j)))
Tactic: rw [h']
-- 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)
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)))
    (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)) :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
        F.obj (op (U (i, j).1 ⊓ U (i, j).2)))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op : c.pt ⟶ F.obj (op (U i ⊓ U j)))
have op : 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 sorry).op)
Tactic: simp only [Category.assoc, limit.lift_π, Fan.mk_π_app]
-- 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)
i j : ι
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op (single i)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (op (Pairwise.pair j i)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (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) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (Pairwise.pair j i))))
    (CategoryStruct.comp (Y := (Functor.op (diagram U) ⋙ F).obj (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) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (single i)))
      ((Functor.op (diagram U) ⋙ F).map (Quiver.Hom.op (right j i))))
have op : 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
  (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) ≫ F.map (homOfLE sorry).op
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)
i j : ι
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i) ≫ F.map (homOfLE ⋯).op
have op : c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
  Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE sorry).op
Tactic: simp only [Category.id_comp, Category.assoc]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (hypothesis)
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 : ι
⊢ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op
have h : 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
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (hypothesis)
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 ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op
have 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)))
Tactic: simp only [Category.id_comp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (hypothesis)
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) =
    Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op
have 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))
Tactic: have h' := h =≫ Pi.π _ (j, i)