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')
G : Presheaf.{v', v, u} C X
α : F ≅ G
⊢ Eq (α := (diagram F U).obj WalkingParallelPair.zero ⟶ (diagram G U).obj WalkingParallelPair.one)
    ((diagram F U).map WalkingParallelPairHom.left ≫
      Iso.hom
        (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
          (diagram F U).obj x ≅ (diagram G U).obj x) WalkingParallelPair.one (piOpens.isoOfIso U α)
          (piInters.isoOfIso U α)))
    (Iso.hom
        (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
          (diagram F U).obj x ≅ (diagram G U).obj x) WalkingParallelPair.zero (piOpens.isoOfIso U α)
          (piInters.isoOfIso U α)) ≫
      (diagram G U).map WalkingParallelPairHom.left)
have zero : Eq (α := piOpens F U ⟶ piInters G U)
  (leftRes F U ≫ Iso.hom (Pi.mapIso fun (x : ι × ι) ↦ α.app (op (U x.1 ⊓ U x.2))) : piOpens F U ⟶ piInters G U)
  (CategoryStruct.comp (Y := piOpens G U)
      (Iso.hom (Pi.mapIso fun (x : ι) ↦ α.app (op (U x))) : piOpens F U ⟶ piOpens G U)
      (leftRes G U : piOpens G U ⟶ piInters G U) :
    piOpens F U ⟶ piInters G 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')
G : Presheaf.{v', v, u} C X
α : F ≅ G
⊢ Eq (α := piOpens F U ⟶ piInters G U)
    (leftRes F U ≫ Iso.hom (Pi.mapIso fun (x : ι × ι) ↦ α.app (op (U x.1 ⊓ U x.2))) : piOpens F U ⟶ piInters G U)
    (CategoryStruct.comp (Y := piOpens G U)
        (Iso.hom (Pi.mapIso fun (x : ι) ↦ α.app (op (U x))) : piOpens F U ⟶ piOpens G U)
        (leftRes G U : piOpens G U ⟶ piInters G U) :
      piOpens F U ⟶ piInters G U)
have zero : ∀ (b : ι × ι),
  Eq (α := piOpens F U ⟶ G.obj (op (U b.1 ⊓ U b.2)))
    (CategoryStruct.comp (Y := piObj.{v', v, u} fun (p : ι × ι) ↦ G.obj (op (U p.1 ⊓ U p.2)))
        (leftRes F U ≫ Iso.hom (Pi.mapIso fun (x : ι × ι) ↦ α.app (op (U x.1 ⊓ U x.2))) : piOpens F U ⟶ piInters G U)
        (Pi.π (fun (p : ι × ι) ↦ G.obj (op (U p.1 ⊓ U p.2))) b :
          (piObj.{v', v, u} fun (p : ι × ι) ↦ G.obj (op (U p.1 ⊓ U p.2))) ⟶ G.obj (op (U b.1 ⊓ U b.2))) :
      piOpens F U ⟶ G.obj (op (U b.1 ⊓ U b.2)))
    (CategoryStruct.comp (Y := piObj.{v', v, u} fun (p : ι × ι) ↦ G.obj (op (U p.1 ⊓ U p.2)))
        (CategoryStruct.comp (Y := piOpens G U)
            (Iso.hom (Pi.mapIso fun (x : ι) ↦ α.app (op (U x))) : piOpens F U ⟶ piOpens G U)
            (leftRes G U : piOpens G U ⟶ piInters G U) :
          piOpens F U ⟶ piInters G U)
        (Pi.π (fun (p : ι × ι) ↦ G.obj (op (U p.1 ⊓ U p.2))) b) :
      piOpens F U ⟶ G.obj (op (U b.1 ⊓ U b.2)))
Tactic: refine Pi.hom_ext _ _ fun b ↦ ?_
-- 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')
G : Presheaf.{v', v, u} C X
α : F ≅ G
⊢ Eq (α := (diagram F U).obj WalkingParallelPair.zero ⟶ (diagram G U).obj WalkingParallelPair.one)
    ((diagram F U).map WalkingParallelPairHom.right ≫
      Iso.hom
        (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
          (diagram F U).obj x ≅ (diagram G U).obj x) WalkingParallelPair.one (piOpens.isoOfIso U α)
          (piInters.isoOfIso U α)))
    (Iso.hom
        (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
          (diagram F U).obj x ≅ (diagram G U).obj x) WalkingParallelPair.zero (piOpens.isoOfIso U α)
          (piInters.isoOfIso U α)) ≫
      (diagram G U).map WalkingParallelPairHom.right)
have zero : Eq (α := piOpens F U ⟶ piInters G U)
  (rightRes F U ≫ Iso.hom (Pi.mapIso fun (x : ι × ι) ↦ α.app (op (U x.1 ⊓ U x.2))) : piOpens F U ⟶ piInters G U)
  (CategoryStruct.comp (Y := piOpens G U)
      (Iso.hom (Pi.mapIso fun (x : ι) ↦ α.app (op (U x))) : piOpens F U ⟶ piOpens G U)
      (rightRes G U : piOpens G U ⟶ piInters G U) :
    piOpens F U ⟶ piInters G U)
Tactic: dsimp [diagram]
-- 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')
G : Presheaf.{v', v, u} C X
α : F ≅ G
⊢ Eq (α := piOpens F U ⟶ piInters G U)
    (rightRes F U ≫ Iso.hom (Pi.mapIso fun (x : ι × ι) ↦ α.app (op (U x.1 ⊓ U x.2))) : piOpens F U ⟶ piInters G U)
    (CategoryStruct.comp (Y := piOpens G U)
        (Iso.hom (Pi.mapIso fun (x : ι) ↦ α.app (op (U x))) : piOpens F U ⟶ piOpens G U)
        (rightRes G U : piOpens G U ⟶ piInters G U) :
      piOpens F U ⟶ piInters G U)
have zero : ∀ (b : ι × ι),
  Eq (α := piOpens F U ⟶ G.obj (op (U b.1 ⊓ U b.2)))
    (CategoryStruct.comp (Y := piObj.{v', v, u} fun (p : ι × ι) ↦ G.obj (op (U p.1 ⊓ U p.2)))
        (rightRes F U ≫ Iso.hom (Pi.mapIso fun (x : ι × ι) ↦ α.app (op (U x.1 ⊓ U x.2))) : piOpens F U ⟶ piInters G U)
        (Pi.π (fun (p : ι × ι) ↦ G.obj (op (U p.1 ⊓ U p.2))) b :
          (piObj.{v', v, u} fun (p : ι × ι) ↦ G.obj (op (U p.1 ⊓ U p.2))) ⟶ G.obj (op (U b.1 ⊓ U b.2))) :
      piOpens F U ⟶ G.obj (op (U b.1 ⊓ U b.2)))
    (CategoryStruct.comp (Y := piObj.{v', v, u} fun (p : ι × ι) ↦ G.obj (op (U p.1 ⊓ U p.2)))
        (CategoryStruct.comp (Y := piOpens G U)
            (Iso.hom (Pi.mapIso fun (x : ι) ↦ α.app (op (U x))) : piOpens F U ⟶ piOpens G U)
            (rightRes G U : piOpens G U ⟶ piInters G U) :
          piOpens F U ⟶ piInters G U)
        (Pi.π (fun (p : ι × ι) ↦ G.obj (op (U p.1 ⊓ U p.2))) b) :
      piOpens F U ⟶ G.obj (op (U b.1 ⊓ U b.2)))
Tactic: refine Pi.hom_ext _ _ fun b ↦ ?_
-- 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')
G : Presheaf.{v', v, u} C X
α : F ≅ G
⊢ Iso (C := Fork (X := piOpens F U) (leftRes F U) (rightRes F U)) (fork F U)
    (Functor.obj (Cone.postcompose (Iso.inv (diagram.isoOfIso U α))) (fork G U))
have i : Cone.pt (F := parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U)) (fork F U) ≅
  Cone.pt (F := parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U))
    (Functor.obj (Cone.postcompose (Iso.inv (diagram.isoOfIso U α))) (fork G U))
Tactic: fapply Fork.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')
G : Presheaf.{v', v, u} C X
α : F ≅ G
i :
  Cone.pt (F := parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U)) (fork F U) ≅
    Cone.pt (F := parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U))
      (Functor.obj (Cone.postcompose (Iso.inv (diagram.isoOfIso U α))) (fork G U))
⊢ Iso (C := Fork (X := piOpens F U) (leftRes F U) (rightRes F U)) (fork F U)
    (Functor.obj (Cone.postcompose (Iso.inv (diagram.isoOfIso U α))) (fork G U))
have w : autoParam
  (Eq (α := Cone.pt (F := parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U)) (fork F U) ⟶ piOpens F U)
    (Iso.hom (α.app (op (iSup U))) ≫
      Fork.ι (Functor.obj (Cone.postcompose (Iso.inv (diagram.isoOfIso U α))) (fork G U)))
    (Fork.ι (fork F U)))
  Fork.ext._auto_1
Tactic: fapply Fork.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')
G : Presheaf.{v', v, u} C X
α : F ≅ G
⊢ autoParam
    (Eq (α := Cone.pt (F := parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U)) (fork F U) ⟶ piOpens F U)
      (Iso.hom (α.app (op (iSup U))) ≫
        Fork.ι (Functor.obj (Cone.postcompose (Iso.inv (diagram.isoOfIso U α))) (fork G U)))
      (Fork.ι (fork F U)))
    Fork.ext._auto_1
have w : autoParam
  (Eq (α := F.obj (op (iSup U)) ⟶ piOpens F U)
    (α.hom.app (op (iSup U)) ≫ Fork.ι (Functor.obj (Cone.postcompose (Iso.inv (diagram.isoOfIso U α))) (fork G U)))
    (res F U))
  Fork.ext._auto_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')
G : Presheaf.{v', v, u} C X
α : F ≅ G
⊢ autoParam
    (Eq (α := F.obj (op (iSup U)) ⟶ piOpens F U)
      (α.hom.app (op (iSup U)) ≫ Fork.ι (Functor.obj (Cone.postcompose (Iso.inv (diagram.isoOfIso U α))) (fork G U)))
      (res F U))
    Fork.ext._auto_1
have w : ∀ (b : ι),
  CategoryStruct.comp (Y := piObj.{v', v, u} fun (i : ι) ↦ F.obj (op (U i)))
      (α.hom.app (op (iSup U)) ≫ Fork.ι (Functor.obj (Cone.postcompose (Iso.inv (diagram.isoOfIso U α))) (fork G U)))
      (Pi.π (fun (i : ι) ↦ F.obj (op (U i))) b) =
    CategoryStruct.comp (Y := piObj.{v', v, u} fun (i : ι) ↦ F.obj (op (U i)))
      (res F U : F.obj (op (iSup U)) ⟶ piOpens F U) (Pi.π (fun (i : ι) ↦ F.obj (op (U i))) b)
Tactic: refine Pi.hom_ext _ _ fun b ↦ ?_
-- 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')
G : Presheaf.{v', v, u} C X
α : F ≅ G
b : ι
⊢ CategoryStruct.comp (Y := piObj.{v', v, u} fun (i : ι) ↦ F.obj (op (U i)))
      (α.hom.app (op (iSup U)) ≫ Fork.ι (Functor.obj (Cone.postcompose (Iso.inv (diagram.isoOfIso U α))) (fork G U)))
      (Pi.π (fun (i : ι) ↦ F.obj (op (U i))) b) =
    CategoryStruct.comp (Y := piObj.{v', v, u} fun (i : ι) ↦ F.obj (op (U i)))
      (res F U : F.obj (op (iSup U)) ⟶ piOpens F U) (Pi.π (fun (i : ι) ↦ F.obj (op (U i))) b)
have w : CategoryStruct.comp (Y := piObj.{v', v, u} fun (i : ι) ↦ F.obj (op (U i)))
    (α.hom.app (op (iSup U)) ≫
      NatTrans.app (Cone.π (Functor.obj (Cone.postcompose (Iso.inv (diagram.isoOfIso U α))) (fork G U)))
        WalkingParallelPair.zero)
    (Pi.π (fun (i : ι) ↦ F.obj (op (U i))) b) =
  CategoryStruct.comp (Y := piObj.{v', v, u} fun (i : ι) ↦ F.obj (op (U i)))
    (res F U : F.obj (op (iSup U)) ⟶ piOpens F U) (Pi.π (fun (i : ι) ↦ F.obj (op (U i))) b)
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 : Cone (Functor.op (diagram U) ⋙ F)
Y Z : WalkingParallelPair
f : Y ⟶ Z
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) Y ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj Z)
    (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)
        Z (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)
        Y (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 zero : ∀ (f : WalkingParallelPair.zero ⟶ Z),
  Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj Z)
    (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)
        Z (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 f)
Tactic: cases Y
Cleared hypotheses: Y, 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)
Z : WalkingParallelPair
f : WalkingParallelPair.zero ⟶ Z
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj Z)
    (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)
        Z (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 f)
have zero : ∀ (f : WalkingParallelPair.zero ⟶ WalkingParallelPair.zero),
  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) 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.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 f)
Tactic: cases Z
Cleared hypotheses: Z, 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)
Z : WalkingParallelPair
f : WalkingParallelPair.one ⟶ Z
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj Z)
    (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)
        Z (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 : ∀ (f : WalkingParallelPair.one ⟶ WalkingParallelPair.zero),
  Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.zero)
    (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.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.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)
Tactic: cases Z
Cleared hypotheses: Z, 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)
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.zero
⊢ 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) 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.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 f)
have zero : 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))
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)
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.one
⊢ 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) 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.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 f)
have zero : 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)
Tactic: cases f
Cleared hypotheses: f