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)
f : WalkingParallelPair.one ⟶ WalkingParallelPair.one
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) f ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map f)
have one : Eq.{v + 1} (α :=
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
    (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
  (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt)
      (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
    WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
        (SheafConditionEqualizerProducts.diagram F U).obj x)
      WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
      (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
  (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
        (SheafConditionEqualizerProducts.diagram F U).obj x)
      WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
      (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
    (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one))
Tactic: cases f
Cleared hypotheses: f
-- 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)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.zero)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt)
        (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.zero (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.zero (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.zero))
have zero : (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) =
  (Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫
    (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.zero)
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 (Functor.op (diagram U) ⋙ F)
⊢ (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) =
    (Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.zero)
have zero : ∀ (j : Discrete ι),
  CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
      (𝟙 c.pt ≫ Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j) =
    ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫
        (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.zero)) ≫
      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 (Functor.op (diagram U) ⋙ F)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPairHom.left ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.zero (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.left)
have zero : Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
  (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)) :
    c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
  ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U :
    c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
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 (Functor.op (diagram U) ⋙ F)
⊢ Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)) :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
have zero : ∀ (ij : Discrete (ι × ι)),
  CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij)
Tactic: ext ij
-- 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)
ij : Discrete (ι × ι)
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij)
have zero : ∀ (i j : ι),
  CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) }) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) : Discrete (ι × ι) })
Tactic: rcases ij with ⟨i, j⟩
Cleared hypotheses: ij
-- 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)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPairHom.right ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.zero (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.right)
have zero : Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
  (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)) :
    c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
  ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U :
    c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
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 (Functor.op (diagram U) ⋙ F)
⊢ Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)) :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U :
      c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
have zero : ∀ (ij : Discrete (ι × ι)),
  CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij)
Tactic: ext ij
-- 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)
ij : Discrete (ι × ι)
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) ij)
have zero : ∀ (i j : ι),
  CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) }) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      ((Pi.lift fun (i : ι) ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) { as := (i, j) : Discrete (ι × ι) })
Tactic: rcases ij with ⟨i, j⟩
Cleared hypotheses: ij
-- 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)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt)
        (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one))
have one : (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
  (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
    (SheafConditionEqualizerProducts.diagram F U).map (𝟙 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 (Functor.op (diagram U) ⋙ F)
⊢ (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.one)
have one : ∀ (j : Discrete (ι × ι)),
  CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 c.pt ≫ Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) =
    ((Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
        (SheafConditionEqualizerProducts.diagram F U).map (𝟙 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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
j : WalkingParallelPair
⊢ Eq (α :=
    Cone.pt (F := SheafConditionEqualizerProducts.diagram F U) (coneEquivFunctorObj F U c) ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj j)
    (f.hom ≫ NatTrans.app (Cone.π (coneEquivFunctorObj F U c')) j) (NatTrans.app (Cone.π (coneEquivFunctorObj F U c)) j)
have zero : Eq (α :=
  Cone.pt (F := SheafConditionEqualizerProducts.diagram F U) (coneEquivFunctorObj F U c) ⟶
    (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.zero)
  (f.hom ≫ NatTrans.app (Cone.π (coneEquivFunctorObj F U c')) WalkingParallelPair.zero)
  (NatTrans.app (Cone.π (coneEquivFunctorObj F U c)) WalkingParallelPair.zero)
Tactic: cases 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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
j : WalkingParallelPair
zero :
  Eq (α :=
    Cone.pt (F := SheafConditionEqualizerProducts.diagram F U) (coneEquivFunctorObj F U c) ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.zero)
    (f.hom ≫ NatTrans.app (Cone.π (coneEquivFunctorObj F U c')) WalkingParallelPair.zero)
    (NatTrans.app (Cone.π (coneEquivFunctorObj F U c)) WalkingParallelPair.zero)
⊢ Eq (α :=
    Cone.pt (F := SheafConditionEqualizerProducts.diagram F U) (coneEquivFunctorObj F U c) ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj j)
    (f.hom ≫ NatTrans.app (Cone.π (coneEquivFunctorObj F U c')) j) (NatTrans.app (Cone.π (coneEquivFunctorObj F U c)) j)
have one : Eq (α :=
  Cone.pt (F := SheafConditionEqualizerProducts.diagram F U) (coneEquivFunctorObj F U c) ⟶
    (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
  (f.hom ≫ NatTrans.app (Cone.π (coneEquivFunctorObj F U c')) WalkingParallelPair.one)
  (NatTrans.app (Cone.π (coneEquivFunctorObj F U c)) WalkingParallelPair.one)
Tactic: cases 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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
⊢ Eq (α :=
    Cone.pt (F := SheafConditionEqualizerProducts.diagram F U) (coneEquivFunctorObj F U c) ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.zero)
    (f.hom ≫ NatTrans.app (Cone.π (coneEquivFunctorObj F U c')) WalkingParallelPair.zero)
    (NatTrans.app (Cone.π (coneEquivFunctorObj F U c)) WalkingParallelPair.zero)
have zero : Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piOpens F U) (f.hom ≫ Pi.lift fun (i : ι) ↦ c'.π.app (op (single i)))
  (Pi.lift fun (i : ι) ↦ 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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
⊢ Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piOpens F U) (f.hom ≫ Pi.lift fun (i : ι) ↦ c'.π.app (op (single i)))
    (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
have zero : ∀ (j : Discrete ι),
  Eq (α := c.pt ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j)
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
      (f.hom ≫ Pi.lift fun (i : ι) ↦ c'.π.app (op (single i)))
      (limit.π (Discrete.functor fun (i : ι) ↦ F.obj (op (U i))) j))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
      (Pi.lift fun (i : ι) ↦ 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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
⊢ Eq (α :=
    Cone.pt (F := SheafConditionEqualizerProducts.diagram F U) (coneEquivFunctorObj F U c) ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (f.hom ≫ NatTrans.app (Cone.π (coneEquivFunctorObj F U c')) WalkingParallelPair.one)
    (NatTrans.app (Cone.π (coneEquivFunctorObj F U c)) WalkingParallelPair.one)
have one : Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
  (f.hom ≫ Pi.lift fun (b : ι × ι) ↦ c'.π.app (op (Pairwise.pair b.1 b.2)))
  (Pi.lift fun (b : ι × ι) ↦ 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 c' : Cone (Functor.op (diagram U) ⋙ F)
f : c ⟶ c'
⊢ Eq (α := c.pt ⟶ SheafConditionEqualizerProducts.piInters F U)
    (f.hom ≫ Pi.lift fun (b : ι × ι) ↦ c'.π.app (op (Pairwise.pair b.1 b.2)))
    (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2)))
have one : ∀ (j : Discrete (ι × ι)),
  Eq (α := c.pt ⟶ Functor.obj.{v', v, v', u} (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (f.hom ≫ Pi.lift fun (b : ι × ι) ↦ c'.π.app (op (Pairwise.pair b.1 b.2)))
      (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 : ι × ι) ↦ 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)
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
have op : (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)
Tactic: induction x with | op x => ?_
Cleared hypotheses: x