ENNReal.exists_enorm_sub_eps_le_biInf

lemma exists_enorm_sub_eps_le_biInf    {f : ι → E} {ε : ℝ≥0} (εpos : 0 < ε) (hs : s.Nonempty) :    ∃ x ∈ s, ‖f x‖ₑ - ε ≤ ⨅ z ∈ s, ‖f z‖ₑ := by  obtain ⟨i₀, mi₀⟩ := hs; set A := ⨅ z ∈ s, ‖f z‖ₑ  have glb : IsGLB ((‖f ·‖ₑ) '' s) A := isGLB_biInf  rw [isGLB_iff_le_iff] at glb  by_contra! h  specialize glb (A + ε)  have key : A + ε ∈ lowerBounds ((‖f ·‖ₑ) '' s) := fun i mi ↦ by    rw [mem_image] at mi; obtain ⟨x, mx, hx⟩ := mi    specialize h x mx; rw [hx] at h; exact (lt_tsub_iff_right.mp h).le  rw [← glb] at key  obtain ⟨B, eB⟩ : ∃ B : ℝ≥0, A = B := Option.ne_none_iff_exists'.mp (h i₀ mi₀).ne_top  rw [eB, ← ENNReal.coe_add, coe_le_coe, ← NNReal.coe_le_coe, NNReal.coe_add,    add_le_iff_nonpos_right] at key  rw [← NNReal.coe_pos] at εpos; linarith only [εpos, key]