-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
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)
y : CategoryTheory.Pairwise ι
a a_1 : ι
f' : unop (Opposite.op y) ⟶ unop (Opposite.op (Pairwise.pair a a_1))
op :
  ∀ (a_2 : ι) (f' : unop (Opposite.op (single a_2)) ⟶ unop (Opposite.op (Pairwise.pair a a_1))),
    Eq.{v + 1} (α :=
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
          (Opposite.op (Pairwise.pair a a_1)) ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a_2)))
      (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) f'.op ≫
        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 (single a_2)))
      (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 (Pairwise.pair a a_1)) ≫
        (Functor.op (diagram U) ⋙ F).map f'.op)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (Pairwise.pair a a_1)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op y))
    (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) f'.op ≫
      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 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 (Pairwise.pair a a_1)) ≫
      (Functor.op (diagram U) ⋙ F).map f'.op)
have op₁ : ∀ (j j_1 : ι) (f' : unop (Opposite.op (Pairwise.pair j j_1)) ⟶ unop (Opposite.op (Pairwise.pair a a_1))),
  Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt)
        (Opposite.op (Pairwise.pair a a_1)) ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair j j_1)))
    (CategoryTheory.Functor.map (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) f'.op ≫
      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 (Pairwise.pair j j_1)))
    (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 (Pairwise.pair a a_1)) ≫
      (Functor.op (diagram U) ⋙ F).map f'.op)
Tactic: rcases y with (⟨⟩ | ⟨j, j⟩)
Cleared hypotheses: y, f'