awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 : ι
refine_2 : ∀ (Jl : Box ι) (Hmem : Jl ∈ split I i (J.upper i)) (Hle : Js ≤ Jl), y i ≤ J.upper i
⊢ 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⟩

Premises used: BoxIntegral.Prepartition.split, BoxIntegral.Box.upper, And.right, BoxIntegral.Prepartition.splitMany_le_split
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
⊢ x ∈ Jl

Tactic:
have := Hle hxs
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
⊢ (↑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

Premises used: And.right, BoxIntegral.Prepartition.coe_eq_of_mem_split_of_mem_le, BoxIntegral.Box.coe_subset_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
Hle₁ : (↑Js : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ J.upper i}
⊢ x ∈ Jl

Tactic:
rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_mem_le Hmem this (hx i).2] at Hle

Premises used: And.right, BoxIntegral.Prepartition.coe_eq_of_mem_split_of_mem_le, BoxIntegral.Box.coe_subset_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ J.upper i}
this : x ∈ Jl
⊢ y i ≤ J.upper i

Tactic:
(Hle hy).2

Premises used: Set.Mem, And.right
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ J.upper i}
this : x ∈ Jl
⊢ y i ≤ J.upper i

Tactic:
exact (Hle hy).2

Premises used: And.right
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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

Tactic:
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'⟩

Premises used: Iff.mpr, Finset.univ, BoxIntegral.Box.upper, Insert.insert, Prod.mk, Finset.biUnion, BoxIntegral.Box.lower, Exists.intro, Filter.eventually_atTop, Singleton.singleton, BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
inst : Finite ι
s : Finset (Box ι)
val : Fintype ι
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
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint (↑J : WithBot (Box ι)) (↑J' : WithBot (Box ι)) → J' ≤ J

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'⟩

Premises used: Iff.mpr, Finset.univ, BoxIntegral.Box.upper, Insert.insert, Prod.mk, Finset.biUnion, BoxIntegral.Box.lower, Exists.intro, Filter.eventually_atTop, Singleton.singleton
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
inst : Finite ι
s : Finset (Box ι)
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:
fun p hp =>
    ht (Finset.mem_biUnion.2 ⟨J, hJ, Finset.mem_biUnion.2 ⟨i, Finset.mem_univ _, hp⟩⟩)

Premises used: Iff.mpr, Finset.mem_univ, And.intro, Exists.intro, Finset.mem_biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
inst : Finite ι
s : Finset (Box ι)
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:
exact fun p hp =>
    ht (Finset.mem_biUnion.2 ⟨J, hJ, Finset.mem_biUnion.2 ⟨i, Finset.mem_univ _, hp⟩⟩)

Premises used: Iff.mpr, Finset.mem_univ, And.intro, Exists.intro, Finset.mem_biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
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
⊢ ∀ᶠ (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⟩⟩)

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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

Tactic:
(eventually_not_disjoint_imp_le_of_mem_splitMany π.boxes).mono fun t ht => ?_

Premises used: BoxIntegral.Prepartition.boxes, Filter.Eventually.mono, BoxIntegral.Prepartition.eventually_not_disjoint_imp_le_of_mem_splitMany
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
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
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    π ⊓ 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 => ?_

Premises used: BoxIntegral.Prepartition.boxes, Filter.Eventually.mono, BoxIntegral.Prepartition.eventually_not_disjoint_imp_le_of_mem_splitMany
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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

Tactic:
le_antisymm ((biUnion_le_iff _).2 fun J hJ => ?_) (le_inf (fun J hJ => ?_) (filter_le _ _))

Premises used: Iff.mpr, BoxIntegral.Prepartition.biUnion_le_iff, le_inf, le_antisymm, BoxIntegral.Prepartition.filter_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
refine_2 :
  ∀ (J : Box ι) (hJ : J ∈ (splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion), ∃ I' ∈ π, J ≤ I'
⊢ π ⊓ splitMany I t = (splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion

Tactic:
refine le_antisymm ((biUnion_le_iff _).2 fun J hJ => ?_) (le_inf (fun J hJ => ?_) (filter_le _ _))

Premises used: Iff.mpr, BoxIntegral.Prepartition.biUnion_le_iff, le_inf, le_antisymm, BoxIntegral.Prepartition.filter_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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

Tactic:
ofWithBot_mono ?_

Premises used: Set.Mem, setOf, BoxIntegral.Prepartition.ofWithBot_mono
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 ∈ π
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'
⊢ (splitMany I t).restrict J ≤ ((splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion).restrict J

Tactic:
refine ofWithBot_mono ?_

Premises used: BoxIntegral.Prepartition.ofWithBot_mono
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 ∈ π
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'
⊢ ∀ (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:
simp only [Finset.mem_image, mem_boxes, mem_filter]

Premises used: Finset.mem_image, BoxIntegral.Prepartition.mem_filter, BoxIntegral.Prepartition.mem_boxes
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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'

Tactic:
⟨_, ⟨J₁, ⟨h₁, Subset.trans ?_ (π.subset_iUnion hJ)⟩, rfl⟩, le_rfl⟩

Premises used: le_rfl, BoxIntegral.Prepartition.subset_iUnion, Set.Subset.trans, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 ι)) ≠ ⊥
refine_1 : (↑J₁ : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
⊢ ∃ (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'

Tactic:
refine ⟨_, ⟨J₁, ⟨h₁, Subset.trans ?_ (π.subset_iUnion hJ)⟩, rfl⟩, le_rfl⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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₁ : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))

Tactic:
ht I J hJ J₁ h₁ (mt disjoint_iff.1 hne)

Premises used: Set.Mem, BoxIntegral.Box.toSet, setOf, disjoint_iff, mt, Set.Subset, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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₁ : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))

Tactic:
exact ht I J hJ J₁ h₁ (mt disjoint_iff.1 hne)

Premises used: disjoint_iff, mt, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
⊢ J ∈ splitMany I t ∧ (↑J : Set (ι → ℝ)) ⊆ π.iUnion

Tactic:
rw [mem_filter] at hJ

Premises used: BoxIntegral.Prepartition.mem_filter
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
refine_2 : ∀ (J' : Box ι) (hJ' : J' ∈ π) (hmem : J.upper ∈ (↑J' : Set (ι → ℝ))), ∃ I' ∈ π, J ≤ I'
⊢ ∃ I' ∈ π, J ≤ I'

