awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ π.biUnionIndex πi J' = J

Tactic:
have : J' ∈ π.biUnion πi := π.mem_biUnion.2 ⟨J, hJ, hJ'⟩
  π.eq_of_le_of_le (π.biUnionIndex_mem this) hJ (π.le_biUnionIndex this) (le_of_mem _ hJ')

Premises used: Iff.mpr, BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Prepartition.eq_of_le_of_le, BoxIntegral.Prepartition.mem_biUnion, BoxIntegral.Prepartition.biUnionIndex_mem, BoxIntegral.Prepartition.le_biUnionIndex, And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
h :
  ∀ (J : Box ι),
    (J ∈ π.biUnion fun (J : Box ι) ↦ (πi J).biUnion (πi' J)) ↔
      J ∈ (π.biUnion πi).biUnion fun (J : Box ι) ↦ πi' (π.biUnionIndex πi J) J
⊢ (π.biUnion fun (J : Box ι) ↦ (πi J).biUnion (πi' J)) =
    (π.biUnion πi).biUnion fun (J : Box ι) ↦ πi' (π.biUnionIndex πi J) J

Tactic:
ext J
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
h :
  (∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1) ↔
    ∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'
⊢ (J ∈ π.biUnion fun (J : Box ι) ↦ (πi J).biUnion (πi' J)) ↔
    J ∈ (π.biUnion πi).biUnion fun (J : Box ι) ↦ πi' (π.biUnionIndex πi J) J

Tactic:
simp only [mem_biUnion]

Premises used: BoxIntegral.Prepartition.mem_biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
h :
  (∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1) →
    ∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'
h₁ :
  (∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J') →
    ∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1
⊢ (∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1) ↔
    ∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'

Tactic:
constructor
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ₁ : J₁ ∈ π
J₂ : Box ι
hJ₂ : J₂ ∈ πi J₁
hJ : J ∈ πi' J₁ J₂
⊢ ∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'

Tactic:
⟨J₂, ⟨J₁, hJ₁, hJ₂⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ₁ : J₁ ∈ π
J₂ : Box ι
hJ₂ : J₂ ∈ πi J₁
hJ : J ∈ πi' J₁ J₂
h : J ∈ πi' (π.biUnionIndex πi J₂) J₂
⊢ ∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'

Tactic:
refine ⟨J₂, ⟨J₁, hJ₁, hJ₂⟩, ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ₁ : J₁ ∈ π
J₂ : Box ι
hJ₂ : J₂ ∈ πi J₁
hJ h h₁ h₂ h₃ : J ∈ πi' J₁ J₂
⊢ J ∈ πi' (π.biUnionIndex πi J₂) J₂

Tactic:
rwa [π.biUnionIndex_of_mem hJ₁ hJ₂]

Premises used: BoxIntegral.Prepartition.biUnionIndex_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (π.biUnionIndex πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
⊢ ∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1

Tactic:
⟨J₂, hJ₂, J₁, hJ₁, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (π.biUnionIndex πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
h : J ∈ πi' J₂ J₁
⊢ ∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1

Tactic:
refine ⟨J₂, hJ₂, J₁, hJ₁, ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (π.biUnionIndex πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
h h₁ h₂ h₃ : ∀ (hJ : J ∈ πi' J₂ J₁) (hJ₂ : J₂ ∈ π) (hJ₁ : J₁ ∈ πi J₂), J ∈ πi' J₂ J₁
⊢ J ∈ πi' J₂ J₁

Tactic:
rwa [π.biUnionIndex_of_mem hJ₂ hJ₁] at hJ

Premises used: BoxIntegral.Prepartition.biUnionIndex_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
J : Box ι
hJ :
  Membership.mem (γ := Finset (Box ι))
    ((eraseNone : (a : Finset (Option (Box ι))) → Finset (Box ι)) boxes : Finset (Box ι)) J
⊢ some J ∈ boxes

Tactic:
rw [mem_eraseNone] at hJ

Premises used: Finset.mem_eraseNone
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
J : Box ι
hJ : some J ∈ boxes
⊢ J ≤ I

Tactic:
simpa only [WithBot.some_eq_coe, WithBot.coe_le_coe] using le_of_mem _ hJ

Premises used: WithBot.coe_le_coe, WithBot.some_eq_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
J₁ : Box ι
h₁ : J₁ ∈ (↑((eraseNone : (a : Finset (Option (Box ι))) → Finset (Box ι)) boxes : Finset (Box ι)) : Set (Box ι))
J₂ : Box ι
h₂ : J₂ ∈ (↑((eraseNone : (a : Finset (Option (Box ι))) → Finset (Box ι)) boxes : Finset (Box ι)) : Set (Box ι))
hne : J₁ ≠ J₂
⊢ some J₁ ∈ boxes

Tactic:
simp only [mem_coe, mem_eraseNone] at h₁ h₂

Premises used: Finset.mem_coe, Finset.mem_eraseNone
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
J₁ : Box ι
h₁ : J₁ ∈ (↑((eraseNone : (a : Finset (Option (Box ι))) → Finset (Box ι)) boxes : Finset (Box ι)) : Set (Box ι))
J₂ : Box ι
h₂ : J₂ ∈ (↑((eraseNone : (a : Finset (Option (Box ι))) → Finset (Box ι)) boxes : Finset (Box ι)) : Set (Box ι))
hne : J₁ ≠ J₂
h₃ : some J₁ ∈ boxes
⊢ some J₂ ∈ boxes

Tactic:
simp only [mem_coe, mem_eraseNone] at h₁ h₂

Premises used: Finset.mem_coe, Finset.mem_eraseNone
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
J₁ J₂ : Box ι
hne : J₁ ≠ J₂
h₁ : some J₁ ∈ boxes
h₂ : some J₂ ∈ boxes
⊢ (Disjoint on Box.toSet) J₁ J₂

Tactic:
Box.disjoint_coe.1 (pairwise_disjoint h₁ h₂ (mt Option.some_inj.1 hne))

Premises used: mt, BoxIntegral.Box.disjoint_coe, Iff.mp, Option.some_inj
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
J₁ J₂ : Box ι
hne : J₁ ≠ J₂
h₁ : some J₁ ∈ boxes
h₂ : some J₂ ∈ boxes
⊢ (Disjoint on Box.toSet) J₁ J₂

Tactic:
exact Box.disjoint_coe.1 (pairwise_disjoint h₁ h₂ (mt Option.some_inj.1 hne))

Premises used: mt, BoxIntegral.Box.disjoint_coe, Iff.mp, Option.some_inj
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
boxes : Finset (WithBot (Box ι))
h₁ : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
h₂ : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
⊢ J ∈ ofWithBot boxes h₁ h₂ ↔ (↑J : WithBot (Box ι)) ∈ boxes

Tactic:
mem_eraseNone

Premises used: WithBot.some, WithBot, Set.Mem, setOf, Finset.mem_eraseNone
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
this :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) ∈ boxes), (↑J : Set (ι → ℝ)))
    (⋃ J ∈ boxes, (↑J : Set (ι → ℝ)))
⊢ (ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, (↑J : Set (ι → ℝ))

Tactic:
simpa [ofWithBot, Prepartition.iUnion]

Premises used: BoxIntegral.Prepartition.ofWithBot, BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
suffices :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) ∈ boxes), (↑J : Set (ι → ℝ)))
    (⋃ J ∈ boxes, (↑J : Set (ι → ℝ)))
⊢ (ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, (↑J : Set (ι → ℝ))

Tactic:
suffices ⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J = ⋃ J ∈ boxes, (J : Set (ι → ℝ)) by
    simpa [ofWithBot, Prepartition.iUnion]
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) ∈ boxes), (↑J : Set (ι → ℝ)))
    (⋃ J ∈ boxes, (↑J : Set (ι → ℝ)))

Tactic:
simp only [← Box.biUnion_coe_eq_coe, @iUnion_comm _ _ (Box ι), @iUnion_comm _ _ (@Eq _ _ _),
    iUnion_iUnion_eq_right]

Premises used: Set.iUnion_iUnion_eq_right, BoxIntegral.Box.biUnion_coe_eq_coe, Set.iUnion_comm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ (↑J' : WithBot (Box ι))
J : Box ι
hJ : (↑J : WithBot (Box ι)) ∈ boxes
⊢ ∃ J' ∈ π, J ≤ J'

Tactic:
simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot

Premises used: WithBot.some, WithBot.coe_le_coe, WithBot.coe_ne_bot
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ (↑J' : WithBot (Box ι))
⊢ ∀ (J : Box ι), (↑J : WithBot (Box ι)) ∈ boxes → ∃ J' ∈ π, J ≤ J'

Tactic:
have : ∀ J : Box ι, ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J' := fun J hJ => by
    simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ (↑J' : WithBot (Box ι))
this : ∀ (J : Box ι), (↑J : WithBot (Box ι)) ∈ boxes → ∃ J' ∈ π, J ≤ J'
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π

Tactic:
simpa [ofWithBot, le_def]

Premises used: BoxIntegral.Prepartition.ofWithBot, BoxIntegral.Prepartition.le_def
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, (↑J : WithBot (Box ι)) ≤ J'
J : Box ι
hJ : J ∈ π
rcases :
  ∀ (J' : WithBot (Box ι)) (J'mem : J' ∈ boxes) (hle : (↑J : WithBot (Box ι)) ≤ J'),
    ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'

Tactic:
rcases H J hJ with ⟨J', J'mem, hle⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, (↑J : WithBot (Box ι)) ≤ J'
J : Box ι
hJ : J ∈ π
J' : WithBot (Box ι)
J'mem : J' ∈ boxes
hle : (↑J : WithBot (Box ι)) ≤ J'
⊢ J' ≠ ⊥

Tactic:
ne_bot_of_le_ne_bot WithBot.coe_ne_bot hle

Premises used: ne_bot_of_le_ne_bot, WithBot.coe_ne_bot
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, (↑J : WithBot (Box ι)) ≤ J'
J : Box ι
hJ : J ∈ π
J' : WithBot (Box ι)
J'mem : J' ∈ boxes
hle : (↑J : WithBot (Box ι)) ≤ J'
lift :
  ∀ (J' : Box ι) (J'mem : (↑J' : WithBot (Box ι)) ∈ boxes) (hle : (↑J : WithBot (Box ι)) ≤ (↑J' : WithBot (Box ι))),
    ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'

Tactic:
lift J' to Box ι using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hle

Premises used: ne_bot_of_le_ne_bot, BoxIntegral.Box
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, (↑J : WithBot (Box ι)) ≤ J'
J : Box ι
hJ : J ∈ π
J' : Box ι
J'mem : (↑J' : WithBot (Box ι)) ∈ boxes
hle : (↑J : WithBot (Box ι)) ≤ (↑J' : WithBot (Box ι))
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'

Tactic:
⟨J', mem_ofWithBot.2 J'mem, WithBot.coe_le_coe.1 hle⟩

Premises used: Iff.mpr, WithBot.coe_le_coe, And.intro, Exists.intro, Iff.mp, BoxIntegral.Prepartition.mem_ofWithBot
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, (↑J : WithBot (Box ι)) ≤ J'
J : Box ι
hJ : J ∈ π
J' : Box ι
J'mem : (↑J' : WithBot (Box ι)) ∈ boxes
hle : (↑J : WithBot (Box ι)) ≤ (↑J' : WithBot (Box ι))
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'

Tactic:
exact ⟨J', mem_ofWithBot.2 J'mem, WithBot.coe_le_coe.1 hle⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
boxes₁ : Finset (WithBot (Box ι))
le_of_mem₁ : ∀ J ∈ boxes₁, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint₁ : (↑boxes₁ : Set (WithBot (Box ι))).Pairwise Disjoint
boxes₂ : Finset (WithBot (Box ι))
le_of_mem₂ : ∀ J ∈ boxes₂, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint₂ : (↑boxes₂ : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ boxes₁, J ≠ ⊥ → ∃ J' ∈ boxes₂, J ≤ J'
⊢ ofWithBot boxes₁ le_of_mem₁ pairwise_disjoint₁ ≤ ofWithBot boxes₂ le_of_mem₂ pairwise_disjoint₂

Tactic:
le_ofWithBot _ fun J hJ => H J (mem_ofWithBot.1 hJ) WithBot.coe_ne_bot

Premises used: WithBot.some, BoxIntegral.Prepartition.le_ofWithBot, Iff.mp, BoxIntegral.Prepartition.mem_ofWithBot, WithBot.coe_ne_bot
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
M : Type u_2
inst : AddCommMonoid M
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
f : Box ι → M
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ (ofWithBot boxes le_of_mem pairwise_disjoint).boxes, f J)
    (∑ J ∈ boxes, Option.elim' 0 f J)

Tactic:
Finset.sum_eraseNone _ _

Premises used: WithBot, Finset.sum_eraseNone
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J : Box ι
J' : WithBot (Box ι)
hJ' :
  Membership.mem (γ := Finset (WithBot (Box ι)))
    (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes) J'
rcases :
  ∀ (J' : Box ι)
    (hJ' :
      Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
        ((↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι)))),
    (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))
⊢ J' ≤ (↑J : WithBot (Box ι))

Tactic:
rcases Finset.mem_image.1 hJ' with ⟨J', -, rfl⟩

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J' : Box ι
hJ' :
  Membership.mem (γ := Finset (WithBot (Box ι)))
    (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
    ((↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι)))
⊢ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J' : Box ι
hJ' :
  Membership.mem (γ := Finset (WithBot (Box ι)))
    (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
    ((↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι)))
⊢ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J : Box ι
simp :
  ∀ ⦃x : WithBot (Box ι)⦄,
    (∃ a ∈ π.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = x) →
      ∀ ⦃y : WithBot (Box ι)⦄,
        (∃ a ∈ π.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = y) → x ≠ y → Disjoint x y
⊢ (↑(Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes) :
        Set (WithBot (Box ι))).Pairwise
    Disjoint

Tactic:
simp only [Set.Pairwise, Finset.mem_coe, Finset.mem_image]

Premises used: Finset.mem_image, Set.Pairwise, Finset.mem_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁_1 J₂ : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J₁ : Box ι
h₁ h₂ : J₁ ∈ π.boxes
Hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι))
⊢ False

Tactic:
Hne rfl

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁_1 J₂ : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J₁ : Box ι
h₁ h₂ : J₁ ∈ π.boxes
Hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι))
⊢ False

Tactic:
exact Hne rfl

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁_1 J₂_1 : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J₁ : Box ι
h₁ : J₁ ∈ π.boxes
J₂ : Box ι
h₂ : J₂ ∈ π.boxes
Hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ (↑J : WithBot (Box ι)) ⊓ (↑J₂ : WithBot (Box ι))
⊢ J₁ ≠ J₂

Tactic:
have : J₁ ≠ J₂ := by
        rintro rfl
        exact Hne rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁_1 J₂_1 : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J₁ : Box ι
h₁ : J₁ ∈ π.boxes
J₂ : Box ι
h₂ : J₂ ∈ π.boxes
Hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ (↑J : WithBot (Box ι)) ⊓ (↑J₂ : WithBot (Box ι))
this : J₁ ≠ J₂
⊢ Disjoint ((↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι))) ((↑J : WithBot (Box ι)) ⊓ (↑J₂ : WithBot (Box ι)))

Tactic:
((Box.disjoint_coe.2 <| π.disjoint_coe_of_mem h₁ h₂ this).inf_left' _).inf_right' _

Premises used: Iff.mpr, Disjoint.inf_right', BoxIntegral.Box.disjoint_coe, BoxIntegral.Prepartition.disjoint_coe_of_mem, Disjoint.inf_left'
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁_1 J₂_1 : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J₁ : Box ι
h₁ : J₁ ∈ π.boxes
J₂ : Box ι
h₂ : J₂ ∈ π.boxes
Hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ (↑J : WithBot (Box ι)) ⊓ (↑J₂ : WithBot (Box ι))
this : J₁ ≠ J₂
⊢ Disjoint ((↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι))) ((↑J : WithBot (Box ι)) ⊓ (↑J₂ : WithBot (Box ι)))

Tactic:
exact ((Box.disjoint_coe.2 <| π.disjoint_coe_of_mem h₁ h₂ this).inf_left' _).inf_right' _

Premises used: Iff.mpr, Disjoint.inf_right', BoxIntegral.Box.disjoint_coe, BoxIntegral.Prepartition.disjoint_coe_of_mem, Disjoint.inf_left'
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁ : Box ι
π : Prepartition I
⊢ J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, (↑J₁ : WithBot (Box ι)) = (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))

Tactic:
simp [restrict, eq_comm]

Premises used: eq_comm, BoxIntegral.Prepartition.restrict
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁ : Box ι
π : Prepartition I
⊢ J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, (↑J₁ : Set (ι → ℝ)) = (↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))

Tactic:
simp only [mem_restrict, ← Box.withBotCoe_inj, Box.coe_inf, Box.coe_coe]

Premises used: BoxIntegral.Box.coe_coe, BoxIntegral.Box.coe_inf, BoxIntegral.Box.withBotCoe_inj, BoxIntegral.Prepartition.mem_restrict
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
⊢ π₁.restrict J ≤ π₂.restrict J

Tactic:
ofWithBot_mono fun J₁ hJ₁ hne => ?_

Premises used: Set.Mem, setOf, BoxIntegral.Prepartition.ofWithBot_mono
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
refine :
  ∀ (J₁ : WithBot (Box ι))
    (hJ₁ :
      Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₁.boxes) J₁)
    (hne : J₁ ≠ ⊥),
    ∃ (J' : WithBot (Box ι)),
      Membership.mem (γ := Finset (WithBot (Box ι)))
          (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
        J₁ ≤ J'
⊢ π₁.restrict J ≤ π₂.restrict J

Tactic:
refine ofWithBot_mono fun J₁ hJ₁ hne => ?_

Premises used: BoxIntegral.Prepartition.ofWithBot_mono
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ :
  Membership.mem (γ := Finset (WithBot (Box ι)))
    (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₁.boxes) J₁
hne : J₁ ≠ ⊥
⊢ ∃ a ∈ π₁.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = J₁

Tactic:
rw [Finset.mem_image] at hJ₁

Premises used: Finset.mem_image