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)
i j : ι
h :
  c.π.app WalkingParallelPair.one =
    Fork.ι c ≫
      Pi.lift fun (p : ι × ι) ↦
        Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
      (Fork.ι c ≫
        Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2))))
      (Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i))
⊢ 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 : Eq (α := c.pt ⟶ F.obj (op (U j ⊓ U i)))
  (CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
      (Fork.ι c ≫
        Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (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)) :
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
      F.obj (op (U (j, i).1 ⊓ U (j, i).2)))
  (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE sorry).op : c.pt ⟶ F.obj (op (U j ⊓ U i)))
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.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2)))
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    CategoryStruct.comp (Y := (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
      (Fork.ι c ≫
        Pi.lift fun (p : ι × ι) ↦
          Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.2 ≫ F.map (Quiver.Hom.op ((U p.1).infLERight (U p.2))))
      (Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i))
⊢ Eq (α := c.pt ⟶ F.obj (op (U j ⊓ U i)))
    (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)) :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
        F.obj (op (U (j, i).1 ⊓ U (j, i).2)))
    (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op : c.pt ⟶ F.obj (op (U j ⊓ U i)))
have op : Eq (α := c.pt ⟶ F.obj (op (U j ⊓ U i)))
  (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (Quiver.Hom.op ((U j).infLERight (U i))))
  (Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i ≫ F.map (homOfLE sorry).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')
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a a_1 : ι
⊢ Eq.{v + 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)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (op (Pairwise.pair a a_1)))
      (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Quiver.Hom.op (id_pair a a_1)))
      (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (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 a a_1))))
    (CategoryStruct.comp (Y := (Functor.op (diagram U) ⋙ F).obj (op (Pairwise.pair a a_1)))
      (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (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 a a_1)))
      ((Functor.op (diagram U) ⋙ F).map (Quiver.Hom.op (id_pair a a_1))))
have op : 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (a, a_1) =
  (c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (a, a_1)) ≫
    F.map (𝟙 (op (U a ⊓ U a_1)))
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)
a a_1 : ι
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (a, a_1) =
    (c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (a, a_1)) ≫
      F.map (𝟙 (op (U a ⊓ U a_1)))
have op : 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (a, a_1) =
  (c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (a, a_1)) ≫
    𝟙 (F.obj (op (U a ⊓ U a_1)))
Tactic: 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 c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
x : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ f.hom ≫ (coneEquivInverseObj F U c').π.app x = (coneEquivInverseObj F U c).π.app x
have op : ∀ (x : CategoryTheory.Pairwise ι),
  Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op x))
    (f.hom ≫ (coneEquivInverseObj F U c').π.app (op x)) ((coneEquivInverseObj F U c).π.app (op x))
Tactic: 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')
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
x : CategoryTheory.Pairwise ι
⊢ Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op x))
    (f.hom ≫ (coneEquivInverseObj F U c').π.app (op x)) ((coneEquivInverseObj F U c).π.app (op x))
have op : ∀ (i : ι),
  Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op (single i)))
    (f.hom ≫ (coneEquivInverseObj F U c').π.app (op (single i))) ((coneEquivInverseObj F U c).π.app (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 c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
x : CategoryTheory.Pairwise ι
op :
  ∀ (i : ι),
    Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single i)))
      (f.hom ≫ (coneEquivInverseObj F U c').π.app (Opposite.op (single i)))
      ((coneEquivInverseObj F U c).π.app (Opposite.op (single i)))
⊢ Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
    (f.hom ≫ (coneEquivInverseObj F U c').π.app (Opposite.op x)) ((coneEquivInverseObj F U c).π.app (Opposite.op x))
have op₁ : ∀ (i j : ι),
  Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair i j)))
    (f.hom ≫ (coneEquivInverseObj F U c').π.app (Opposite.op (Pairwise.pair i j)))
    ((coneEquivInverseObj F U c).π.app (Opposite.op (Pairwise.pair i j)))
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 c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i : ι
⊢ Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op (single i)))
    (f.hom ≫ (coneEquivInverseObj F U c').π.app (op (single i))) ((coneEquivInverseObj F U c).π.app (op (single i)))
have op : f.hom ≫ Fork.ι c' ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i = Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) 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 c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i : ι
⊢ f.hom ≫ Fork.ι c' ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i = Fork.ι c ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i
have op : f.hom ≫ c'.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i =
  c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i
Tactic: dsimp only [Fork.ι]
-- 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 c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i : ι
⊢ f.hom ≫ c'.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i =
    c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i
have op : f.hom ≫ c'.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i =
  (f.hom ≫ c'.π.app WalkingParallelPair.zero) ≫ Pi.π (fun (i : ι) ↦ F.obj (op (U i))) i
Tactic: rw [← f.w WalkingParallelPair.zero, 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')
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
⊢ 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
have 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
Tactic: rw [← f.w WalkingParallelPair.zero, 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')
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i j : ι
⊢ Eq (α := (coneEquivInverseObj F U c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (op (Pairwise.pair i j)))
    (f.hom ≫ (coneEquivInverseObj F U c').π.app (op (Pairwise.pair i j)))
    ((coneEquivInverseObj F U c).π.app (op (Pairwise.pair i j)))
have op : f.hom ≫ c'.π.app WalkingParallelPair.one ≫ 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)
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 c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i j : ι
⊢ f.hom ≫ c'.π.app WalkingParallelPair.one ≫ 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)
have op : f.hom ≫ c'.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
  (f.hom ≫ c'.π.app WalkingParallelPair.one) ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j)
Tactic: rw [← f.w WalkingParallelPair.one, 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')
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)
⊢ 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)
have 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)
Tactic: rw [← f.w WalkingParallelPair.one, 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')
c : Cone (Functor.op (diagram U) ⋙ F)
j : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ 𝟙 (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
have op : ∀ (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: induction j with | op j => ?_
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 ι
⊢ 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))
have op : ∀ (a : ι),
  Eq (α :=
    (Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (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
        (op (single a)))
    ((Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) 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.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)))
⊢ 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))
have 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)))
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.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ⟶ (Functor.op (diagram U) ⋙ F).obj (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
        (op (single a)))
    ((Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (op (single a)))
have op : 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: 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.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (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
        (op (Pairwise.pair a a_1)))
    ((Functor.obj (𝟭 (Cone (Functor.op (diagram U) ⋙ F))) c).π.app (op (Pairwise.pair a a_1)))
have op : 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: 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)
j : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ 𝟙
        ((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
have 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 (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: induction j with | op j => ?_
Cleared hypotheses: j