-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f_1 : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ Eq (α :=
    (cospan f_1.unop g.unop).obj (some WalkingPair.left) ⟶
      obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) (some WalkingPair.left))
    ((cospan f_1.unop g.unop).map f ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
                x with
              | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
              (cospan f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
          (some WalkingPair.left)))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
                x with
              | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
              (cospan f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
          (some WalkingPair.left)) ≫
      map (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) f)
have some : Eq (α :=
  (cospan f_1.unop g.unop).obj (some WalkingPair.left) ⟶
    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) (some WalkingPair.left))
  ((cospan f_1.unop g.unop).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
    Iso.hom
      ((fun (x : WalkingCospan) ↦
          (match (motive :=
              (x : WalkingCospan) →
                (cospan f_1.unop g.unop).obj x ≅
                  obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
              x with
            | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
            | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
            | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
            (cospan f_1.unop g.unop).obj x ≅
              obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
        (some WalkingPair.left)))
  (Iso.hom
      ((fun (x : WalkingCospan) ↦
          (match (motive :=
              (x : WalkingCospan) →
                (cospan f_1.unop g.unop).obj x ≅
                  obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
              x with
            | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
            | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
            | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
            (cospan f_1.unop g.unop).obj x ≅
              obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
        (some WalkingPair.left)) ≫
    map (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) (WidePullbackShape.Hom.id (some WalkingPair.left)))
Tactic: cases f
Cleared hypotheses: f