no goals
α : Type u_1
β : Type ?u.377356
γ : Type ?u.377359
ι : Type ?u.377362
inst✝ : DenselyNormedField α
r₁ r₂ : ℝ≥0
h : r₁ < r₂
⊢ ∃ x, r₁ < ‖x‖₊ ∧ ‖x‖₊ < r₂
exact_mod_cast exists_lt_norm_lt α r₁.prop h