-- 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)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
⊢ ∀ (ef : f = f.unop.op),
    Eq.{v + 1} (α :=
      Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
        (Functor.op (diagram U) ⋙ F).obj (op 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) (op x) ⟶
                (Functor.op (diagram U) ⋙ F).obj (op x))
              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 (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) (op x) ⟶
                (Functor.op (diagram U) ⋙ F).obj (op x))
              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) ≫
        (Functor.op (diagram U) ⋙ F).map f)
have op : ∀ (f' : unop (op y) ⟶ unop (op x)) (ef : f = f'.op),
  Eq.{v + 1} (α :=
    Functor.obj.{v', v, v', u} (Functor.obj (Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ) c.pt) (op x) ⟶
      (Functor.op (diagram U) ⋙ F).obj (op 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) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            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 (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) (op x) ⟶
              (Functor.op (diagram U) ⋙ F).obj (op x))
            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) ≫
      (Functor.op (diagram U) ⋙ F).map f)
Tactic: generalize f.unop = f'