[STATEMENT]
lemma depth_lowerB: "v \<in> verts T \<Longrightarrow> depth w \<ge> \<mu> w root v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> verts T \<Longrightarrow> \<mu> w root v \<le> depth w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> verts T \<Longrightarrow> \<mu> w root v \<le> depth w
[PROOF STEP]
assume "v \<in> verts T"
[PROOF STATE]
proof (state)
this:
v \<in> verts T

goal (1 subgoal):
 1. v \<in> verts T \<Longrightarrow> \<mu> w root v \<le> depth w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> verts T
[PROOF STEP]
have "\<mu> w root v \<in> {\<mu> w root v|v. v \<in> verts T}"
[PROOF STATE]
proof (prove)
using this:
v \<in> verts T

goal (1 subgoal):
 1. \<mu> w root v \<in> {\<mu> w root v |v. v \<in> verts T}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> w root v \<in> {\<mu> w root v |v. v \<in> verts T}

goal (1 subgoal):
 1. v \<in> verts T \<Longrightarrow> \<mu> w root v \<le> depth w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<mu> w root v \<in> {\<mu> w root v |v. v \<in> verts T}
[PROOF STEP]
show "depth w \<ge> \<mu> w root v"
[PROOF STATE]
proof (prove)
using this:
\<mu> w root v \<in> {\<mu> w root v |v. v \<in> verts T}

goal (1 subgoal):
 1. \<mu> w root v \<le> depth w
[PROOF STEP]
unfolding depth_def
[PROOF STATE]
proof (prove)
using this:
\<mu> w root v \<in> {\<mu> w root v |v. v \<in> verts T}

goal (1 subgoal):
 1. \<mu> w root v \<le> Sup {\<mu> w root v |v. v \<in> verts T}
[PROOF STEP]
by (simp add: Sup_upper)
[PROOF STATE]
proof (state)
this:
\<mu> w root v \<le> depth w

goal:
No subgoals!
[PROOF STEP]
qed