awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∀ (J' : Box ι) (h' : J' ∈ (splitCenter J).biUnionTagged πi), J'.distortion = J.distortion
⊢ ((splitCenter J).biUnionTagged πi).distortion = J.distortion

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

Premises used: BoxIntegral.TaggedPrepartition.distortion_of_const, BoxIntegral.Prepartition.IsPartition.nonempty_boxes
-- 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
J' : Box ι
h' : J' ∈ (splitCenter J).biUnionTagged πi
refine_1 :
  ∀ (n : ℕ) (hn : ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 n),
    J'.distortion = J.distortion
⊢ J'.distortion = J.distortion

Tactic:
rcases hsub J' h' with ⟨n, 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_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_1 : (J' J : Box ι) → ℕ
hn_1 :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 2 (n_1 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
J' : Box ι
h' : J' ∈ (splitCenter J).biUnionTagged πi
n : ℕ
hn : ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 n
⊢ J'.distortion = J.distortion

Tactic:
Box.distortion_eq_of_sub_eq_div hn

Premises used: BoxIntegral.Box.distortion_eq_of_sub_eq_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_1 : (J' J : Box ι) → ℕ
hn_1 :
  ∀ J' ∈ splitCenter J,
    ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / HPow.hPow (α := ℝ) 2 (n_1 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
J' : Box ι
h' : J' ∈ (splitCenter J).biUnionTagged πi
n : ℕ
hn : ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 n
⊢ J'.distortion = J.distortion

Tactic:
exact Box.distortion_eq_of_sub_eq_div hn

Premises used: BoxIntegral.Box.distortion_eq_of_sub_eq_div
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
z : ι → ℝ
h : 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

Tactic:
⟨Box.Icc I ∩ closedBall z (r z),
      inter_mem_nhdsWithin _ (closedBall_mem_nhds _ (r z).coe_prop), ?_⟩

Premises used: Subtype.coe_prop, inter_mem_nhdsWithin, Metric.closedBall_mem_nhds, BoxIntegral.Box.Icc, Inter.inter, And.intro, Exists.intro, Metric.closedBall, Subtype.val, DFunLike.coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
z : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z
refine_2 :
  ∀ J ≤ I,
    ∀ (m : ℕ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
        Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
            ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ closedBall z (↑(r z) : ℝ) : Set (ι → ℝ)) →
          (∀ (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
⊢ ∃ 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

Tactic:
refine ⟨Box.Icc I ∩ closedBall z (r z),
      inter_mem_nhdsWithin _ (closedBall_mem_nhds _ (r z).coe_prop), ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
z : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z
J : Box ι
refine_2 :
  J ≤ I →
    ∀ (m : ℕ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
        Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
            ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ closedBall z (↑(r z) : ℝ) : Set (ι → ℝ)) →
          (∀ (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
⊢ J ≤ I →
    ∀ (m : ℕ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
        Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
            ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ closedBall z (↑(r z) : ℝ) : Set (ι → ℝ)) →
          (∀ (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

Tactic:
_
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
z : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z
J : Box ι
h_1 : J ≤ I
n : ℕ
Hmem : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z
HIcc :
  Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
    ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ closedBall z (↑(r z) : ℝ) : Set (ι → ℝ))
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 n
⊢ Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) ∧
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall z (↑(r z) : ℝ)

Tactic:
rw [Set.subset_inter_iff] at HIcc

Premises used: Set.subset_inter_iff
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
z : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z
J : Box ι
h_1 : J ≤ I
n : ℕ
Hmem : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z
HIcc :
  Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
    ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ closedBall z (↑(r z) : ℝ) : Set (ι → ℝ))
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 n
HIcc₁ :
  Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) ∧
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall z (↑(r z) : ℝ)
⊢ ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 n

Tactic:
rw [Set.subset_inter_iff] at HIcc

Premises used: Set.subset_inter_iff
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
z : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z
J : Box ι
h_1 : J ≤ I
n : ℕ
Hmem : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z
HIcc :
  Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) ∧
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall z (↑(r z) : ℝ)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.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:
⟨single _ _ le_rfl _ Hmem, isPartition_single _, isHenstock_single _,
      (isSubordinate_single _ _).2 HIcc.2, ?_, distortion_single _ _⟩

Premises used: Iff.mpr, le_rfl, BoxIntegral.TaggedPrepartition.isHenstock_single, BoxIntegral.TaggedPrepartition.isSubordinate_single, BoxIntegral.TaggedPrepartition.single, And.right, And.intro, Exists.intro, BoxIntegral.TaggedPrepartition.isPartition_single, BoxIntegral.TaggedPrepartition.distortion_single
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
z : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z
J : Box ι
h_1 : J ≤ I
n : ℕ
Hmem : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z
HIcc :
  Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) ∧
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall z (↑(r z) : ℝ)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 n
refine_2 :
  ∀ J_1 ∈ TaggedPrepartition.single J J ⋯ z Hmem,
    ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.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

Tactic:
refine ⟨single _ _ le_rfl _ Hmem, isPartition_single _, isHenstock_single _,
      (isSubordinate_single _ _).2 HIcc.2, ?_, distortion_single _ _⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
z : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z
J : Box ι
h_1 : J ≤ I
n : ℕ
Hmem : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z
HIcc :
  Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) ∧
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall z (↑(r z) : ℝ)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 n
refine_2 : ∃ (m : ℕ), ∀ (i : ι), J.upper i - J.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m
⊢ ∀ J_1 ∈ TaggedPrepartition.single J J ⋯ z Hmem,
    ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m

Tactic:
simp only [TaggedPrepartition.mem_single, forall_eq]

Premises used: forall_eq, BoxIntegral.TaggedPrepartition.mem_single
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
z : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z
J : Box ι
h_1 : J ≤ I
n : ℕ
Hmem : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z
HIcc :
  Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) ∧
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall z (↑(r z) : ℝ)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 n
⊢ ∃ (m : ℕ), ∀ (i : ι), J.upper i - J.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m

Tactic:
⟨0, fun i => ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
z : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z
J : Box ι
h_1 : J ≤ I
n : ℕ
Hmem : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z
HIcc :
  Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) ∧
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall z (↑(r z) : ℝ)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 n
refine_2 : ∀ (i : ι), J.upper i - J.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) (β := ℕ) 2 0
⊢ ∃ (m : ℕ), ∀ (i : ι), J.upper i - J.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m

Tactic:
refine ⟨0, fun i => ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Ioi 0) : Type)
z : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z
J : Box ι
h_1 : J ≤ I
n : ℕ
Hmem : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z
HIcc :
  Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) ∧
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall z (↑(r z) : ℝ)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 n
i : ι
⊢ J.upper i - J.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) (β := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : Prepartition I
⊢ ∀ (J : Box ι),
    ∃ (π : 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:
have := fun J => Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic J r
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : Prepartition I
this :
  ∀ (J : Box ι),
    ∃ (π : 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
choose! :
  ∀ (πi : (J : Box ι) → TaggedPrepartition J) (πip : ∀ (J : Box ι), (πi J).IsPartition)
    (πiH : ∀ (J : Box ι), (πi J).IsHenstock) (πir : ∀ (J : Box ι), (πi J).IsSubordinate r),
    (∀ (J J_1 : Box ι),
        J_1 ∈ πi J →
          ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m) →
      ∀ (πid : ∀ (J : Box ι), (πi J).distortion = J.distortion),
        ∃ (π' : TaggedPrepartition I),
          π'.toPrepartition ≤ π ∧
            π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion
⊢ ∃ (π' : TaggedPrepartition I),
    π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion

Tactic:
choose! πi πip πiH πir _ πid using this
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), (πi J).IsPartition
πiH : ∀ (J : Box ι), (πi J).IsHenstock
πir : ∀ (J : Box ι), (πi J).IsSubordinate r
h :
  ∀ (J J_1 : Box ι),
    J_1 ∈ πi J → ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m
πid : ∀ (J : Box ι), (πi J).distortion = J.distortion
⊢ ∃ (π' : TaggedPrepartition I),
    π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion

Tactic:
⟨π.biUnionTagged πi, biUnion_le _ _, isHenstock_biUnionTagged.2 fun J _ => πiH J,
    isSubordinate_biUnionTagged.2 fun J _ => πir J, ?_, π.iUnion_biUnion_partition fun J _ => πip J⟩

Premises used: Iff.mpr, BoxIntegral.Prepartition.biUnion_le, BoxIntegral.TaggedPrepartition.isHenstock_biUnionTagged, And.intro, Exists.intro, BoxIntegral.TaggedPrepartition.isSubordinate_biUnionTagged, BoxIntegral.Prepartition.biUnionTagged, BoxIntegral.Prepartition.iUnion_biUnion_partition
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), (πi J).IsPartition
πiH : ∀ (J : Box ι), (πi J).IsHenstock
πir : ∀ (J : Box ι), (πi J).IsSubordinate r
h :
  ∀ (J J_1 : Box ι),
    J_1 ∈ πi J → ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m
πid : ∀ (J : Box ι), (πi J).distortion = J.distortion
refine : (π.biUnionTagged πi).distortion = π.distortion
⊢ ∃ (π' : TaggedPrepartition I),
    π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion

Tactic:
refine ⟨π.biUnionTagged πi, biUnion_le _ _, isHenstock_biUnionTagged.2 fun J _ => πiH J,
    isSubordinate_biUnionTagged.2 fun J _ => πir J, ?_, π.iUnion_biUnion_partition fun J _ => πip J⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), (πi J).IsPartition
πiH : ∀ (J : Box ι), (πi J).IsHenstock
πir : ∀ (J : Box ι), (πi J).IsSubordinate r
h :
  ∀ (J J_1 : Box ι),
    J_1 ∈ πi J → ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m
πid : ∀ (J : Box ι), (πi J).distortion = J.distortion
rw : (π.boxes.sup fun (J : Box ι) ↦ (πi J).distortion) = π.distortion
⊢ (π.biUnionTagged πi).distortion = π.distortion

Tactic:
rw [distortion_biUnionTagged]

Premises used: BoxIntegral.Prepartition.distortion_biUnionTagged
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), (πi J).IsPartition
πiH : ∀ (J : Box ι), (πi J).IsHenstock
πir : ∀ (J : Box ι), (πi J).IsSubordinate r
h :
  ∀ (J J_1 : Box ι),
    J_1 ∈ πi J → ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m
πid : ∀ (J : Box ι), (πi J).distortion = J.distortion
⊢ (π.boxes.sup fun (J : Box ι) ↦ (πi J).distortion) = π.distortion

Tactic:
sup_congr rfl fun J _ => πid J

Premises used: BoxIntegral.Prepartition.distortion, Finset.sup_congr, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), (πi J).IsPartition
πiH : ∀ (J : Box ι), (πi J).IsHenstock
πir : ∀ (J : Box ι), (πi J).IsSubordinate r
h :
  ∀ (J J_1 : Box ι),
    J_1 ∈ πi J → ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m
πid : ∀ (J : Box ι), (πi J).distortion = J.distortion
⊢ (π.boxes.sup fun (J : Box ι) ↦ (πi J).distortion) = π.distortion

Tactic:
exact sup_congr rfl fun J _ => πid J

Premises used: Finset.sup_congr, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
π : Prepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ (π.toSubordinate r).toPrepartition ≤ π

Tactic:
(π.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r).choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, setOf, BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq, And.left