Dijkstra's Algorithm Invariant I am trying to prove the first assertion in the following code, taken from notes of Damon Wischik:
def dijkstra(g, s):
    for v in g.vertices:
        v.distance = ∞
    s.distance = 0
    toexplore =  PriorityQueue([s], sortkey = lambda  v: v.distance)

    while not toexplore.isempty():
        v = toexplore.popmin()
        # Assert: v.distance is the true shortest path distance between s and v
        # Assert: v is never put back into toexplore
        for (w, edgecost) in v.neighbours:
            dist_w = v.distance + edgecost
            if dist_w &lt; w.distance:
                w.distance = dist_w
                if w in toexplore:
                    toexplore.decreasekey(w)
                else:
                    toexplore.push(w)

Base case: The estimate of the source node is correct when it is popped.
Inductive step: Consider the shortest path from the source node $s$ to some destination node $d$,
$$ s \to v_1 \to v_2 \to \cdots \to v_k \to d. $$
Assume that the estimates for $s,v_1,v_2,\ldots,v_k$ are correct when they are popped.
When $d$ is popped, we can be sure that $s, v_1, v_2, \dots, v_k$ were popped prior to that as their true shortest distances from the source $s$ are lower than that of $d$. In particular, when $v_k$ is popped, we are sure that the edge $(v_k, d)$ will be relaxed since relaxing the edge $(v_k, d)$ gives us the true shortest distance from the source to the destination, which is definitely an improvement on any prior estimate of D. Hence D's estimate is the true shortest distance from the source when it is popped.
Hence the assertion is true.
Is there a flaw in my proof?
I believe your proof is a bit incomplete, since you do not guarantee the shortest path to $d$ is a path which only traverses the popped nodes. You can add this part to make you proof complete :
Assume the shortest path to our vertex $d$ is the path $s \to u_1 \to u_ 2 \to \cdots \to u_l \to x \to \cdots \to  d$
Where nodes $s, u_1, u_2, \cdots, u_l$ are popped earlier, therefore their distances are correctly determined, and $x$ as the first vertex which is not popped yet. Since the edges are nonnegative, therefore $dist_x \le dist_d$ (let $dist_v$ be the actual distance of the vertex $v$). Since $x$ is the first vertex which is not popped yet, it's distance should now have been determined by relaxing $(u_l, x)$. We assumed $d$ has the smallest estimate, let it be $est_d$, so $est_d \le est_x = dist_x$, and thus $est_d \le dist_x \le dist_d \implies est_d \le dist_d$, and since estimate can never be less than actual distance, $est_d = dist_d$.
I hope my answer was helpful.