-- 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')
P :
  IsLimit (F :=
    parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
      (SheafConditionEqualizerProducts.rightRes F U))
    (SheafConditionEqualizerProducts.fork F U)
x : CategoryTheory.Pairwise ι
op :
  ∀ (a : ι),
    Eq (α :=
      (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ⟶
        (Functor.op (diagram U) ⋙ F).obj (Opposite.op (single a)))
      (𝟙
          (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).pt ≫
        (Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op (single a)))
      ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
              (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
              (SheafConditionEqualizerProducts.fork F U)).π.app
        (Opposite.op (single a)))
⊢ Eq (α :=
    (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
          (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
          (SheafConditionEqualizerProducts.fork F U)).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op x))
    (𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op x))
    ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).π.app
      (Opposite.op x))
have op₁ : ∀ (a a_1 : ι),
  Eq (α :=
    (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
          (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
          (SheafConditionEqualizerProducts.fork F U)).pt ⟶
      (Functor.op (diagram U) ⋙ F).obj (Opposite.op (Pairwise.pair a a_1)))
    (𝟙
        (Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (Cocone.op (cocone U))).π.app (Opposite.op (Pairwise.pair a a_1)))
    ((Functor.obj (C := Cone (SheafConditionEqualizerProducts.diagram F U))
            (Equivalence.functor (CategoryTheory.Equivalence.symm (coneEquiv F U)))
            (SheafConditionEqualizerProducts.fork F U)).π.app
      (Opposite.op (Pairwise.pair a a_1)))
Tactic: rcases x with ⟨⟩
Cleared hypotheses: x