-- 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)
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.one
zero :
  Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPairHom.left ≫
      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))))
    (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 WalkingParallelPairHom.left)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
      (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
    (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)
        WalkingParallelPair.one (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)
have zero₁ : Eq.{v + 1} (α :=
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPair.zero ⟶
    (SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one)
  (CategoryTheory.Functor.map (Functor.obj (Functor.const WalkingParallelPair) c.pt) WalkingParallelPairHom.right ≫
    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))))
  (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 WalkingParallelPairHom.right)
Tactic: cases f
Cleared hypotheses: f