-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem distortion_eq_of_sub_eq_div {I J : Box ι} {r : ℝ}
    (h : ∀ i, I.upper i - I.lower i = (J.upper i - J.lower i) / r) :
    distortion I = distortion J

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
⊢ 0 < r

Tactic:
by_contra hr

Result:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
hr : ¬0 < r
⊢ False

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
hr : ¬0 < r
this : I.upper i - I.lower i ≤ 0
⊢ False

Tactic:
exact this.not_lt (sub_pos.2 <| I.lower_lt_upper i)

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
⊢ (Finset.univ.sup fun i =>
      (Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    Finset.univ.sup fun i =>
      (Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i)

Tactic:
congr 1 with i

Result:
case e_f.h.a
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
⊢ ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))

Proof state:
case e_f.h.a
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
this : 0 < r
⊢ ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))

Tactic:
have hn0 := (map_ne_zero Real.nnabs).2 this.ne'

Result:
case e_f.h.a
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
this : 0 < r
hn0 : Real.nnabs r ≠ 0
⊢ ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))

Proof state:
case e_f.h.a
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
⊢ ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))

Tactic:
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)

Result:
case e_f.h.a
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
this : 0 < r
⊢ ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))

Proof state:
case e_f.h.a
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
this : 0 < r
hn0 : Real.nnabs r ≠ 0
⊢ ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))

Tactic:
simp_rw [NNReal.finset_sup_div, div_div_div_cancel_right₀ hn0]

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
hr : ¬0 < r
this : (J.upper i - J.lower i) / r ≤ 0
⊢ False

Tactic:
rw [← h] at this

Result:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
hr : ¬0 < r
this : I.upper i - I.lower i ≤ 0
⊢ False

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
⊢ I.distortion = J.distortion

Tactic:
simp only [distortion, nndist_pi_def, Real.nndist_eq', h, map_div₀]

Result:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
⊢ (Finset.univ.sup fun i =>
      (Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    Finset.univ.sup fun i =>
      (Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
hr : ¬0 < r
⊢ False

Tactic:
have := div_nonpos_of_nonneg_of_nonpos (sub_nonneg.2 <| J.lower_le_upper i) (not_lt.1 hr)

Result:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
hr : ¬0 < r
this : (J.upper i - J.lower i) / r ≤ 0
⊢ False