[STATEMENT]
lemma AE_ball_countable:
  assumes [intro]: "countable X"
  shows "(AE x in M. \<forall>y\<in>X. P x y) \<longleftrightarrow> (\<forall>y\<in>X. AE x in M. P x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (AE x in M. \<forall>y\<in>X. P x y) = (\<forall>y\<in>X. AE x in M. P x y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
assume "\<forall>y\<in>X. AE x in M. P x y"
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>X. AE x in M. P x y

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
from this[unfolded eventually_ae_filter Bex_def, THEN bchoice]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x\<in>X. f x \<in> null_sets M \<and> {xa \<in> space M. \<not> P xa x} \<subseteq> f x
[PROOF STEP]
obtain N where N: "\<And>y. y \<in> X \<Longrightarrow> N y \<in> null_sets M" "\<And>y. y \<in> X \<Longrightarrow> {x\<in>space M. \<not> P x y} \<subseteq> N y"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x\<in>X. f x \<in> null_sets M \<and> {xa \<in> space M. \<not> P xa x} \<subseteq> f x

goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<And>y. y \<in> X \<Longrightarrow> N y \<in> null_sets M; \<And>y. y \<in> X \<Longrightarrow> {x \<in> space M. \<not> P x y} \<subseteq> N y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?y \<in> X \<Longrightarrow> N ?y \<in> null_sets M
?y \<in> X \<Longrightarrow> {x \<in> space M. \<not> P x ?y} \<subseteq> N ?y

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
have "{x\<in>space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. {x\<in>space M. \<not> P x y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. {x \<in> space M. \<not> P x y})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. {x \<in> space M. \<not> P x y})

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. {x \<in> space M. \<not> P x y})

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
have "\<dots> \<subseteq> (\<Union>y\<in>X. N y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>y\<in>X. {x \<in> space M. \<not> P x y}) \<subseteq> \<Union> (N ` X)
[PROOF STEP]
using N
[PROOF STATE]
proof (prove)
using this:
?y \<in> X \<Longrightarrow> N ?y \<in> null_sets M
?y \<in> X \<Longrightarrow> {x \<in> space M. \<not> P x ?y} \<subseteq> N ?y

goal (1 subgoal):
 1. (\<Union>y\<in>X. {x \<in> space M. \<not> P x y}) \<subseteq> \<Union> (N ` X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>y\<in>X. {x \<in> space M. \<not> P x y}) \<subseteq> \<Union> (N ` X)

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)
[PROOF STEP]
have "{x\<in>space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. N y)"
[PROOF STATE]
proof (prove)
using this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)

goal (1 subgoal):
 1. {x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
?y \<in> X \<Longrightarrow> N ?y \<in> null_sets M
?y \<in> X \<Longrightarrow> {x \<in> space M. \<not> P x ?y} \<subseteq> N ?y
[PROOF STEP]
have "(\<Union>y\<in>X. N y) \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
?y \<in> X \<Longrightarrow> N ?y \<in> null_sets M
?y \<in> X \<Longrightarrow> {x \<in> space M. \<not> P x ?y} \<subseteq> N ?y

goal (1 subgoal):
 1. \<Union> (N ` X) \<in> null_sets M
[PROOF STEP]
by (intro null_sets_UN') auto
[PROOF STATE]
proof (state)
this:
\<Union> (N ` X) \<in> null_sets M

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)
\<Union> (N ` X) \<in> null_sets M
[PROOF STEP]
show "AE x in M. \<forall>y\<in>X. P x y"
[PROOF STATE]
proof (prove)
using this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)
\<Union> (N ` X) \<in> null_sets M

goal (1 subgoal):
 1. AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
unfolding eventually_ae_filter
[PROOF STATE]
proof (prove)
using this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)
\<Union> (N ` X) \<in> null_sets M

goal (1 subgoal):
 1. Bex (null_sets M) ((\<subseteq>) {x \<in> space M. \<not> Ball X (P x)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. \<forall>y\<in>X. P x y

goal (1 subgoal):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
[PROOF STEP]
qed auto