F : Type ?u.1563197
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (↑f x) (↑0 x) ≤ nndist f 0
⊢ ↑f x ≤ nndist f 0
F : Type ?u.1563197
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
⊢ ↑f x ≤ nndist f 0
have key : nndist (f x) ((0 : α →ᵇ ℝ≥0) x) ≤ nndist f 0 := @dist_coe_le_dist α ℝ≥0 _ _ f 0 x
F : Type ?u.1563197
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (↑f x) 0 ≤ nndist f 0
⊢ ↑f x ≤ nndist f 0
F : Type ?u.1563197
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (↑f x) (↑0 x) ≤ nndist f 0
⊢ ↑f x ≤ nndist f 0
simp only [coe_zero, Pi.zero_apply] at key
no goals
F : Type ?u.1563197
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (↑f x) 0 ≤ nndist f 0
⊢ ↑f x ≤ nndist f 0
rwa [NNReal.nndist_zero_eq_val' (f x)] at key