mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
⊢ ((𝟭 (Presheaf C X)).map f ≫ toSkyscraperPresheaf p₀ (𝟙 (((𝟭 (Presheaf C X)).obj 𝓖).stalk p₀))).app (op U) =
    (toSkyscraperPresheaf p₀ (𝟙 (((𝟭 (Presheaf C X)).obj 𝓕).stalk p₀)) ≫
          (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀).map f).app
      (op U)

Tactic:
dsimp

Goal state after:
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
⊢ (f.app (op U) ≫
      if h : p₀ ∈ U then 𝓖.germ U p₀ h ≫ 𝟙 (𝓖.stalk p₀) ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓖.obj (op U))) =
    (if h : p₀ ∈ U then 𝓕.germ U p₀ h ≫ 𝟙 (𝓕.stalk p₀) ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj (op U))) ≫
      if h : p₀ ∈ U then eqToHom ⋯ ≫ (Presheaf.stalkFunctor C p₀).map f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U then 𝓕.stalk p₀ else ⊤_ C)
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
U : (Opens ↑X)ᵒᵖ
h : p₀ ∉ unop U
⊢ IsTerminal ((skyscraperSheaf p₀ A).obj.obj U)

Tactic:
dsimp

Goal state after:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
U : (Opens ↑X)ᵒᵖ
h : p₀ ∉ unop U
⊢ IsTerminal (if p₀ ∈ unop U then A else ⊤_ C)
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
hm :
  ∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
    m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j
⊢ m = limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S)

Tactic:
dsimp

Goal state after:
X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
hm :
  ∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
    m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j
⊢ m = limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S)
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: case inr.inl
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑i ⟶ ↑j)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op))
      ((ConcreteCategory.hom ((F.obj ⋙ CategoryTheory.forget AddCommGrpCat).map ↑h₁.some.right)) (↑i).right.snd)

Tactic:
dsimp

Goal state after:
case inr.inl
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑i ⟶ ↑j)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op))
      ((ConcreteCategory.hom (F.obj.map ↑h₁.some.right)) (↑i).right.snd)
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: case inr.inr
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑j ⟶ ↑i)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op))
      ((ConcreteCategory.hom ((F.obj ⋙ CategoryTheory.forget AddCommGrpCat).map ↑h₁.some.right)) (↑j).right.snd) =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd

Tactic:
dsimp

Goal state after:
case inr.inr
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑j ⟶ ↑i)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op))
      ((ConcreteCategory.hom (F.obj.map ↑h₁.some.right)) (↑j).right.snd) =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map WalkingParallelPairHom.left ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map WalkingParallelPairHom.left

Tactic:
dsimp

Goal state after:
case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ leftRes F U ≫ (Pi.mapIso fun x ↦ α.app (op (U x.1 ⊓ U x.2))).hom =
    (Pi.mapIso fun x ↦ α.app (op (U x))).hom ≫ leftRes G U
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ autoParam
    ((α.app (op (iSup U))).hom ≫ Fork.ι ((Cone.postcompose (diagram.isoOfIso U α).inv).obj (fork G U)) = (fork F U).ι)
    Fork.ext._auto_1

Tactic:
dsimp

Goal state after:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ autoParam (α.hom.app (op (iSup U)) ≫ Fork.ι ((Cone.postcompose (diagram.isoOfIso U α).inv).obj (fork G U)) = res F U)
    Fork.ext._auto_1
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
Z : WalkingParallelPair
f : WalkingParallelPair.zero ⟶ Z
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn 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 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

Goal state after:
case zero.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.zero
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn 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 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

case zero.one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.one
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn 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 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
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
Z : WalkingParallelPair
f : WalkingParallelPair.one ⟶ Z
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn 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 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

Goal state after:
case one.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
f : WalkingParallelPair.one ⟶ WalkingParallelPair.zero
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn 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 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

case one.one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
f : WalkingParallelPair.one ⟶ WalkingParallelPair.one
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn 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 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
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.zero.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      WalkingParallelPair.casesOn 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 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:
dsimp

Goal state after:
case zero.zero.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ 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)
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map WalkingParallelPairHom.left ≫
      WalkingParallelPair.casesOn 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 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:
dsimp

Goal state after:
case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ (𝟙 c.pt ≫ Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    (Pi.lift fun i ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.leftRes F U
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map WalkingParallelPairHom.right ≫
      WalkingParallelPair.casesOn 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 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

Tactic:
dsimp

Goal state after:
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ (𝟙 c.pt ≫ Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    (Pi.lift fun i ↦ c.π.app (op (single i))) ≫ SheafConditionEqualizerProducts.rightRes F U
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      WalkingParallelPair.casesOn 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 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:
dsimp

Goal state after:
case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ 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)
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
⊢ f.hom ≫ (coneEquivFunctorObj F U c').π.app WalkingParallelPair.zero =
    (coneEquivFunctorObj F U c).π.app WalkingParallelPair.zero

Tactic:
dsimp

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
⊢ (f.hom ≫ Pi.lift fun i ↦ c'.π.app (op (single i))) = Pi.lift fun i ↦ c.π.app (op (single i))
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
⊢ f.hom ≫ (coneEquivFunctorObj F U c').π.app WalkingParallelPair.one =
    (coneEquivFunctorObj F U c).π.app WalkingParallelPair.one

Tactic:
dsimp

Goal state after:
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
⊢ (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))
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op.single.single.id_single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (Quiver.Hom.op (id_single i)) ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (single i)) =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (single i)) ≫
      ((diagram U).op ⋙ F).map (Quiver.Hom.op (id_single i))

Tactic:
dsimp

Goal state after:
case op.op.single.single.id_single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i : ι
⊢ 𝟙 c.pt ≫ Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i =
    (Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) ≫ F.map (𝟙 (op (U i)))
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (Quiver.Hom.op (left i j)) ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (Pairwise.pair i j)) =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (single i)) ≫
      ((diagram U).op ⋙ F).map (Quiver.Hom.op (left i j))

Tactic:
dsimp

Goal state after:
case op.op.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    (Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) ≫ F.map (homOfLE ⋯).op
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (Quiver.Hom.op (right j i)) ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (Pairwise.pair j i)) =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (single i)) ≫
      ((diagram U).op ⋙ F).map (Quiver.Hom.op (right j i))

Tactic:
dsimp

Goal state after:
case op.op.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    (Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) ≫ F.map (homOfLE ⋯).op
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op.pair.pair.id_pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a✝¹ a✝ : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (Quiver.Hom.op (id_pair a✝¹ a✝)) ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn 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✝)) =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn 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✝)) ≫
      ((diagram U).op ⋙ F).map (Quiver.Hom.op (id_pair a✝¹ a✝))

Tactic:
dsimp

Goal state after:
case op.op.pair.pair.id_pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a✝¹ a✝ : ι
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (a✝¹, a✝) =
    (c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (a✝¹, a✝)) ≫
      F.map (𝟙 (op (U a✝¹ ⊓ U a✝)))
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i : ι
⊢ f.hom ≫ (coneEquivInverseObj F U c').π.app (op (single i)) = (coneEquivInverseObj F U c).π.app (op (single i))

Tactic:
dsimp

Goal state after:
case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
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