-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f_1 g : X ⟶ Y
f : WalkingParallelPair.one ⟶ WalkingParallelPair.one
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one ⟶
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj WalkingParallelPair.one)
    (map (parallelPair f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
          WalkingParallelPair.one))
    (Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
          WalkingParallelPair.one) ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).map f)
have one : Eq (α :=
  obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one ⟶
    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj WalkingParallelPair.one)
  (map (parallelPair f_1.op g.op) (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
    Iso.hom
      ((fun (x : WalkingParallelPair) ↦
          (match (motive :=
              (x : WalkingParallelPair) →
                obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                  (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
              x with
            | WalkingParallelPair.zero =>
              Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
            | WalkingParallelPair.one =>
              Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
            obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
              (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
        WalkingParallelPair.one))
  (Iso.hom
      ((fun (x : WalkingParallelPair) ↦
          (match (motive :=
              (x : WalkingParallelPair) →
                obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                  (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
              x with
            | WalkingParallelPair.zero =>
              Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
            | WalkingParallelPair.one =>
              Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
            obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
              (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
        WalkingParallelPair.one) ≫
    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).map
      (WalkingParallelPairHom.id WalkingParallelPair.one))
Tactic: cases f
Cleared hypotheses: f