[STATEMENT]
lemma eventually_at_Pair_within_TimesI2:
  fixes x::"'a::metric_space"
  assumes "\<forall>\<^sub>F y' in at y within Y. P y'" "P y"
  shows "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'
[PROOF STEP]
from assms[unfolded eventually_at_topological]
[PROOF STATE]
proof (chain)
picking this:
\<exists>S. open S \<and> y \<in> S \<and> (\<forall>x\<in>S. x \<noteq> y \<longrightarrow> x \<in> Y \<longrightarrow> P x)
P y
[PROOF STEP]
obtain S where S: "open S" "y \<in> S" "\<And>y'. y' \<in> Y \<Longrightarrow> y' \<in> S \<Longrightarrow> P y'"
[PROOF STATE]
proof (prove)
using this:
\<exists>S. open S \<and> y \<in> S \<and> (\<forall>x\<in>S. x \<noteq> y \<longrightarrow> x \<in> Y \<longrightarrow> P x)
P y

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>open S; y \<in> S; \<And>y'. \<lbrakk>y' \<in> Y; y' \<in> S\<rbrakk> \<Longrightarrow> P y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
open S
y \<in> S
\<lbrakk>?y' \<in> Y; ?y' \<in> S\<rbrakk> \<Longrightarrow> P ?y'

goal (1 subgoal):
 1. \<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'
[PROOF STEP]
show "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'
[PROOF STEP]
unfolding eventually_at_topological
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S. open S \<and> (x, y) \<in> S \<and> (\<forall>xa\<in>S. xa \<noteq> (x, y) \<longrightarrow> xa \<in> X \<times> Y \<longrightarrow> (case xa of (x', x) \<Rightarrow> P x))
[PROOF STEP]
by (auto intro!: exI[where x="UNIV \<times> S"] S open_Times)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'

goal:
No subgoals!
[PROOF STEP]
qed