awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
e_p :
  Eq.{u_1 + 1} (α := Prepartition I → Prop) (fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion)
    fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion
⊢ ⋯.choose (p := fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion) =
    ⋯.choose (p := fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion)

Tactic:
congr 1
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
e_p e_p₁ :
  Eq.{u_1 + 1} (α := Prepartition I → Prop) (fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion)
    fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion
⊢ Eq.{u_1 + 1} (α := Prepartition I → Prop) (fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion)
    fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion

Tactic:
rw [h]
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
h : π.IsPartition
rw : π.compl.iUnion = ∅
rw₁ : (↑I : Set (ι → ℝ)) \ π.iUnion = ∅
rw₂ : (↑I : Set (ι → ℝ)) \ (↑I : Set (ι → ℝ)) = ∅
rw₃ rw₄ : Eq.{u_1 + 1} (α := Set (ι → ℝ)) ∅ ∅
⊢ π.compl = ⊥

Tactic:
rw [← iUnion_eq_empty, iUnion_compl, h.iUnion_eq, diff_self]

Premises used: BoxIntegral.Prepartition.IsPartition.iUnion_eq, BoxIntegral.Prepartition.iUnion_eq_empty, BoxIntegral.Prepartition.iUnion_compl, Set.diff_self
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
⊢ Eq.{u_1 + 1} (α := Prepartition I) (compl ⊤) ⊥

Tactic:
(isPartitionTop I).compl_eq_bot

Premises used: BoxIntegral.Prepartition.IsPartition.compl_eq_bot, BoxIntegral.Prepartition.isPartitionTop
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I_1 J I : Box ι
⊢ ∀ J ∈ Finset.map I.splitCenterBoxEmb Finset.univ, J ≤ I

Tactic:
simp [I.splitCenterBox_le]

Premises used: BoxIntegral.Box.splitCenterBox_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I_1 J I : Box ι
rw :
  Set.Pairwise (α := Box ι) (range (ι := Set ι) (⇑I.splitCenterBoxEmb : (a : Set ι) → Box ι))
    (Function.onFun Disjoint Box.toSet)
⊢ (↑(Finset.map I.splitCenterBoxEmb Finset.univ) : Set (Box ι)).Pairwise (Function.onFun Disjoint Box.toSet)

Tactic:
rw [Finset.coe_map, Finset.coe_univ, image_univ]

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_map
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I_1 J I : Box ι
s t : Set ι
Hne :
  Ne (α := Box ι) ((I.splitCenterBoxEmb : (a : Set ι) → Box ι) s : Box ι)
    ((I.splitCenterBoxEmb : (a : Set ι) → Box ι) t : Box ι)
⊢ Function.onFun.{u_1 + 1, u_1 + 1, 1} (α := Box ι) Disjoint Box.toSet ((I.splitCenterBoxEmb : (a : Set ι) → Box ι) s)
    ((I.splitCenterBoxEmb : (a : Set ι) → Box ι) t)

Tactic:
I.disjoint_splitCenterBox (mt (congr_arg _) Hne)

Premises used: BoxIntegral.Box.disjoint_splitCenterBox, BoxIntegral.Box.splitCenterBox, mt, congr_arg
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I_1 J I : Box ι
s t : Set ι
Hne :
  Ne (α := Box ι) ((I.splitCenterBoxEmb : (a : Set ι) → Box ι) s : Box ι)
    ((I.splitCenterBoxEmb : (a : Set ι) → Box ι) t : Box ι)
⊢ Function.onFun.{u_1 + 1, u_1 + 1, 1} (α := Box ι) Disjoint Box.toSet ((I.splitCenterBoxEmb : (a : Set ι) → Box ι) s)
    ((I.splitCenterBoxEmb : (a : Set ι) → Box ι) t)

Tactic:
exact I.disjoint_splitCenterBox (mt (congr_arg _) Hne)

Premises used: BoxIntegral.Box.disjoint_splitCenterBox, mt, congr_arg
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
⊢ J ∈ splitCenter I ↔ ∃ (s : Set ι), I.splitCenterBox s = J

Tactic:
simp [splitCenter]

Premises used: BoxIntegral.Prepartition.splitCenter
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
x : ι → ℝ
hx : x ∈ I
⊢ ∃ J ∈ splitCenter I, x ∈ J

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
h : J ∈ splitCenter I
i : ι
⊢ J.upper i - J.lower i = (I.upper i - I.lower i) / 2

Tactic:
let ⟨s, hs⟩ := mem_splitCenter.1 h
  hs ▸ I.upper_sub_lower_splitCenterBox s i

