Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.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 : Cone (SheafConditionEqualizerProducts.diagram F U)
y : CategoryTheory.Pairwise ι
i : ι
f' : unop (op y) ⟶ unop (op (single i))
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      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 y) =
    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 f'.op

pp: case op.op.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)
y : CategoryTheory.Pairwise ι
a✝¹ a✝ : ι
f' : unop (op y) ⟶ unop (op (Pairwise.pair a✝¹ a✝))
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      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 y) =
    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 f'.op

Tactic:
<;>

Goal state after:
case op.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 : Cone (SheafConditionEqualizerProducts.diagram F U)
y : CategoryTheory.Pairwise ι
i : ι
f' : unop (op y) ⟶ unop (op (single i))
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      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 y) =
    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 f'.op

case op.op.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)
y : CategoryTheory.Pairwise ι
a✝¹ a✝ : ι
f' : unop (op y) ⟶ unop (op (Pairwise.pair a✝¹ a✝))
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      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 y) =
    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 f'.op