Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op
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)
x y : CategoryTheory.Pairwise ι
f' : unop (op y) ⟶ unop (op x)
⊢ ((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 x) ≫
      ((diagram U).op ⋙ F).map f'.op

Tactic:
rcases x with (⟨i⟩ | ⟨⟩) <;> rcases y with (⟨⟩ | ⟨j, j⟩) <;> rcases f' with ⟨⟩

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 : ι
⊢ ((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))

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))

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))

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✝))