[STATEMENT]
lemma real_lim_then_eventually_real:
  assumes "(u \<longlongrightarrow> ereal l) F"
  shows "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
have "ereal l \<in> {-\<infinity><..<(\<infinity>::ereal)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ereal l \<in> {- \<infinity><..<\<infinity>}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ereal l \<in> {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ereal l \<in> {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
have "open {-\<infinity><..<(\<infinity>::ereal)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open {- \<infinity><..<\<infinity>}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
open {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ereal l \<in> {- \<infinity><..<\<infinity>}
open {- \<infinity><..<\<infinity>}
[PROOF STEP]
have "eventually (\<lambda>n. u n \<in> {-\<infinity><..<(\<infinity>::ereal)}) F"
[PROOF STATE]
proof (prove)
using this:
ereal l \<in> {- \<infinity><..<\<infinity>}
open {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}
[PROOF STEP]
using assms tendsto_def
[PROOF STATE]
proof (prove)
using this:
ereal l \<in> {- \<infinity><..<\<infinity>}
open {- \<infinity><..<\<infinity>}
(u \<longlongrightarrow> ereal l) F
(?f \<longlongrightarrow> ?l) ?F = (\<forall>S. open S \<longrightarrow> ?l \<in> S \<longrightarrow> (\<forall>\<^sub>F x in ?F. ?f x \<in> S))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
have "\<And>x. x \<in> {-\<infinity><..<(\<infinity>::ereal)} \<Longrightarrow> x = ereal(real_of_ereal x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {- \<infinity><..<\<infinity>} \<Longrightarrow> x = ereal (real_of_ereal x)
[PROOF STEP]
using ereal_real
[PROOF STATE]
proof (prove)
using this:
ereal (real_of_ereal ?x) = (if \<bar>?x\<bar> = \<infinity> then 0 else ?x)

goal (1 subgoal):
 1. \<And>x. x \<in> {- \<infinity><..<\<infinity>} \<Longrightarrow> x = ereal (real_of_ereal x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> {- \<infinity><..<\<infinity>} \<Longrightarrow> ?x = ereal (real_of_ereal ?x)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}
?x \<in> {- \<infinity><..<\<infinity>} \<Longrightarrow> ?x = ereal (real_of_ereal ?x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}
?x \<in> {- \<infinity><..<\<infinity>} \<Longrightarrow> ?x = ereal (real_of_ereal ?x)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
by (metis (mono_tags, lifting) eventually_mono)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))

goal:
No subgoals!
[PROOF STEP]
qed