[STATEMENT]
lemma homeomorphic_map_derived_set_of:
  assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
  shows "Y derived_set_of (f ` S) = f ` (X derived_set_of S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
have fim: "f ` (topspace X) = topspace Y" and inj: "inj_on f (topspace X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` topspace X = topspace Y &&& inj_on f (topspace X)
[PROOF STEP]
using hom
[PROOF STATE]
proof (prove)
using this:
homeomorphic_map X Y f

goal (1 subgoal):
 1. f ` topspace X = topspace Y &&& inj_on f (topspace X)
[PROOF STEP]
by (auto simp: homeomorphic_eq_everything_map)
[PROOF STATE]
proof (state)
this:
f ` topspace X = topspace Y
inj_on f (topspace X)

goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
have iff: "(\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) =
            (\<forall>T. T \<subseteq> topspace Y \<longrightarrow> f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))"
    if "x \<in> topspace X" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
have \<section>: "(x \<in> T \<and> openin X T) = (T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T))" for T
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> T \<and> openin X T) = (T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T))
[PROOF STEP]
by (meson hom homeomorphic_map_openness_eq inj inj_on_image_mem_iff that)
[PROOF STATE]
proof (state)
this:
(x \<in> ?T \<and> openin X ?T) = (?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T))

goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x \<in> ?T \<and> openin X ?T) = (?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T))

goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
have "(\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T)"  (is "?lhs = ?rhs")
      if "T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T)" for T
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T \<Longrightarrow> \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T
 2. \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T \<Longrightarrow> \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T
[PROOF STEP]
show "?lhs \<Longrightarrow> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T \<Longrightarrow> \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T
[PROOF STEP]
by (meson \<section> imageI inj inj_on_eq_iff inj_on_subset that)
[PROOF STATE]
proof (state)
this:
\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T \<Longrightarrow> \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T

goal (1 subgoal):
 1. \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T \<Longrightarrow> \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T
[PROOF STEP]
show "?rhs \<Longrightarrow> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T \<Longrightarrow> \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T
[PROOF STEP]
using S inj inj_onD that
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> topspace X
inj_on f (topspace X)
\<lbrakk>inj_on ?f ?A; ?f ?x = ?f ?y; ?x \<in> ?A; ?y \<in> ?A\<rbrakk> \<Longrightarrow> ?x = ?y
T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T)

goal (1 subgoal):
 1. \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T \<Longrightarrow> \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T \<Longrightarrow> \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T) \<Longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> ?T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` ?T)

goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x \<in> ?T \<and> openin X ?T) = (?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T))
?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T) \<Longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> ?T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` ?T)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x \<in> ?T \<and> openin X ?T) = (?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T))
?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T) \<Longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> ?T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` ?T)

goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
by (auto simp flip: fim simp: all_subset_image)
[PROOF STATE]
proof (state)
this:
(\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> topspace X \<Longrightarrow> (\<forall>T. ?x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> ?x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f ?x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f ?x \<and> y \<in> f ` S \<and> y \<in> T))

goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
have *: "\<lbrakk>T = f ` S; \<And>x. x \<in> S \<Longrightarrow> P x \<longleftrightarrow> Q(f x)\<rbrakk> \<Longrightarrow> {y. y \<in> T \<and> Q y} = f ` {x \<in> S. P x}" for T S P Q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>T = f ` S; \<And>x. x \<in> S \<Longrightarrow> P x = Q (f x)\<rbrakk> \<Longrightarrow> {y \<in> T. Q y} = f ` {x \<in> S. P x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?T = f ` ?S; \<And>x. x \<in> ?S \<Longrightarrow> ?P x = ?Q (f x)\<rbrakk> \<Longrightarrow> {y \<in> ?T. ?Q y} = f ` {x \<in> ?S. ?P x}

goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
unfolding derived_set_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> topspace Y. \<forall>T. x \<in> T \<and> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> f ` S \<and> y \<in> T)} = f ` {x \<in> topspace X. \<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)}
[PROOF STEP]
by (rule *) (use fim iff openin_subset in force)+
[PROOF STATE]
proof (state)
this:
Y derived_set_of f ` S = f ` (X derived_set_of S)

goal:
No subgoals!
[PROOF STEP]
qed