[STATEMENT]
lemma nhds_imp_cauchy_filter:
  assumes *: "F \<le> nhds x"
  shows "cauchy_filter F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
have "F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x
[PROOF STEP]
by (intro prod_filter_mono *)
[PROOF STATE]
proof (state)
this:
F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x

goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x

goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
have "\<dots> \<le> uniformity"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nhds x \<times>\<^sub>F nhds x \<le> uniformity
[PROOF STEP]
unfolding le_filter_def eventually_nhds_uniformity eventually_prod_same
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P. eventually P uniformity \<longrightarrow> (\<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. eventually P uniformity \<Longrightarrow> \<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. eventually P uniformity \<Longrightarrow> \<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))
[PROOF STEP]
assume "eventually P uniformity"
[PROOF STATE]
proof (state)
this:
eventually P uniformity

goal (1 subgoal):
 1. \<And>P. eventually P uniformity \<Longrightarrow> \<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eventually P uniformity
[PROOF STEP]
obtain Ql where ev: "eventually Ql uniformity"
      and "Ql (x, y) \<Longrightarrow> Ql (y, z) \<Longrightarrow> P (x, z)" for x y z
[PROOF STATE]
proof (prove)
using this:
eventually P uniformity

goal (1 subgoal):
 1. (\<And>Ql. \<lbrakk>eventually Ql uniformity; \<And>x y z. \<lbrakk>Ql (x, y); Ql (y, z)\<rbrakk> \<Longrightarrow> P (x, z)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule uniformity_transE) simp
[PROOF STATE]
proof (state)
this:
eventually Ql uniformity
\<lbrakk>Ql (?x, ?y); Ql (?y, ?z)\<rbrakk> \<Longrightarrow> P (?x, ?z)

goal (1 subgoal):
 1. \<And>P. eventually P uniformity \<Longrightarrow> \<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))
[PROOF STEP]
with ev[THEN uniformity_sym]
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F (x, y) in uniformity. Ql (y, x)
eventually Ql uniformity
\<lbrakk>Ql (?x, ?y); Ql (?y, ?z)\<rbrakk> \<Longrightarrow> P (?x, ?z)
[PROOF STEP]
show "\<exists>Q. eventually (\<lambda>(x', y). x' = x \<longrightarrow> Q y) uniformity \<and>
        (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F (x, y) in uniformity. Ql (y, x)
eventually Ql uniformity
\<lbrakk>Ql (?x, ?y); Ql (?y, ?z)\<rbrakk> \<Longrightarrow> P (?x, ?z)

goal (1 subgoal):
 1. \<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))
[PROOF STEP]
by (rule_tac exI[of _ "\<lambda>y. Ql (y, x) \<and> Ql (x, y)"]) (fastforce elim: eventually_elim2)
[PROOF STATE]
proof (state)
this:
\<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nhds x \<times>\<^sub>F nhds x \<le> uniformity

goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
F \<times>\<^sub>F F \<le> uniformity
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F \<times>\<^sub>F F \<le> uniformity

goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
by (simp add: cauchy_filter_def)
[PROOF STATE]
proof (state)
this:
cauchy_filter F

goal:
No subgoals!
[PROOF STEP]
qed