fixes #1123

Co-authored-by: Takafumi Saikawa <[email protected]>
Co-authored-by: Zachary Stone <[email protected]>

theories/ereal.v

@@ -533,15 +533,21 @@ Proof. by move=> A B AB; apply: ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed
 Lemma le_ereal_inf : {homo @ereal_inf R : A B / A `<=` B >-> B <= A}.
 Proof. by move=> A B AB; apply: lb_ereal_inf => x Bx; exact/ereal_inf_lb/AB. Qed.
 
-Lemma hasNub_ereal_sup (A : set (\bar R)) : ~ has_ubound A ->
-  A !=set0 -> ereal_sup A = +oo%E.
+Lemma hasNub_ereal_sup (A : set R) : ~ has_ubound A ->
+  A !=set0 -> ereal_sup (EFin @` A) = +oo%E.
 Proof.
 move=> hasNubA A0.
 apply/eqP; rewrite eq_le leey /= leNgt; apply: contra_notN hasNubA => Aoo.
-by exists (ereal_sup A); exact: ereal_sup_ub.
+exists (fine (ereal_sup (EFin @` A))) => x Ax.
+rewrite -lee_fin -(@fineK _ x%:E)// lee_fin fine_le//; last first.
+  by apply: ereal_sup_ub => /=; exists x.
+rewrite fin_numE// -ltey Aoo andbT.
+apply/negP => /eqP/ereal_sup_ninfty/(_ x%:E).
+have : (EFin @` A) x%:E by exists x.
+by move=> /[swap] /[apply].
 Qed.
 
-Lemma ereal_sup_EFin  (A : set R) :
+Lemma ereal_sup_EFin (A : set R) :
   has_ubound A -> A !=set0 -> ereal_sup (EFin @` A) = (sup A)%:E.
 Proof.
 move=> has_ubA A0; apply/eqP; rewrite eq_le; apply/andP; split.