[STATEMENT]
lemma Inf_countable_INF:
  assumes "A \<noteq> {}" shows "\<exists>f::nat \<Rightarrow> ereal. decseq f \<and> range f \<subseteq> A \<and> Inf A = (INF i. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. decseq f \<and> range f \<subseteq> A \<and> Inf A = Inf (range f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. decseq f \<and> range f \<subseteq> A \<and> Inf A = Inf (range f)
[PROOF STEP]
obtain f where "incseq f" "range f \<subseteq> uminus`A" "Sup (uminus`A) = (SUP i. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>incseq f; range f \<subseteq> uminus ` A; Sup (uminus ` A) = Sup (range f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Sup_countable_SUP[of "uminus ` A"] \<open>A \<noteq> {}\<close>
[PROOF STATE]
proof (prove)
using this:
uminus ` A \<noteq> {} \<Longrightarrow> \<exists>f. incseq f \<and> range f \<subseteq> uminus ` A \<and> Sup (uminus ` A) = Sup (range f)
A \<noteq> {}

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>incseq f; range f \<subseteq> uminus ` A; Sup (uminus ` A) = Sup (range f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
incseq f
range f \<subseteq> uminus ` A
Sup (uminus ` A) = Sup (range f)

goal (1 subgoal):
 1. \<exists>f. decseq f \<and> range f \<subseteq> A \<and> Inf A = Inf (range f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
incseq f
range f \<subseteq> uminus ` A
Sup (uminus ` A) = Sup (range f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
incseq f
range f \<subseteq> uminus ` A
Sup (uminus ` A) = Sup (range f)

goal (1 subgoal):
 1. \<exists>f. decseq f \<and> range f \<subseteq> A \<and> Inf A = Inf (range f)
[PROOF STEP]
by (intro exI[of _ "\<lambda>x. - f x"])
       (auto simp: ereal_Sup_uminus_image_eq ereal_INF_uminus_eq eq_commute[of "- _"])
[PROOF STATE]
proof (state)
this:
\<exists>f. decseq f \<and> range f \<subseteq> A \<and> Inf A = Inf (range f)

goal:
No subgoals!
[PROOF STEP]
qed