Tactic:
rcases Set.mem_iUnion₂.1 (hJ.2 J.upper_mem) with ⟨J', hJ', hmem⟩

Premises used: Set.mem_iUnion₂, And.right, Iff.mp, BoxIntegral.Box.upper_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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'

Tactic:
⟨J', hJ', ht I _ hJ' _ hJ.1 <| Box.not_disjoint_coe_iff_nonempty_inter.2 ?_⟩

Premises used: Iff.mpr, BoxIntegral.Box.not_disjoint_coe_iff_nonempty_inter, And.left, And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 (ι → ℝ))
refine_2 : ((↑J' : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty
⊢ ∃ I' ∈ π, J ≤ I'

Tactic:
refine ⟨J', hJ', ht I _ hJ' _ hJ.1 <| Box.not_disjoint_coe_iff_nonempty_inter.2 ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 (ι → ℝ))
⊢ ((↑J' : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty

Tactic:
⟨J.upper, hmem, J.upper_mem⟩

Premises used: BoxIntegral.Box.upper, Set.Nonempty, And.intro, Exists.intro, BoxIntegral.Box.upper_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 (ι → ℝ))
⊢ ((↑J' : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty

Tactic:
exact ⟨J.upper, hmem, J.upper_mem⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
s : Set (Prepartition I)
hs : s.Finite
⊢ ∃ (t : Finset (ι × ℝ)),
    ∀ π ∈ s, π ⊓ splitMany I t = (splitMany I t).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion

Tactic:
haveI := fun π (_ : π ∈ s) => eventually_splitMany_inf_eq_filter π
  (hs.eventually_all.2 this).exists

Premises used: Iff.mpr, Set.Finite.eventually_all, Filter.Eventually.exists, BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
⊢ ∃ (s : Finset (ι × ℝ)), splitMany I s ≤ π

Tactic:
(eventually_splitMany_inf_eq_filter π).exists.imp fun s hs => ?_

Premises used: Exists.imp, Filter.Eventually.exists, BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
refine :
  ∀ (s : Finset (ι × ℝ))
    (hs : π ⊓ splitMany I s = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion), splitMany I s ≤ π
⊢ ∃ (s : Finset (ι × ℝ)), splitMany I s ≤ π

Tactic:
refine (eventually_splitMany_inf_eq_filter π).exists.imp fun s hs => ?_

Premises used: Exists.imp, Filter.Eventually.exists, BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
hp :
  ∀ (hs : π ⊓ splitMany I s = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))),
    ∀ J ∈ splitMany I s, (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))
⊢ splitMany I s ≤ π

Tactic:
rwa [h.iUnion_eq, filter_of_true, inf_eq_right] at hs

Premises used: BoxIntegral.Prepartition.IsPartition.iUnion_eq, BoxIntegral.Prepartition.filter_of_true, inf_eq_right
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))
⊢ ∀ J ∈ splitMany I s, (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))

Tactic:
fun J hJ => le_of_mem _ hJ

Premises used: BoxIntegral.Prepartition.le_of_mem, Set.Mem, BoxIntegral.Box.toSet, setOf, Set.Subset, BoxIntegral.Prepartition.splitMany
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))
⊢ ∀ J ∈ splitMany I s, (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))

Tactic:
exact fun J hJ => le_of_mem _ hJ

Premises used: BoxIntegral.Prepartition.le_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
rcases :
  ∀ (s : Finset (ι × ℝ))
    (hs : π ⊓ splitMany I s = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion),
    ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
⊢ ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion

Tactic:
rcases π.eventually_splitMany_inf_eq_filter.exists with ⟨s, hs⟩

Premises used: Filter.Eventually.exists, BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
⊢ ((splitMany I s).filter fun (J : Box ι) ↦ ¬(↑J : Set (ι → ℝ)) ⊆ π.iUnion).iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion

Tactic:
simp [← hs]
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
inst : Finite ι
π : Prepartition I
⊢ π.compl.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion

Tactic:
π.exists_iUnion_eq_diff.choose_spec

Premises used: Exists.choose_spec, BoxIntegral.Prepartition.exists_iUnion_eq_diff, BoxIntegral.Prepartition.compl