awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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')
⊢ Eq (α := Cone.pt (F := parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U)) (fork F U) ⟶ piOpens F U)
    (Fork.ι (fork F U)) (res F U)

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.limit.lift, rfl, TopCat.Presheaf.SheafConditionEqualizerProducts.res
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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')
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const WalkingParallelPair)
          (Cone.pt (F := parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U)) (fork F U)))
        WalkingParallelPair.zero ⟶
      (parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U)).obj WalkingParallelPair.zero)
    (NatTrans.app (Cone.π (fork F U)) WalkingParallelPair.zero) (res F U)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.lift, rfl, TopCat.Presheaf.SheafConditionEqualizerProducts.res
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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')
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const WalkingParallelPair)
          (Cone.pt (F := parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U)) (fork F U)))
        WalkingParallelPair.one ⟶
      (parallelPair (X := piOpens F U) (leftRes F U) (rightRes F U)).obj WalkingParallelPair.one)
    (NatTrans.app (Cone.π (fork F U)) WalkingParallelPair.one) (res F U ≫ leftRes F U)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit, TopCat.Presheaf.SheafConditionEqualizerProducts.piInters, rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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
⊢ (diagram F U).obj WalkingParallelPair.zero ≅ (diagram G U).obj WalkingParallelPair.zero

Tactic:
exact piOpens.isoOfIso U α

Premises used: TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIso
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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
⊢ (diagram F U).obj WalkingParallelPair.one ≅ (diagram G U).obj WalkingParallelPair.one

Tactic:
exact piInters.isoOfIso U α

Premises used: TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIso
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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.zero)
    ((diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      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 α)))
    (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.id WalkingParallelPair.zero))

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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
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)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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)

Tactic:
Pi.hom_ext _ _ fun b ↦ ?_

Premises used: CategoryTheory.Limits.Pi.hom_ext, TopCat.Presheaf.SheafConditionEqualizerProducts.piInters
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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
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)))
⊢ 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:
refine Pi.hom_ext _ _ fun b ↦ ?_

Premises used: CategoryTheory.Limits.Pi.hom_ext
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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 : ι × ι
⊢ 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:
simp [leftRes]

Premises used: TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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
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)
⊢ 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)

Tactic:
dsimp [diagram]

Premises used: TopCat.Presheaf.SheafConditionEqualizerProducts.diagram
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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)

Tactic:
Pi.hom_ext _ _ fun b ↦ ?_

Premises used: CategoryTheory.Limits.Pi.hom_ext, TopCat.Presheaf.SheafConditionEqualizerProducts.piInters
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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
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)))
⊢ 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:
refine Pi.hom_ext _ _ fun b ↦ ?_

Premises used: CategoryTheory.Limits.Pi.hom_ext
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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 : ι × ι
⊢ 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:
simp [rightRes]

Premises used: TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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.one ⟶ (diagram G U).obj WalkingParallelPair.one)
    ((diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      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.one (piOpens.isoOfIso U α)
          (piInters.isoOfIso U α)) ≫
      (diagram G U).map (WalkingParallelPairHom.id WalkingParallelPair.one))

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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))
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
⊢ 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))

Tactic:
fapply Fork.ext

Premises used: CategoryTheory.Limits.Fork.ext
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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
⊢ 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:
apply α.app

Premises used: CategoryTheory.Iso.app
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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
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
⊢ 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:
dsimp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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

Tactic:
Pi.hom_ext _ _ fun b ↦ ?_

Premises used: CategoryTheory.Limits.Pi.hom_ext, TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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
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)
⊢ 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:
refine Pi.hom_ext _ _ fun b ↦ ?_

Premises used: CategoryTheory.Limits.Pi.hom_ext
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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 : ι
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)
⊢ 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:
dsimp only [Fork.ι]

Premises used: CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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)) ≫
        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:
simp [res, diagram.isoOfIso]

Premises used: TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso, TopCat.Presheaf.SheafConditionEqualizerProducts.res
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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
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))
⊢ 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 f