-- Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.lean
theorem exists_taggedPartition_isHenstock_isSubordinate_homothetic (I : Box ι)
    (r : (ι → ℝ) → Ioi (0 : ℝ)) :
    ∃ π : TaggedPrepartition I, π.IsPartition ∧ π.IsHenstock ∧ π.IsSubordinate r ∧
      (∀ J ∈ π, ∃ m : ℕ, ∀ i, (J :).upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) ∧
        π.distortion = I.distortion

Proof state:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
⊢ ∀ J ≤ I,
    ∀ (m : ℕ),
      z ∈ Box.Icc J →
        Box.Icc J ⊆ Box.Icc I ∩ closedBall z ↑(r z) →
          (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) →
            ∃ π,
              π.IsPartition ∧
                π.IsHenstock ∧
                  π.IsSubordinate r ∧
                    (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧
                      π.distortion = J.distortion

Tactic:
intro J _ n Hmem HIcc Hsub

Result:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ Box.Icc J
HIcc : Box.Icc J ⊆ Box.Icc I ∩ closedBall z ↑(r z)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ n
⊢ ∃ π,
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧
            π.distortion = J.distortion

Proof state:
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
a✝ : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : Box ι → Box ι → ℕ
hn : ∀ J' ∈ splitCenter J, ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ n J' J
hP : ((splitCenter J).biUnionTagged πi).IsPartition
J' : Box ι
hJ' : J' ∈ (splitCenter J).biUnionTagged πi
J₁ : Box ι
h₁ : J₁ ∈ splitCenter J
h₂ : J' ∈ πi J₁
⊢ ∃ n, ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ n

Tactic:
refine ⟨n J₁ J' + 1, fun i => ?_⟩

Result:
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
a✝ : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : Box ι → Box ι → ℕ
hn : ∀ J' ∈ splitCenter J, ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ n J' J
hP : ((splitCenter J).biUnionTagged πi).IsPartition
J' : Box ι
hJ' : J' ∈ (splitCenter J).biUnionTagged πi
J₁ : Box ι
h₁ : J₁ ∈ splitCenter J
h₂ : J' ∈ πi J₁
i : ι
⊢ J'.upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ (n J₁ J' + 1)

Proof state:
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
a✝ : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : Box ι → Box ι → ℕ
hn : ∀ J' ∈ splitCenter J, ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ n J' J
hP : ((splitCenter J).biUnionTagged πi).IsPartition
J' : Box ι
hJ' : J' ∈ (splitCenter J).biUnionTagged πi
J₁ : Box ι
h₁ : J₁ ∈ splitCenter J
h₂ : J' ∈ πi J₁
i : ι
⊢ J'.upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ (n J₁ J' + 1)

Tactic:
simp only [hn J₁ h₁ J' h₂, upper_sub_lower_of_mem_splitCenter h₁, pow_succ', div_div]

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
a✝ : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : Box ι → Box ι → ℕ
hn : ∀ J' ∈ splitCenter J, ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ n J' J
hP : ((splitCenter J).biUnionTagged πi).IsPartition
⊢ ∃ π,
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧
            π.distortion = J.distortion

Tactic:
have hsub : ∀ J' ∈ (splitCenter J).biUnionTagged πi, ∃ n : ℕ, ∀ i,
    (J' :).upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ n := by
  intro J' hJ'
  rcases (splitCenter J).mem_biUnionTagged.1 hJ' with ⟨J₁, h₁, h₂⟩
  refine ⟨n J₁ J' + 1, fun i => ?_⟩
  simp only [hn J₁ h₁ J' h₂, upper_sub_lower_of_mem_splitCenter h₁, pow_succ', div_div]

Result:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
a✝ : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : Box ι → Box ι → ℕ
hn : ∀ J' ∈ splitCenter J, ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ n J' J
hP : ((splitCenter J).biUnionTagged πi).IsPartition
hsub :
  ∀ J' ∈ (splitCenter J).biUnionTagged πi, ∃ n, ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ n
⊢ ∃ π,
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧
            π.distortion = J.distortion

Proof state:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ Box.Icc J
HIcc : Box.Icc J ⊆ Box.Icc I ∧ Box.Icc J ⊆ closedBall z ↑(r z)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ n
⊢ ∀ J_1 ∈ TaggedPrepartition.single J J ⋯ z Hmem,
    ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m

Tactic:
simp only [TaggedPrepartition.mem_single, forall_eq]

Result:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ Box.Icc J
HIcc : Box.Icc J ⊆ Box.Icc I ∧ Box.Icc J ⊆ closedBall z ↑(r z)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ n
⊢ ∃ m, ∀ (i : ι), J.upper i - J.lower i = (J.upper i - J.lower i) / 2 ^ m