[STATEMENT]
lemma tendsto_unique_eventually:
  fixes x x' :: "'a :: t2_space"
  shows "F \<noteq> bot \<Longrightarrow> eventually (\<lambda>x. f x = g x) F \<Longrightarrow> (f \<longlongrightarrow> x) F \<Longrightarrow> (g \<longlongrightarrow> x') F \<Longrightarrow> x = x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<noteq> \<bottom>; \<forall>\<^sub>F x in F. f x = g x; (f \<longlongrightarrow> x) F; (g \<longlongrightarrow> x') F\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
by (metis tendsto_unique filterlim_cong)