chore(order/conditionally_complete_lattice): drop an unneeded nonempty assumption (#10132)

Author: urkud

src/order/conditionally_complete_lattice.lean

@@ -516,18 +516,19 @@ theorem cinfi_eq_of_forall_ge_of_forall_gt_exists_lt [nonempty ι] {f : ι → 
 
 /-- Nested intervals lemma: if `f` is a monotone sequence, `g` is an antitone sequence, and
 `f n ≤ g n` for all `n`, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
-lemma monotone.csupr_mem_Inter_Icc_of_antitone [nonempty β] [semilattice_sup β]
+lemma monotone.csupr_mem_Inter_Icc_of_antitone [semilattice_sup β]
   {f g : β → α} (hf : monotone f) (hg : antitone g) (h : f ≤ g) :
   (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) :=
 begin
-  inhabit β,
-  refine mem_Inter.2 (λ n, ⟨le_csupr ⟨g $ default β, forall_range_iff.2 $ λ m, _⟩ _,
-    csupr_le $ λ m, _⟩); exact hf.forall_le_of_antitone hg h _ _
+  refine mem_Inter.2 (λ n, _),
+  haveI : nonempty β := ⟨n⟩,
+  have : ∀ m, f m ≤ g n := λ m, hf.forall_le_of_antitone hg h m n,
+  exact ⟨le_csupr ⟨g $ n, forall_range_iff.2 this⟩ _, csupr_le this⟩
 end
 
 /-- Nested intervals lemma: if `[f n, g n]` is an antitone sequence of nonempty
 closed intervals, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
-lemma csupr_mem_Inter_Icc_of_antitone_Icc [nonempty β] [semilattice_sup β]
+lemma csupr_mem_Inter_Icc_of_antitone_Icc [semilattice_sup β]
   {f g : β → α} (h : antitone (λ n, Icc (f n) (g n))) (h' : ∀ n, f n ≤ g n) :
   (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) :=
 monotone.csupr_mem_Inter_Icc_of_antitone (λ m n hmn, ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).1)