ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
⊢ (Finset.sup Finset.univ fun i =>
      (Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    Finset.sup Finset.univ fun i =>
      (Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i)
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
⊢ distortion I = distortion J
simp only [distortion, nndist_pi_def, Real.nndist_eq', h, map_div₀]
case e_f.h.a
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
⊢ ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i))
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
⊢ (Finset.sup Finset.univ fun i =>
      (Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    Finset.sup Finset.univ fun i =>
      (Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i)
congr 1 with i
case e_f.h.a
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
this : 0 < r
⊢ ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i))
case e_f.h.a
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
⊢ ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i))
have : 0 < r := by
  by_contra hr
  have := div_nonpos_of_nonneg_of_nonpos (sub_nonneg.2 <| J.lower_le_upper i) (not_lt.1 hr)
  rw [← h] at this
  exact this.not_lt (sub_pos.2 <| I.lower_lt_upper i)
case e_f.h.a
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
this : 0 < r
hn0 : ↑Real.nnabs r ≠ 0
⊢ ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i))
case e_f.h.a
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
this : 0 < r
⊢ ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i))
have hn0 := (map_ne_zero Real.nnabs).2 this.ne'
no goals
case e_f.h.a
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
this : 0 < r
hn0 : ↑Real.nnabs r ≠ 0
⊢ ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i))
simp_rw [NNReal.finset_sup_div, div_div_div_cancel_right _ hn0]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
hr : ¬0 < r
⊢ False
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
⊢ 0 < r
by_contra hr
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
hr : ¬0 < r
this : (upper J i - lower J i) / r ≤ 0
⊢ False
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
hr : ¬0 < r
⊢ False
have := div_nonpos_of_nonneg_of_nonpos (sub_nonneg.2 <| J.lower_le_upper i) (not_lt.1 hr)
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
hr : ¬0 < r
this : upper I i - lower I i ≤ 0
⊢ False
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
hr : ¬0 < r
this : (upper J i - lower J i) / r ≤ 0
⊢ False
rw [← h] at this
no goals
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
hr : ¬0 < r
this : upper I i - lower I i ≤ 0
⊢ False
exact this.not_lt (sub_pos.2 <| I.lower_lt_upper i)