-- 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 : Quiver.Hom (V := WalkingCospan) none none
⊢ Eq (α := obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none ⟶ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj none)
    (map (cospan f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
              obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
          none))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
              | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
              | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
              obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
          none) ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).map f)
have none : Eq (α := obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none ⟶ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj none)
  (map (cospan f_1.op g.op) (WidePullbackShape.Hom.id none) ≫
    Iso.hom
      ((fun (x : WalkingCospan) ↦
          (match (motive :=
              (x : WalkingCospan) →
                obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
              x with
            | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
            | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
            | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
            obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
        none))
  (Iso.hom
      ((fun (x : WalkingCospan) ↦
          (match (motive :=
              (x : WalkingCospan) →
                obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x)
              x with
            | none => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) none)
            | some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.left)
            | some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) WalkingCospan.right) :
            obj.{0, v₁, 0, u₁} (cospan f_1.op g.op) x ≅ (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).obj x))
        none) ≫
    (walkingSpanOpEquiv.inverse ⋙ (span f_1 g).op).map (WidePullbackShape.Hom.id none))
Tactic: cases f
Cleared hypotheses: f