ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
A : lower I i - upper I i < 0
⊢ dist I.lower I.upper ≤ ↑(distortion I) * (upper I i - lower I i)
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
⊢ dist I.lower I.upper ≤ ↑(distortion I) * (upper I i - lower I i)
have A : I.lower i - I.upper i < 0 := sub_neg.2 (I.lower_lt_upper i)
no goals
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
A : lower I i - upper I i < 0
⊢ dist I.lower I.upper ≤ ↑(distortion I) * (upper I i - lower I i)
simpa only [← NNReal.coe_le_coe, ← dist_nndist, NNReal.coe_mul, Real.dist_eq, abs_of_neg A,
  neg_sub] using I.nndist_le_distortion_mul i