-- 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 (Functor.op (diagram U) ⋙ F)
Y Z : WalkingParallelPair
f : Y ⟶ Z
zero :
  ∀ (f : WalkingParallelPair.zero ⟶ Z),
    Eq.{v + 1} (α :=
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
        (SheafConditionEqualizerProducts.diagram F U).obj Z)
      (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) f ≫
        WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
            (SheafConditionEqualizerProducts.diagram F U).obj x)
          Z (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
          (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
      (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
            (SheafConditionEqualizerProducts.diagram F U).obj x)
          WalkingParallelPair.zero (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
          (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
        (SheafConditionEqualizerProducts.diagram F U).map f)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) Y ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj Z)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) f ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        Z (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        Y (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map f)
have one : ∀ (f : WalkingParallelPair.one ⟶ Z),
  Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.one ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj Z)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) f ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        Z (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))))
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) x ⟶
          (SheafConditionEqualizerProducts.diagram F U).obj x)
        WalkingParallelPair.one (Pi.lift fun (i : ι) ↦ c.π.app (op (single i)))
        (Pi.lift fun (b : ι × ι) ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map f)
Tactic: cases Y
Cleared hypotheses: Y, f