awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (hypothesis)
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)
⊢ ∃ (π : 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
have hP₁ : ((splitCenter J).biUnionTagged πi).IsPartition
Tactic: have hP : ((splitCenter J).biUnionTagged πi).IsPartition :=
      (isPartition_splitCenter _).biUnionTagged hP
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
⊢ ∃ (n : ℕ), ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 n
have 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
Tactic: rcases (splitCenter J).mem_biUnionTagged.1 hJ' with ⟨J₁, h₁, h₂⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
have refine : ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 (n J₁ J' + 1)
Tactic: refine ⟨n J₁ J' + 1, fun i => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (hypothesis)
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
⊢ ∃ (π : 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
have hsub : ∀ 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
have refine_1 : ((splitCenter J).biUnionTagged πi).distortion = J.distortion
Tactic: refine ⟨_, hP, isHenstock_biUnionTagged.2 hHen, isSubordinate_biUnionTagged.2 hr, hsub, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
have refine_1 : ∀ (J' : Box ι) (h' : J' ∈ (splitCenter J).biUnionTagged πi), J'.distortion = J.distortion
Tactic: refine TaggedPrepartition.distortion_of_const _ hP.nonempty_boxes fun J' h' => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
⊢ J'.distortion = J.distortion
have 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
Tactic: rcases hsub J' h' with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
have 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
Tactic: refine ⟨Box.Icc I ∩ closedBall z (r z),
      inter_mem_nhdsWithin _ (closedBall_mem_nhds _ (r z).coe_prop), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (hypothesis)
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
⊢ ∃ (π : 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
have 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) : ℝ)
Tactic: rw [Set.subset_inter_iff] at HIcc
Cleared hypotheses: HIcc, Hsub
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
have refine_2 : ∀ J_1 ∈ TaggedPrepartition.single J J sorry z Hmem,
  ∃ (m : ℕ), ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m
Tactic: refine ⟨single _ _ le_rfl _ Hmem, isPartition_single _, isHenstock_single _,
      (isSubordinate_single _ _).2 HIcc.2, ?_, distortion_single _ _⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
⊢ ∀ 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
have refine_2 : ∃ (m : ℕ), ∀ (i : ι), J.upper i - J.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) 2 m
Tactic: simp only [TaggedPrepartition.mem_single, forall_eq]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
have refine_2 : ∀ (i : ι), J.upper i - J.lower i = (J.upper i - J.lower i) / HPow.hPow (α := ℝ) (β := ℕ) 2 0
Tactic: refine ⟨0, fun i => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : Prepartition I
⊢ ∃ (π' : TaggedPrepartition I),
    π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion
have 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
Tactic: have := fun J => Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic J r
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
⊢ ∃ (π' : TaggedPrepartition I),
    π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion
have 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
Tactic: choose! πi πip πiH πir _ πid using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
have refine : (π.biUnionTagged πi).distortion = π.distortion
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⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
⊢ (π.biUnionTagged πi).distortion = π.distortion
have rw : (π.boxes.sup fun (J : Box ι) ↦ (πi J).distortion) = π.distortion
Tactic: rw [distortion_biUnionTagged]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
⊢ x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J
have h : ∀ (x_1 : Box ι), x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π.toPrepartition), x ∈ (↑x_1 : Set (ι → ℝ))
Tactic: convert! Set.mem_iUnion₂
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
x_1 : Box ι
⊢ x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π.toPrepartition), x ∈ (↑x_1 : Set (ι → ℝ))
have h : x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π.toPrepartition), x ∈ x_1
Tactic: rw [Box.mem_coe, mem_toPrepartition, exists_prop]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
x_1 : Box ι
h : x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π.toPrepartition), x ∈ x_1
⊢ x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π.toPrepartition), x ∈ (↑x_1 : Set (ι → ℝ))
have h₁ : x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π), x ∈ x_1
Tactic: rw [Box.mem_coe, mem_toPrepartition, exists_prop]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
x_1 : Box ι
h : x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π.toPrepartition), x ∈ x_1
h₁ : x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π), x ∈ x_1
⊢ x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π.toPrepartition), x ∈ (↑x_1 : Set (ι → ℝ))
have h₂ : x_1 ∈ π ∧ x ∈ x_1 ↔ x_1 ∈ π ∧ x ∈ x_1
Tactic: rw [Box.mem_coe, mem_toPrepartition, exists_prop]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ (π.biUnionTagged πi).tag J' = (πi J).tag J'
have rw : (π.biUnionTagged πi).tag J' =
  TaggedPrepartition.tag (I := π.biUnionIndex (fun (J : Box ι) ↦ (πi J).toPrepartition) J')
    (πi (π.biUnionIndex (fun (J : Box ι) ↦ (πi J).toPrepartition) J')) J'
Tactic: rw [← π.biUnionIndex_of_mem (πi := fun J => (πi J).toPrepartition) hJ hJ']
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (∀ J ∈ π.biUnionTagged πi, p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
have simp : (∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
Tactic: simp only [mem_biUnionTagged]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
have refine_1 : ∀ (H : ∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J) (J : Box ι) (hJ : J ∈ π) (J' : Box ι)
  (hJ' : J' ∈ πi J), p ((πi J).tag J') J'
Tactic: refine ⟨fun H J hJ J' hJ' => ?_, fun H J' ⟨J, hJ, hJ'⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
refine_1 :
  ∀ (H : ∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J) (J : Box ι) (hJ : J ∈ π) (J' : Box ι)
    (hJ' : J' ∈ πi J), p ((πi J).tag J') J'
⊢ (∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
have refine_2 : ∀ (H : ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J') (J' : Box ι),
  (∃ J'_1 ∈ π, J' ∈ πi J'_1) → ∀ (J : Box ι) (hJ : J ∈ π) (hJ' : J' ∈ πi J), p ((π.biUnionTagged πi).tag J') J'
Tactic: refine ⟨fun H J hJ J' hJ' => ?_, fun H J' ⟨J, hJ, hJ'⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p ((πi J).tag J') J'
have refine_1 : p ((π.biUnionTagged πi).tag J') J'
Tactic: rw [← π.tag_biUnionTagged hJ hJ']
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
J' : Box ι
h : ∃ J'_1 ∈ π, J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p ((π.biUnionTagged πi).tag J') J'
have refine_2 : p ((πi J).tag J') J'
Tactic: rw [π.tag_biUnionTagged hJ hJ']
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
⊢ #({J ∈ π.boxes | π.tag J = x}) ≤
    #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x})
have refine : ∀ (J : Box ι) (hJ : J ∈ {J ∈ π.boxes | π.tag J = x}),
  J ∈ {J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}
Tactic: refine Finset.card_le_card fun J hJ => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J : Box ι
hJ : J ∈ {J ∈ π.boxes | π.tag J = x}
⊢ J ∈ {J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}
have rw : ∀ (hJ : J ∈ π.boxes ∧ π.tag J = x),
  J ∈ π.boxes ∧ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x
Tactic: rw [Finset.mem_filter] at hJ ⊢
Cleared hypotheses: hJ