[STATEMENT]
lemma point_indices_balanced: "point_indices \<t> = {\<Lambda>\<^sub>t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. point_indices \<t> = {\<Lambda>\<^sub>t}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. point_indices \<t> = {\<Lambda>\<^sub>t}
[PROOF STEP]
have "point_indices \<t> = {i . \<exists> ps . i = \<B> index ps \<and> card ps = \<t> \<and> ps \<subseteq> \<V>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. point_indices \<t> = {\<B> index ps |ps. card ps = \<t> \<and> ps \<subseteq> \<V>}
[PROOF STEP]
by (simp add: point_indices_def)
[PROOF STATE]
proof (state)
this:
point_indices \<t> = {\<B> index ps |ps. card ps = \<t> \<and> ps \<subseteq> \<V>}

goal (1 subgoal):
 1. point_indices \<t> = {\<Lambda>\<^sub>t}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
point_indices \<t> = {\<B> index ps |ps. card ps = \<t> \<and> ps \<subseteq> \<V>}
[PROOF STEP]
have "point_indices  \<t> = {i . i = \<Lambda>\<^sub>t}"
[PROOF STATE]
proof (prove)
using this:
point_indices \<t> = {\<B> index ps |ps. card ps = \<t> \<and> ps \<subseteq> \<V>}

goal (1 subgoal):
 1. point_indices \<t> = {i. i = \<Lambda>\<^sub>t}
[PROOF STEP]
using balanced Collect_cong obtain_t_subset_points
[PROOF STATE]
proof (prove)
using this:
point_indices \<t> = {\<B> index ps |ps. card ps = \<t> \<and> ps \<subseteq> \<V>}
\<lbrakk>?ps \<subseteq> \<V>; card ?ps = \<t>\<rbrakk> \<Longrightarrow> \<B> index ?ps = \<Lambda>\<^sub>t
(\<And>x. ?P x = ?Q x) \<Longrightarrow> {x. ?P x} = {x. ?Q x}
(\<And>T. \<lbrakk>T \<subseteq> \<V>; card T = \<t>; finite T\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. point_indices \<t> = {i. i = \<Lambda>\<^sub>t}
[PROOF STEP]
by (smt (verit, best))
[PROOF STATE]
proof (state)
this:
point_indices \<t> = {i. i = \<Lambda>\<^sub>t}

goal (1 subgoal):
 1. point_indices \<t> = {\<Lambda>\<^sub>t}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
point_indices \<t> = {i. i = \<Lambda>\<^sub>t}

goal (1 subgoal):
 1. point_indices \<t> = {\<Lambda>\<^sub>t}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
point_indices \<t> = {\<Lambda>\<^sub>t}

goal:
No subgoals!
[PROOF STEP]
qed