case a0
ι : Type u_1
I✝ J : Box ι
x✝ y✝ : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : distortion I ≤ c
this : 0 ≤ ↑c * (upper I i - lower I i)
x : ι → ℝ
hx : x ∈ ↑Box.Icc I
y : ι → ℝ
hy : y ∈ ↑Box.Icc I
⊢ 0 ≤ upper I i - lower I i
ι : Type u_1
I✝ J : Box ι
x✝ y✝ : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : distortion I ≤ c
this : 0 ≤ ↑c * (upper I i - lower I i)
x : ι → ℝ
hx : x ∈ ↑Box.Icc I
y : ι → ℝ
hy : y ∈ ↑Box.Icc I
⊢ ↑(distortion I) * (upper I i - lower I i) ≤ ↑c * (upper I i - lower I i)
gcongr
no goals
case a0
ι : Type u_1
I✝ J : Box ι
x✝ y✝ : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : distortion I ≤ c
this : 0 ≤ ↑c * (upper I i - lower I i)
x : ι → ℝ
hx : x ∈ ↑Box.Icc I
y : ι → ℝ
hy : y ∈ ↑Box.Icc I
⊢ 0 ≤ upper I i - lower I i
exact sub_nonneg.2 (I.lower_le_upper i)