[STATEMENT]
lemma sets_lebesgue_inner_closed:
  fixes e::real
  assumes "S \<in> sets lebesgue" "e > 0"
  obtains T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "emeasure lebesgue (S - T) < ennreal e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T. \<lbrakk>closed T; T \<subseteq> S; S - T \<in> lmeasurable; emeasure lebesgue (S - T) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>T. \<lbrakk>closed T; T \<subseteq> S; S - T \<in> lmeasurable; emeasure lebesgue (S - T) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "-S \<in> sets lebesgue"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - S \<in> sets lebesgue
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
S \<in> sets lebesgue
0 < e

goal (1 subgoal):
 1. - S \<in> sets lebesgue
[PROOF STEP]
by (simp add: Compl_in_sets_lebesgue)
[PROOF STATE]
proof (state)
this:
- S \<in> sets lebesgue

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>closed T; T \<subseteq> S; S - T \<in> lmeasurable; emeasure lebesgue (S - T) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
- S \<in> sets lebesgue
[PROOF STEP]
obtain T where "open T" "-S \<subseteq> T"
          and T: "(T - -S) \<in> lmeasurable" "emeasure lebesgue (T - -S) < e"
[PROOF STATE]
proof (prove)
using this:
- S \<in> sets lebesgue

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>open T; - S \<subseteq> T; T - - S \<in> lmeasurable; emeasure lebesgue (T - - S) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sets_lebesgue_outer_open assms
[PROOF STATE]
proof (prove)
using this:
- S \<in> sets lebesgue
\<lbrakk>?S \<in> sets lebesgue; 0 < ?e; \<And>T. \<lbrakk>open T; ?S \<subseteq> T; T - ?S \<in> lmeasurable; emeasure lebesgue (T - ?S) < ennreal ?e\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
S \<in> sets lebesgue
0 < e

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>open T; - S \<subseteq> T; T - - S \<in> lmeasurable; emeasure lebesgue (T - - S) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
open T
- S \<subseteq> T
T - - S \<in> lmeasurable
emeasure lebesgue (T - - S) < ennreal e

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>closed T; T \<subseteq> S; S - T \<in> lmeasurable; emeasure lebesgue (S - T) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. closed ?T
 2. ?T \<subseteq> S
 3. S - ?T \<in> lmeasurable
 4. emeasure lebesgue (S - ?T) < ennreal e
[PROOF STEP]
show "closed (-T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (- T)
[PROOF STEP]
using \<open>open T\<close>
[PROOF STATE]
proof (prove)
using this:
open T

goal (1 subgoal):
 1. closed (- T)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
closed (- T)

goal (3 subgoals):
 1. - T \<subseteq> S
 2. S - - T \<in> lmeasurable
 3. emeasure lebesgue (S - - T) < ennreal e
[PROOF STEP]
show "-T \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - T \<subseteq> S
[PROOF STEP]
using \<open>- S \<subseteq> T\<close>
[PROOF STATE]
proof (prove)
using this:
- S \<subseteq> T

goal (1 subgoal):
 1. - T \<subseteq> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- T \<subseteq> S

goal (2 subgoals):
 1. S - - T \<in> lmeasurable
 2. emeasure lebesgue (S - - T) < ennreal e
[PROOF STEP]
show "S - ( -T) \<in> lmeasurable" "emeasure lebesgue (S - (- T)) < e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S - - T \<in> lmeasurable &&& emeasure lebesgue (S - - T) < ennreal e
[PROOF STEP]
using T
[PROOF STATE]
proof (prove)
using this:
T - - S \<in> lmeasurable
emeasure lebesgue (T - - S) < ennreal e

goal (1 subgoal):
 1. S - - T \<in> lmeasurable &&& emeasure lebesgue (S - - T) < ennreal e
[PROOF STEP]
by (auto simp: Int_commute)
[PROOF STATE]
proof (state)
this:
S - - T \<in> lmeasurable
emeasure lebesgue (S - - T) < ennreal e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed