awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint (↑J : WithBot (Box ι)) (↑Js : WithBot (Box ι))
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ (↑J : Set (ι → ℝ))
hxs : x ∈ (↑Js : Set (ι → ℝ))
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ y i ≤ J.upper i
have refine_2 : ∀ (Jl : Box ι) (Hmem : Jl ∈ split I i (J.upper i)) (Hle : Js ≤ Jl), y i ≤ J.upper i
Tactic: rcases splitMany_le_split I (H i).2 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.upper i), Hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (hypothesis)
Goal:
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint (↑J : WithBot (Box ι)) (↑Js : WithBot (Box ι))
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ (↑J : Set (ι → ℝ))
hxs : x ∈ (↑Js : Set (ι → ℝ))
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (J.upper i)
Hle : Js ≤ Jl
⊢ y i ≤ J.upper i
have this : x ∈ Jl
Tactic: have := Hle hxs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (hypothesis)
Goal:
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint (↑J : WithBot (Box ι)) (↑Js : WithBot (Box ι))
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ (↑J : Set (ι → ℝ))
hxs : x ∈ (↑Js : Set (ι → ℝ))
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (J.upper i)
Hle : Js ≤ Jl
this : x ∈ Jl
⊢ y i ≤ J.upper i
have Hle₁ : (↑Js : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ J.upper i}
Tactic: rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_mem_le Hmem this (hx i).2] at Hle
Cleared hypotheses: Hle, this
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Finset (Box ι)
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
have intro : ∀ (val : Fintype ι),
  ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Finset (Box ι)
val : Fintype ι
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
have intro : ∀ (t : Finset (ι × ℝ))
  (ht : t ≥ s.biUnion fun (J : Box ι) ↦ Finset.biUnion Finset.univ fun (i : ι) ↦ {(i, J.lower i), (i, J.upper i)})
  (I J : Box ι) (hJ : J ∈ s) (J' : Box ι) (hJ' : J' ∈ splitMany I t) (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ t
Tactic: refine eventually_atTop.2
    ⟨s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)},
      fun t ht I J hJ J' hJ' => not_disjoint_imp_le_of_subset_of_mem_splitMany (fun i => ?_) hJ'⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Finset (Box ι)
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
have intro : ∀ (val : Fintype ι),
  ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
Tactic: classical
  cases nonempty_fintype ι
  refine eventually_atTop.2
    ⟨s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)},
      fun t ht I J hJ J' hJ' => not_disjoint_imp_le_of_subset_of_mem_splitMany (fun i => ?_) hJ'⟩
  exact fun p hp =>
    ht (Finset.mem_biUnion.2 ⟨J, hJ, Finset.mem_biUnion.2 ⟨i, Finset.mem_univ _, hp⟩⟩)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Finset (Box ι)
intro :
  ∀ (val : Fintype ι),
    ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
      ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
have intro₁ : ∀ (val : Fintype ι) (t : Finset (ι × ℝ))
  (ht : t ≥ s.biUnion fun (J : Box ι) ↦ Finset.biUnion Finset.univ fun (i : ι) ↦ {(i, J.lower i), (i, J.upper i)})
  (I J : Box ι) (hJ : J ∈ s) (J' : Box ι) (hJ' : J' ∈ splitMany I t) (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ t
Tactic: classical
  cases nonempty_fintype ι
  refine eventually_atTop.2
    ⟨s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)},
      fun t ht I J hJ J' hJ' => not_disjoint_imp_le_of_subset_of_mem_splitMany (fun i => ?_) hJ'⟩
  exact fun p hp =>
    ht (Finset.mem_biUnion.2 ⟨J, hJ, Finset.mem_biUnion.2 ⟨i, Finset.mem_univ _, hp⟩⟩)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    π ⊓ splitMany I t = (splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
have refine : ∀ (t : Finset (ι × ℝ))
  (ht :
    ∀ (I_1 J : Box ι),
      J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J),
  π ⊓ splitMany I t = (splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
Tactic: refine (eventually_not_disjoint_imp_le_of_mem_splitMany π.boxes).mono fun t ht => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht :
  ∀ (I_1 J : Box ι),
    J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
⊢ π ⊓ splitMany I t = (splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
have refine_1 : ∀ (J : Box ι) (hJ : J ∈ π),
  (splitMany I t).restrict J ≤ ((splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion).restrict J
Tactic: refine le_antisymm ((biUnion_le_iff _).2 fun J hJ => ?_) (le_inf (fun J hJ => ?_) (filter_le _ _))
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht :
  ∀ (I_1 J : Box ι),
    J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
refine_1 :
  ∀ (J : Box ι) (hJ : J ∈ π),
    (splitMany I t).restrict J ≤ ((splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion).restrict J
⊢ π ⊓ splitMany I t = (splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
have refine_2 : ∀ (J : Box ι) (hJ : J ∈ (splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion), ∃ I' ∈ π, J ≤ I'
Tactic: refine le_antisymm ((biUnion_le_iff _).2 fun J hJ => ?_) (le_inf (fun J hJ => ?_) (filter_le _ _))
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht :
  ∀ (I_1 J : Box ι),
    J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ (splitMany I t).restrict J ≤ ((splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion).restrict J
have refine_1 : ∀ (J_1 : WithBot (Box ι)),
  Membership.mem (γ := Finset (WithBot (Box ι)))
      (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) (splitMany I t).boxes) J_1 →
    J_1 ≠ ⊥ →
      ∃ (J' : WithBot (Box ι)),
        Membership.mem (γ := Finset (WithBot (Box ι)))
            (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι)))
              ((splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion).boxes)
            J' ∧
          J_1 ≤ J'
Tactic: refine ofWithBot_mono ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht :
  ∀ (I_1 J : Box ι),
    J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ (J_1 : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) (splitMany I t).boxes) J_1 →
      J_1 ≠ ⊥ →
        ∃ (J' : WithBot (Box ι)),
          Membership.mem (γ := Finset (WithBot (Box ι)))
              (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι)))
                ((splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion).boxes)
              J' ∧
            J_1 ≤ J'
have refine_1 : ∀ (J_1 : WithBot (Box ι)),
  (∃ a ∈ splitMany I t, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = J_1) →
    J_1 ≠ ⊥ →
      ∃ (J' : WithBot (Box ι)),
        (∃ (a : Box ι),
            (a ∈ splitMany I t ∧ (↑a : Set (ι → ℝ)) ⊆ π.iUnion) ∧
              (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = J') ∧
          J_1 ≤ J'
Tactic: simp only [Finset.mem_image, mem_boxes, mem_filter]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht :
  ∀ (I_1 J : Box ι),
    J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ ⊥
⊢ ∃ (J' : WithBot (Box ι)),
    (∃ (a : Box ι),
        (a ∈ splitMany I t ∧ (↑a : Set (ι → ℝ)) ⊆ π.iUnion) ∧ (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = J') ∧
      (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≤ J'
have refine_1 : (↑J₁ : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
Tactic: refine ⟨_, ⟨J₁, ⟨h₁, Subset.trans ?_ (π.subset_iUnion hJ)⟩, rfl⟩, le_rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (hypothesis)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht :
  ∀ (I_1 J : Box ι),
    J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
J : Box ι
hJ : J ∈ (splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
⊢ ∃ I' ∈ π, J ≤ I'
have hJ₁ : J ∈ splitMany I t ∧ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
Tactic: rw [mem_filter] at hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht :
  ∀ (I_1 J : Box ι),
    J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
⊢ ∃ I' ∈ π, J ≤ I'
have refine_2 : ∀ (J' : Box ι) (hJ' : J' ∈ π) (hmem : J.upper ∈ (↑J' : Set (ι → ℝ))), ∃ I' ∈ π, J ≤ I'
Tactic: rcases Set.mem_iUnion₂.1 (hJ.2 J.upper_mem) with ⟨J', hJ', hmem⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht :
  ∀ (I_1 J : Box ι),
    J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
J' : Box ι
hJ' : J' ∈ π
hmem : J.upper ∈ (↑J' : Set (ι → ℝ))
⊢ ∃ I' ∈ π, J ≤ I'
have refine_2 : ((↑J' : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty
Tactic: refine ⟨J', hJ', ht I _ hJ' _ hJ.1 <| Box.not_disjoint_coe_iff_nonempty_inter.2 ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
⊢ ∃ (s : Finset (ι × ℝ)), splitMany I s ≤ π
have refine : ∀ (s : Finset (ι × ℝ))
  (hs : π ⊓ splitMany I s = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion), splitMany I s ≤ π
Tactic: refine (eventually_splitMany_inf_eq_filter π).exists.imp fun s hs => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
⊢ splitMany I s ≤ π
have hp : ∀ (hs : π ⊓ splitMany I s = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))),
  ∀ J ∈ splitMany I s, (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))
Tactic: rwa [h.iUnion_eq, filter_of_true, inf_eq_right] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
⊢ ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
have rcases : ∀ (s : Finset (ι × ℝ))
  (hs : π ⊓ splitMany I s = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion),
  ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
Tactic: rcases π.eventually_splitMany_inf_eq_filter.exists with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ ⋯.choose (p := fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion) =
    ⋯.choose (p := fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion)
have e_p : Eq.{u_1 + 1} (α := Prepartition I → Prop) (fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion)
  fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ Eq.{u_1 + 1} (α := Prepartition I → Prop) (fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion)
    fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion
have e_p : Eq.{u_1 + 1} (α := Prepartition I → Prop) (fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion)
  fun (π' : Prepartition I) ↦ π'.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
h : π.IsPartition
⊢ π.compl = ⊥
have rw : π.compl.iUnion = ∅
Tactic: rw [← iUnion_eq_empty, iUnion_compl, h.iUnion_eq, diff_self]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
h : π.IsPartition
rw : π.compl.iUnion = ∅
⊢ π.compl = ⊥
have rw₁ : (↑I : Set (ι → ℝ)) \ π.iUnion = ∅
Tactic: rw [← iUnion_eq_empty, iUnion_compl, h.iUnion_eq, diff_self]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
h : π.IsPartition
rw : π.compl.iUnion = ∅
rw₁ : (↑I : Set (ι → ℝ)) \ π.iUnion = ∅
⊢ π.compl = ⊥
have rw₂ : (↑I : Set (ι → ℝ)) \ (↑I : Set (ι → ℝ)) = ∅
Tactic: rw [← iUnion_eq_empty, iUnion_compl, h.iUnion_eq, diff_self]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
h : π.IsPartition
rw : π.compl.iUnion = ∅
rw₁ : (↑I : Set (ι → ℝ)) \ π.iUnion = ∅
rw₂ : (↑I : Set (ι → ℝ)) \ (↑I : Set (ι → ℝ)) = ∅
⊢ π.compl = ⊥
have rw₃ : Eq.{u_1 + 1} (α := Set (ι → ℝ)) ∅ ∅
Tactic: rw [← iUnion_eq_empty, iUnion_compl, h.iUnion_eq, diff_self]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
Goal:
ι : Type u_1
inst : Fintype ι
I_1 J I : Box ι
⊢ (↑(Finset.map I.splitCenterBoxEmb Finset.univ) : Set (Box ι)).Pairwise (Function.onFun Disjoint Box.toSet)
have rw : Set.Pairwise (α := Box ι) (range (ι := Set ι) (⇑I.splitCenterBoxEmb : (a : Set ι) → Box ι))
  (Function.onFun Disjoint Box.toSet)
Tactic: rw [Finset.coe_map, Finset.coe_univ, image_univ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
have refine : ∀ (J : Box ι) (hle : J ≤ I) (hs : ∀ (s : Set ι), p (J.splitCenterBox s)) (J' : Box ι) (h' : J' ∈ splitCenter J), p J'
Tactic: refine subbox_induction_on' I (fun J hle hs => H_ind J hle fun J' h' => ?_) H_nhds
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
⊢ p J'
have rcases : ∀ (s : Set ι) (h' : J.splitCenterBox s ∈ splitCenter J), p (J.splitCenterBox s)
Tactic: rcases mem_splitCenter.1 h' with ⟨s, rfl⟩
Cleared hypotheses: 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)
⊢ ∃ (π : 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
have 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
Tactic: refine subbox_induction_on I (fun J _ hJ => ?_) fun z _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (goal)
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
⊢ ∃ (π : 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
have 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
Tactic: refine subbox_induction_on I (fun J _ hJ => ?_) fun z _ => ?_
-- 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
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
have 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
Tactic: choose! πi hP hHen hr Hn _ using hJ
Cleared hypotheses: hJ
-- 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 : ∀ 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
⊢ ∃ (π : 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 : ∀ (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
Tactic: choose! n hn using Hn
Cleared hypotheses: Hn