[STATEMENT]
lemma Int_convex_hull_insert_rel_exterior:
  fixes z :: "'a::euclidean_space"
  assumes "convex C" "T \<subseteq> C" and z: "z \<in> rel_interior C" and dis: "disjnt S (rel_interior C)"
  shows "S \<inter> (convex hull (insert z T)) = S \<inter> (convex hull T)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> convex hull insert z T = S \<inter> convex hull T
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S \<inter> convex hull insert z T \<subseteq> S \<inter> convex hull T
 2. S \<inter> convex hull T \<subseteq> S \<inter> convex hull insert z T
[PROOF STEP]
have "T = {} \<Longrightarrow> z \<notin> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T = {} \<Longrightarrow> z \<notin> S
[PROOF STEP]
using dis z
[PROOF STATE]
proof (prove)
using this:
disjnt S (rel_interior C)
z \<in> rel_interior C

goal (1 subgoal):
 1. T = {} \<Longrightarrow> z \<notin> S
[PROOF STEP]
by (auto simp add: disjnt_def)
[PROOF STATE]
proof (state)
this:
T = {} \<Longrightarrow> z \<notin> S

goal (2 subgoals):
 1. S \<inter> convex hull insert z T \<subseteq> S \<inter> convex hull T
 2. S \<inter> convex hull T \<subseteq> S \<inter> convex hull insert z T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T = {} \<Longrightarrow> z \<notin> S
[PROOF STEP]
show "?lhs \<subseteq> ?rhs"
[PROOF STATE]
proof (prove)
using this:
T = {} \<Longrightarrow> z \<notin> S

goal (1 subgoal):
 1. S \<inter> convex hull insert z T \<subseteq> S \<inter> convex hull T
[PROOF STEP]
proof (clarsimp simp add: convex_hull_insert_segments)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
assume "x \<in> S" and y: "y \<in> convex hull T" and "x \<in> closed_segment z y"
[PROOF STATE]
proof (state)
this:
x \<in> S
y \<in> convex hull T
x \<in> closed_segment z y

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
have "y \<in> closure C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> closure C
[PROOF STEP]
by (metis y \<open>convex C\<close> \<open>T \<subseteq> C\<close> closure_subset contra_subsetD convex_hull_eq hull_mono)
[PROOF STATE]
proof (state)
this:
y \<in> closure C

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> closure C

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
have "x \<notin> rel_interior C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> rel_interior C
[PROOF STEP]
by (meson \<open>x \<in> S\<close> dis disjnt_iff)
[PROOF STATE]
proof (state)
this:
x \<notin> rel_interior C

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<notin> rel_interior C

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
have "x \<in> open_segment z y \<union> {z, y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> open_segment z y \<union> {z, y}
[PROOF STEP]
using \<open>x \<in> closed_segment z y\<close> closed_segment_eq_open
[PROOF STATE]
proof (prove)
using this:
x \<in> closed_segment z y
closed_segment ?a ?b = open_segment ?a ?b \<union> {?a, ?b}

goal (1 subgoal):
 1. x \<in> open_segment z y \<union> {z, y}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> open_segment z y \<union> {z, y}

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<in> closure C
x \<notin> rel_interior C
x \<in> open_segment z y \<union> {z, y}
[PROOF STEP]
show "x \<in> convex hull T"
[PROOF STATE]
proof (prove)
using this:
y \<in> closure C
x \<notin> rel_interior C
x \<in> open_segment z y \<union> {z, y}

goal (1 subgoal):
 1. x \<in> convex hull T
[PROOF STEP]
using rel_interior_closure_convex_segment [OF \<open>convex C\<close> z]
[PROOF STATE]
proof (prove)
using this:
y \<in> closure C
x \<notin> rel_interior C
x \<in> open_segment z y \<union> {z, y}
?b \<in> closure C \<Longrightarrow> open_segment z ?b \<subseteq> rel_interior C

goal (1 subgoal):
 1. x \<in> convex hull T
[PROOF STEP]
using y z
[PROOF STATE]
proof (prove)
using this:
y \<in> closure C
x \<notin> rel_interior C
x \<in> open_segment z y \<union> {z, y}
?b \<in> closure C \<Longrightarrow> open_segment z ?b \<subseteq> rel_interior C
y \<in> convex hull T
z \<in> rel_interior C

goal (1 subgoal):
 1. x \<in> convex hull T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> convex hull T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<inter> convex hull insert z T \<subseteq> S \<inter> convex hull T

goal (1 subgoal):
 1. S \<inter> convex hull T \<subseteq> S \<inter> convex hull insert z T
[PROOF STEP]
show "?rhs \<subseteq> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> convex hull T \<subseteq> S \<inter> convex hull insert z T
[PROOF STEP]
by (meson hull_mono inf_mono subset_insertI subset_refl)
[PROOF STATE]
proof (state)
this:
S \<inter> convex hull T \<subseteq> S \<inter> convex hull insert z T

goal:
No subgoals!
[PROOF STEP]
qed