[STATEMENT]
lemma stc_part_Ex:
  assumes "x \<in> HFinite" 
  shows "\<exists>t \<in> SComplex. x \<approx> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
let ?t = "HComplex (st (hRe x)) (st (hIm x))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
have "?t \<in> SComplex"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex
[PROOF STEP]
using HFinite_hIm HFinite_hRe Reals_eq_Standard assms st_SReal
[PROOF STATE]
proof (prove)
using this:
?x \<in> HFinite \<Longrightarrow> hIm ?x \<in> HFinite
?x \<in> HFinite \<Longrightarrow> hRe ?x \<in> HFinite
\<real> = Standard
x \<in> HFinite
?x \<in> HFinite \<Longrightarrow> st ?x \<in> \<real>

goal (1 subgoal):
 1. HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex

goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex

goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
have "x \<approx> ?t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<approx> HComplex (st (hRe x)) (st (hIm x))
[PROOF STEP]
by (simp add: HFinite_hIm HFinite_hRe assms hcomplex_approx_iff st_HFinite st_eq_approx)
[PROOF STATE]
proof (state)
this:
x \<approx> HComplex (st (hRe x)) (st (hIm x))

goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex
x \<approx> HComplex (st (hRe x)) (st (hIm x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex
x \<approx> HComplex (st (hRe x)) (st (hIm x))

goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>SComplex. x \<approx> t

goal:
No subgoals!
[PROOF STEP]
qed