Premises used: BoxIntegral.Box.upper_sub_lower_splitCenterBox, HSub.hSub, _private.0.BoxIntegral.Prepartition.upper_sub_lower_of_mem_splitCenter.match_1, BoxIntegral.Box.upper, Eq.rec, HDiv.hDiv, BoxIntegral.Prepartition.mem_splitCenter, BoxIntegral.Box.lower, Iff.mp, OfNat.ofNat, Eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
⊢ p I

Tactic:
subbox_induction_on' I (fun J hle hs => H_ind J hle fun J' h' => ?_) H_nhds

Premises used: BoxIntegral.Box.subbox_induction_on'
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
refine :
  ∀ (J : Box ι) (hle : J ≤ I) (hs : ∀ (s : Set ι), p (J.splitCenterBox s)) (J' : Box ι) (h' : J' ∈ splitCenter J), p J'
⊢ p I

Tactic:
refine subbox_induction_on' I (fun J hle hs => H_ind J hle fun J' h' => ?_) H_nhds
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (J.splitCenterBox s)
J' : Box ι
h' : J' ∈ splitCenter J
rcases : ∀ (s : Set ι) (h' : J.splitCenterBox s ∈ splitCenter J), p (J.splitCenterBox s)
⊢ p J'

Tactic:
rcases mem_splitCenter.1 h' with ⟨s, rfl⟩

Premises used: BoxIntegral.Prepartition.mem_splitCenter, Iff.mp, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (J.splitCenterBox s)
s : Set ι
h' : J.splitCenterBox s ∈ splitCenter J
⊢ p (J.splitCenterBox s)

Tactic:
hs s
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (J.splitCenterBox s)
s : Set ι
h' : J.splitCenterBox s ∈ splitCenter J
⊢ p (J.splitCenterBox s)

Tactic:
exact hs s
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
⊢ ∃ (π : TaggedPrepartition I),
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J ∈ π, ∃ (m : ℕ), ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
            π.distortion = I.distortion

Tactic:
subbox_induction_on I (fun J _ hJ => ?_) fun z _ => ?_

Premises used: BoxIntegral.Box.subbox_induction_on
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
refine_1 :
  ∀ J ≤ I,
    ∀
      (hJ :
        ∀ J' ∈ splitCenter J,
          ∃ (π : TaggedPrepartition J'),
            π.IsPartition ∧
              π.IsHenstock ∧
                π.IsSubordinate r ∧
                  (∀ J ∈ π,
                      ∃ (m : ℕ),
                        ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
                    π.distortion = J'.distortion),
      ∃ (π : TaggedPrepartition J),
        π.IsPartition ∧
          π.IsHenstock ∧
            π.IsSubordinate r ∧
              (∀ J_1 ∈ π,
                  ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
                π.distortion = J.distortion
refine_2 :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) →
                  ∃ (π : TaggedPrepartition J),
                    π.IsPartition ∧
                      π.IsHenstock ∧
                        π.IsSubordinate r ∧
                          (∀ J_1 ∈ π,
                              ∃ (m : ℕ),
                                ∀ (i : ι),
                                  J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
                            π.distortion = J.distortion
⊢ ∃ (π : TaggedPrepartition I),
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J ∈ π, ∃ (m : ℕ), ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
            π.distortion = I.distortion

Tactic:
refine subbox_induction_on I (fun J _ hJ => ?_) fun z _ => ?_
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
J : Box ι
h : J ≤ I
hJ :
  ∀ J' ∈ splitCenter J,
    ∃ (π : TaggedPrepartition J'),
      π.IsPartition ∧
        π.IsHenstock ∧
          π.IsSubordinate r ∧
            (∀ J ∈ π,
                ∃ (m : ℕ), ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
              π.distortion = J'.distortion
refine_1 :
  ∀ (π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)
    (Hn :
      ∀ J' ∈ splitCenter J,
        ∀ J ∈ πi J', ∃ (m : ℕ), ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 2 m),
    (∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion) →
      ∃ (π : TaggedPrepartition J),
        π.IsPartition ∧
          π.IsHenstock ∧
            π.IsSubordinate r ∧
              (∀ J_1 ∈ π,
                  ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
                π.distortion = J.distortion
⊢ ∃ (π : TaggedPrepartition J),
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J_1 ∈ π,
              ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
            π.distortion = J.distortion

Tactic:
choose! πi hP hHen hr Hn _ using hJ
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
J : Box ι
h : 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
Hn :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∃ (m : ℕ), ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 2 m
h_1 : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
refine_1 :
  ∀ (n : (J' J : Box ι) → ℕ)
    (hn :
      ∀ J' ∈ splitCenter J,
        ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 2 (n J' J)),
    ∃ (π : TaggedPrepartition J),
      π.IsPartition ∧
        π.IsHenstock ∧
          π.IsSubordinate r ∧
            (∀ J_1 ∈ π,
                ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
              π.distortion = J.distortion
⊢ ∃ (π : TaggedPrepartition J),
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J_1 ∈ π,
              ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
            π.distortion = J.distortion

Tactic:
choose! n hn using Hn
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
J : Box ι
h : 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
h_1 : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : (J' J : Box ι) → ℕ
hn :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 2 (n J' J)
⊢ ((splitCenter J).biUnionTagged πi).IsPartition

Tactic:
have hP : ((splitCenter J).biUnionTagged πi).IsPartition :=
      (isPartition_splitCenter _).biUnionTagged hP
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
J : Box ι
h : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP_1 : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
h_1 : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : (J' J : Box ι) → ℕ
hn :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 2 (n J' J)
hP : ((splitCenter J).biUnionTagged πi).IsPartition
J' : Box ι
hJ' : J' ∈ (splitCenter J).biUnionTagged πi
rcases :
  ∀ (J₁ : Box ι) (h₁ : J₁ ∈ splitCenter J) (h₂ : J' ∈ πi J₁),
    ∃ (n : ℕ), ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 n
⊢ ∃ (n : ℕ), ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 n

Tactic:
rcases (splitCenter J).mem_biUnionTagged.1 hJ' with ⟨J₁, h₁, h₂⟩

Premises used: BoxIntegral.Prepartition.splitCenter, Iff.mp, BoxIntegral.Prepartition.mem_biUnionTagged
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
J : Box ι
h : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP_1 : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
h_1 : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : (J' J : Box ι) → ℕ
hn :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 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) / HPow.hPow (α := ℝ) 2 n

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

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
J : Box ι
h : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP_1 : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
h_1 : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : (J' J : Box ι) → ℕ
hn :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 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₁
refine : ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 (n J₁ J' + 1)
⊢ ∃ (n : ℕ), ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 n

Tactic:
refine ⟨n J₁ J' + 1, fun i => ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
J : Box ι
h : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP_1 : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
h_1 : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : (J' J : Box ι) → ℕ
hn :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 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) / HPow.hPow (α := ℝ) 2 (n J₁ J' + 1)

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

Premises used: BoxIntegral.Prepartition.upper_sub_lower_of_mem_splitCenter, div_div, pow_succ'
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
J : Box ι
h : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP_1 : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
h_1 : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : (J' J : Box ι) → ℕ
hn :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 2 (n J' J)
hP : ((splitCenter J).biUnionTagged πi).IsPartition
⊢ ∀ J' ∈ (splitCenter J).biUnionTagged πi,
    ∃ (n : ℕ), ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 n

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]
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
J : Box ι
h : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP_1 : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
h_1 : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : (J' J : Box ι) → ℕ
hn :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 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) / HPow.hPow (α := ℝ) 2 n
⊢ ∃ (π : TaggedPrepartition J),
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J_1 ∈ π,
              ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
            π.distortion = J.distortion

Tactic:
⟨_, hP, isHenstock_biUnionTagged.2 hHen, isSubordinate_biUnionTagged.2 hr, hsub, ?_⟩

Premises used: Iff.mpr, BoxIntegral.TaggedPrepartition.isHenstock_biUnionTagged, And.intro, Exists.intro, BoxIntegral.TaggedPrepartition.isSubordinate_biUnionTagged
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
J : Box ι
h : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP_1 : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
h_1 : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : (J' J : Box ι) → ℕ
hn :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 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) / HPow.hPow (α := ℝ) 2 n
refine_1 : ((splitCenter J).biUnionTagged πi).distortion = J.distortion
⊢ ∃ (π : TaggedPrepartition J),
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J_1 ∈ π,
              ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m) ∧
            π.distortion = J.distortion

Tactic:
refine ⟨_, hP, isHenstock_biUnionTagged.2 hHen, isSubordinate_biUnionTagged.2 hr, hsub, ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
J : Box ι
h : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP_1 : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
h_1 : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : (J' J : Box ι) → ℕ
hn :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 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) / HPow.hPow (α := ℝ) 2 n
⊢ ((splitCenter J).biUnionTagged πi).distortion = J.distortion

Tactic:
TaggedPrepartition.distortion_of_const _ hP.nonempty_boxes fun J' h' => ?_

Premises used: BoxIntegral.TaggedPrepartition.distortion_of_const, BoxIntegral.Prepartition.IsPartition.nonempty_boxes