-- 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 (SheafConditionEqualizerProducts.diagram F U)
x y : (CategoryTheory.Pairwise ι)ᵒᵖ
f : x ⟶ y
op :
  ∀ (x : CategoryTheory.Pairwise ι) (f : Opposite.op x ⟶ y),
    Eq.{v + 1} (α :=
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (Opposite.op x) ⟶
        (Functor.op (diagram U) ⋙ F).obj y)
      (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) f ≫
        Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
          Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
            (Functor.op (diagram U) ⋙ F).obj x)
          (fun (x : CategoryTheory.Pairwise ι) ↦
            Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
              Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
                  (Opposite.op x) ⟶
                (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
              x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i)
              fun (i j : ι) ↦
              c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j))
          y)
      (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
          Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
            (Functor.op (diagram U) ⋙ F).obj x)
          (fun (x : CategoryTheory.Pairwise ι) ↦
            Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
              Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
                  (Opposite.op x) ⟶
                (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
              x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i)
              fun (i j : ι) ↦
              c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j))
          (Opposite.op x) ≫
        (Functor.op (diagram U) ⋙ F).map f)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
      (Functor.op (diagram U) ⋙ F).obj y)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) f ≫
      Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
                (Opposite.op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i)
            fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j))
        y)
    (Opposite.rec (motive := fun (x : (CategoryTheory.Pairwise ι)ᵒᵖ) ↦
        Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) x ⟶
          (Functor.op (diagram U) ⋙ F).obj x)
        (fun (x : CategoryTheory.Pairwise ι) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise ι) ↦
            Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
                (Opposite.op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
            x (fun (i : ι) ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun (i : ι) ↦ F.obj (Opposite.op (U i))) i)
            fun (i j : ι) ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun (p : ι × ι) ↦ F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j))
        x ≫
      (Functor.op (diagram U) ⋙ F).map f)

Tactic:
induction x with | op x => ?_

Premises used: Opposite.op