awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π.iUnion ⊆ (↑I : Set (ι → ℝ))

Tactic:
iUnion₂_subset π.le_of_mem'

Premises used: Set.iUnion₂_subset, BoxIntegral.Prepartition.le_of_mem', BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h : π₁ ≤ π₂
⊢ π₁.iUnion ⊆ π₂.iUnion

Tactic:
fun _ hx =>
  let ⟨_, hJ₁, hx⟩ := π₁.mem_iUnion.1 hx
  let ⟨J₂, hJ₂, hle⟩ := h hJ₁
  π₂.mem_iUnion.2 ⟨J₂, hJ₂, hle hx⟩

Premises used: Iff.mpr, Membership.mem, Set.Subset, BoxIntegral.Prepartition.partialOrder.match_1, And.intro, _private.0.BoxIntegral.Prepartition.iUnion_mono.match_1, Exists.intro, Iff.mp, BoxIntegral.Prepartition.mem_iUnion, BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ Disjoint π₁.boxes π₂.boxes

Tactic:
Finset.disjoint_left.2 fun J h₁ h₂ =>
    Disjoint.le_bot (h.mono (π₁.subset_iUnion h₁) (π₂.subset_iUnion h₂)) ⟨J.upper_mem, J.upper_mem⟩

Premises used: Iff.mpr, Disjoint.le_bot, BoxIntegral.Prepartition.subset_iUnion, And.intro, Disjoint.mono, Finset.disjoint_left, BoxIntegral.Box.upper_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
mp :
  π₁ ≤ π₂ → (∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion
mpr :
  (∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion → π₁ ≤ π₂
⊢ π₁ ≤ π₂ ↔ (∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion

Tactic:
constructor
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
⊢ π₁ ≤ π₂ → (∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion

Tactic:
fun H => ⟨fun J hJ J' hJ' Hne => ?_, iUnion_mono H⟩

Premises used: BoxIntegral.Prepartition.iUnion_mono, And.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
mp :
  ∀ (H : π₁ ≤ π₂) (J : Box ι) (hJ : J ∈ π₁) (J' : Box ι) (hJ' : J' ∈ π₂)
    (Hne : ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty), J ≤ J'
⊢ π₁ ≤ π₂ → (∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion

Tactic:
refine fun H => ⟨fun J hJ J' hJ' Hne => ?_, iUnion_mono H⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
Hne : ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty
mp : ∀ (J'' : Box ι) (hJ'' : J'' ∈ π₂) (Hle : J ≤ J''), J ≤ J'
⊢ J ≤ J'

Tactic:
rcases H hJ with ⟨J'', hJ'', Hle⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
Hne : ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty
J'' : Box ι
hJ'' : J'' ∈ π₂
Hle : J ≤ J''
mp : ∀ (x : ι → ℝ) (hx : x ∈ (↑J : Set (ι → ℝ))) (hx' : x ∈ (↑J' : Set (ι → ℝ))), J ≤ J'
⊢ J ≤ J'

Tactic:
rcases Hne with ⟨x, hx, hx'⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
J'' : Box ι
hJ'' : J'' ∈ π₂
Hle : J ≤ J''
x : ι → ℝ
hx : x ∈ (↑J : Set (ι → ℝ))
hx' : x ∈ (↑J' : Set (ι → ℝ))
mp mp₁ mp₂ mp₃ : J ≤ J''
⊢ J ≤ J'

Tactic:
rwa [π₂.eq_of_mem_of_mem hJ' hJ'' hx' (Hle hx)]

Premises used: BoxIntegral.Prepartition.eq_of_mem_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : ∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J'
HU : π₁.iUnion ⊆ π₂.iUnion
J : Box ι
hJ : J ∈ π₁
⊢ ∀ (x : ι → ℝ), (∃ J ∈ π₁, x ∈ J) → ∃ J ∈ π₂, x ∈ J

Tactic:
simp only [Set.subset_def, mem_iUnion] at HU

Premises used: Set.subset_def, BoxIntegral.Prepartition.mem_iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : ∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J ∈ π₁, x ∈ J) → ∃ J ∈ π₂, x ∈ J
mpr : ∀ (J₂ : Box ι) (hJ₂ : J₂ ∈ π₂) (hx : J.upper ∈ J₂), ∃ I' ∈ π₂, J ≤ I'
⊢ ∃ I' ∈ π₂, J ≤ I'

Tactic:
rcases HU J.upper ⟨J, hJ, J.upper_mem⟩ with ⟨J₂, hJ₂, hx⟩

Premises used: BoxIntegral.Box.upper, And.intro, Exists.intro, BoxIntegral.Box.upper_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : ∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J ∈ π₁, x ∈ J) → ∃ J ∈ π₂, x ∈ J
J₂ : Box ι
hJ₂ : J₂ ∈ π₂
hx : J.upper ∈ J₂
⊢ ∃ I' ∈ π₂, J ≤ I'

Tactic:
⟨J₂, hJ₂, H _ hJ _ hJ₂ ⟨_, J.upper_mem, hx⟩⟩

Premises used: And.intro, Exists.intro, BoxIntegral.Box.upper_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : ∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J ∈ π₁, x ∈ J) → ∃ J ∈ π₂, x ∈ J
J₂ : Box ι
hJ₂ : J₂ ∈ π₂
hx : J.upper ∈ J₂
⊢ ∃ I' ∈ π₂, J ≤ I'

Tactic:
exact ⟨J₂, hJ₂, H _ hJ _ hJ₂ ⟨_, J.upper_mem, hx⟩⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h₁ : π₁.boxes ⊆ π₂.boxes
h₂ : π₂.iUnion ⊆ π₁.iUnion
⊢ π₁ = π₂

Tactic:
le_antisymm (fun J hJ => ⟨J, h₁ hJ, le_rfl⟩) <|
    le_iff_nonempty_imp_le_and_iUnion_subset.2
      ⟨fun _ hJ₁ _ hJ₂ Hne =>
        (π₂.eq_of_mem_of_mem hJ₁ (h₁ hJ₂) Hne.choose_spec.1 Hne.choose_spec.2).le, h₂⟩

Premises used: Iff.mpr, Exists.choose_spec, BoxIntegral.Prepartition.eq_of_mem_of_mem, Eq.le, le_antisymm, And.right, And.left, And.intro, BoxIntegral.Prepartition.le_iff_nonempty_imp_le_and_iUnion_subset
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : Membership.mem (γ := Finset (Box ι)) (π.boxes.biUnion fun (J : Box ι) ↦ (πi J).boxes) J
⊢ ∃ a ∈ π, J ∈ πi a

Tactic:
simp only [Finset.mem_biUnion, mem_boxes] at hJ

Premises used: BoxIntegral.Prepartition.mem_boxes, Finset.mem_biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : ∃ a ∈ π, J ∈ πi a
rcases : ∀ (J' : Box ι) (hJ' : J' ∈ π) (hJ : J ∈ πi J'), J ≤ I
⊢ J ≤ I

Tactic:
rcases hJ with ⟨J', hJ', hJ⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J J' : Box ι
hJ' : J' ∈ π
hJ : J ∈ πi J'
⊢ J ≤ I

Tactic:
((πi J').le_of_mem hJ).trans (π.le_of_mem hJ')

Premises used: BoxIntegral.Prepartition.le_of_mem, LE.le.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J J' : Box ι
hJ' : J' ∈ π
hJ : J ∈ πi J'
⊢ J ≤ I

Tactic:
exact ((πi J').le_of_mem hJ).trans (π.le_of_mem hJ')

Premises used: BoxIntegral.Prepartition.le_of_mem, LE.le.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
simp :
  ∀ ⦃x : Box ι⦄,
    (∃ a ∈ π.boxes, x ∈ (πi a).boxes) →
      ∀ ⦃y : Box ι⦄, (∃ a ∈ π.boxes, y ∈ (πi a).boxes) → x ≠ y → (Disjoint on Box.toSet) x y
⊢ (↑(π.boxes.biUnion fun (J : Box ι) ↦ (πi J).boxes) : Set (Box ι)).Pairwise (Disjoint on Box.toSet)

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

Premises used: Set.Pairwise, Finset.mem_coe, Finset.mem_biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
rw : ∀ ⦃a : ι → ℝ⦄, a ∈ (↑J₁' : Set (ι → ℝ)) → a ∉ (↑J₂' : Set (ι → ℝ))
⊢ (Disjoint on Box.toSet) J₁' J₂'

Tactic:
rw [Function.onFun, Set.disjoint_left]

Premises used: Function.onFun, Set.disjoint_left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x_1 : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ (↑J₁' : Set (ι → ℝ))
hx₂ : x ∈ (↑J₂' : Set (ι → ℝ))
apply : J₁' = J₂'
⊢ False

Tactic:
apply Hne
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x_1 : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ (↑J₁' : Set (ι → ℝ))
hx₂ : x ∈ (↑J₂' : Set (ι → ℝ))
⊢ J₁ = J₂

Tactic:
π.eq_of_mem_of_mem hJ₁ hJ₂ ((πi J₁).le_of_mem hJ₁' hx₁) ((πi J₂).le_of_mem hJ₂' hx₂)

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Prepartition.eq_of_mem_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x_1 : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ (↑J₁' : Set (ι → ℝ))
hx₂ : x ∈ (↑J₂' : Set (ι → ℝ))
⊢ J₁ ∈ π.boxes

Tactic:
obtain rfl : J₁ = J₂ :=
      π.eq_of_mem_of_mem hJ₁ hJ₂ ((πi J₁).le_of_mem hJ₁' hx₁) ((πi J₂).le_of_mem hJ₂' hx₂)

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Prepartition.eq_of_mem_of_mem, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x_1 : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ (↑J₁' : Set (ι → ℝ))
hx₂ : x ∈ (↑J₂' : Set (ι → ℝ))
hJ₃ : J₁ ∈ π.boxes
⊢ J₂' ∈ (πi J₁).boxes

Tactic:
obtain rfl : J₁ = J₂ :=
      π.eq_of_mem_of_mem hJ₁ hJ₂ ((πi J₁).le_of_mem hJ₁' hx₁) ((πi J₂).le_of_mem hJ₂' hx₂)

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Prepartition.eq_of_mem_of_mem, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁_1 J₂ : Box ι
π π₁ π₂ : Prepartition I
x_1 : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' : Box ι
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ (↑J₁' : Set (ι → ℝ))
hx₂ : x ∈ (↑J₂' : Set (ι → ℝ))
hJ₂ : J₁ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₁).boxes
⊢ J₁' = J₂'

Tactic:
(πi J₁).eq_of_mem_of_mem hJ₁' hJ₂' hx₁ hx₂

Premises used: BoxIntegral.Prepartition.eq_of_mem_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁_1 J₂ : Box ι
π π₁ π₂ : Prepartition I
x_1 : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' : Box ι
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ (↑J₁' : Set (ι → ℝ))
hx₂ : x ∈ (↑J₂' : Set (ι → ℝ))
hJ₂ : J₁ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₁).boxes
⊢ J₁' = J₂'

Tactic:
exact (πi J₁).eq_of_mem_of_mem hJ₁' hJ₂' hx₁ hx₂

Premises used: BoxIntegral.Prepartition.eq_of_mem_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ J ∈ π.biUnion πi ↔ ∃ J' ∈ π, J ∈ πi J'

Tactic:
simp [biUnion]

Premises used: BoxIntegral.Prepartition.biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ π.biUnion πi ≤ π

Tactic:
fun _ hJ =>
  let ⟨J', hJ', hJ⟩ := π.mem_biUnion.1 hJ
  ⟨J', hJ', (πi J').le_of_mem hJ⟩

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Prepartition.mem_biUnion, Membership.mem, Exists, LE.le, And, _private.0.BoxIntegral.Prepartition.biUnion_le.match_1, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
h : ∀ (J : Box ι), (J ∈ π.biUnion fun (x : Box ι) ↦ ⊤) ↔ J ∈ π
⊢ (π.biUnion fun (x : Box ι) ↦ ⊤) = π

Tactic:
ext
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
J : Box ι
⊢ (J ∈ π.biUnion fun (x : Box ι) ↦ ⊤) ↔ J ∈ π

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
h : π₁ = π₂
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
subst : π₁.biUnion πi₁ = π₁.biUnion πi₂
⊢ π₁.biUnion πi₁ = π₂.biUnion πi₂

Tactic:
subst π₂
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
h : ∀ (J : Box ι), J ∈ π₁.biUnion πi₁ ↔ J ∈ π₁.biUnion πi₂
⊢ π₁.biUnion πi₁ = π₁.biUnion πi₂

Tactic:
ext J
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
h : (∃ J' ∈ π₁, J ∈ πi₁ J') ↔ ∃ J' ∈ π₁, J ∈ πi₂ J'
⊢ J ∈ π₁.biUnion πi₁ ↔ J ∈ π₁.biUnion πi₂

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₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
h : (∃ J' ∈ π₁, J ∈ πi₁ J') → ∃ J' ∈ π₁, J ∈ πi₂ J'
h₁ : (∃ J' ∈ π₁, J ∈ πi₂ J') → ∃ J' ∈ π₁, J ∈ πi₁ J'
⊢ (∃ J' ∈ π₁, J ∈ πi₁ J') ↔ ∃ J' ∈ π₁, J ∈ πi₂ J'

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

Tactic:
fun ⟨J', h₁, h₂⟩ => ⟨J', h₁, hi J' h₁ ▸ h₂⟩

Premises used: Membership.mem, Exists, Eq.rec, And, _private.0.BoxIntegral.Prepartition.biUnion_le.match_1, And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₁ J') → ∃ J' ∈ π₁, J ∈ πi₂ J'

Tactic:
exact fun ⟨J', h₁, h₂⟩ => ⟨J', h₁, hi J' h₁ ▸ h₂⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₂ J') → ∃ J' ∈ π₁, J ∈ πi₁ J'

Tactic:
fun ⟨J', h₁, h₂⟩ => ⟨J', h₁, hi J' h₁ ▸ h₂⟩

Premises used: Membership.mem, Exists, Eq.rec, And, _private.0.BoxIntegral.Prepartition.biUnion_le.match_1, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₂ J') → ∃ J' ∈ π₁, J ∈ πi₁ J'

Tactic:
exact fun ⟨J', h₁, h₂⟩ => ⟨J', h₁, hi J' h₁ ▸ h₂⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
h : π₁ = π₂
hi : ∀ J ≤ I, πi₁ J = πi₂ J
⊢ π₁.biUnion πi₁ = π₂.biUnion πi₂

Tactic:
biUnion_congr h fun J hJ => hi J (π₁.le_of_mem hJ)

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Prepartition.biUnion_congr
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnion πi).iUnion = ⋃ J ∈ π, (πi J).iUnion

Tactic:
simp [Prepartition.iUnion]

Premises used: BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
M : Type u_2
inst : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π.boxes.biUnion fun (J : Box ι) ↦ (πi J).boxes, f J)
    (∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J')

Tactic:
Finset.sum_biUnion fun J₁ h₁ J₂ h₂ hne => Finset.disjoint_left.2 fun J' h₁' h₂' => ?_

Premises used: Iff.mpr, Finset.sum_biUnion, Finset.disjoint_left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
M : Type u_2
inst : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
refine :
  ∀ (J₁ : Box ι) (h₁ : J₁ ∈ (↑π.boxes : Set (Box ι))) (J₂ : Box ι) (h₂ : J₂ ∈ (↑π.boxes : Set (Box ι))) (hne : J₁ ≠ J₂)
    (J' : Box ι) (h₁' : Membership.mem (γ := Finset (Box ι)) ((fun (J : Box ι) ↦ (πi J).boxes) J₁) J')
    (h₂' : Membership.mem (γ := Finset (Box ι)) ((fun (J : Box ι) ↦ (πi J).boxes) J₂) J'), False
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π.boxes.biUnion fun (J : Box ι) ↦ (πi J).boxes, f J)
    (∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J')

Tactic:
refine Finset.sum_biUnion fun J₁ h₁ J₂ h₂ hne => Finset.disjoint_left.2 fun J' h₁' h₂' => ?_

Premises used: Iff.mpr, Finset.sum_biUnion, Finset.disjoint_left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
M : Type u_2
inst : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
J₁ : Box ι
h₁ : J₁ ∈ (↑π.boxes : Set (Box ι))
J₂ : Box ι
h₂ : J₂ ∈ (↑π.boxes : Set (Box ι))
hne : J₁ ≠ J₂
J' : Box ι
h₁' : Membership.mem (γ := Finset (Box ι)) ((fun (J : Box ι) ↦ (πi J).boxes) J₁) J'
h₂' : Membership.mem (γ := Finset (Box ι)) ((fun (J : Box ι) ↦ (πi J).boxes) J₂) J'
⊢ False

Tactic:
hne (π.eq_of_le_of_le h₁ h₂ ((πi J₁).le_of_mem h₁') ((πi J₂).le_of_mem h₂'))

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Prepartition.eq_of_le_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
M : Type u_2
inst : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
J₁ : Box ι
h₁ : J₁ ∈ (↑π.boxes : Set (Box ι))
J₂ : Box ι
h₂ : J₂ ∈ (↑π.boxes : Set (Box ι))
hne : J₁ ≠ J₂
J' : Box ι
h₁' : Membership.mem (γ := Finset (Box ι)) ((fun (J : Box ι) ↦ (πi J).boxes) J₁) J'
h₂' : Membership.mem (γ := Finset (Box ι)) ((fun (J : Box ι) ↦ (πi J).boxes) J₂) J'
⊢ False

Tactic:
exact hne (π.eq_of_le_of_le h₁ h₂ ((πi J₁).le_of_mem h₁') ((πi J₂).le_of_mem h₂'))

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Prepartition.eq_of_le_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
rw : ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J') ∈ π
⊢ π.biUnionIndex πi J ∈ π

Tactic:
rw [biUnionIndex, dif_pos hJ]

Premises used: BoxIntegral.Prepartition.biUnionIndex, dif_pos
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J') ∈ π

Tactic:
(π.mem_biUnion.1 hJ).choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, BoxIntegral.Prepartition.mem_biUnion, setOf, And.left, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J') ∈ π

Tactic:
exact (π.mem_biUnion.1 hJ).choose_spec.1

Premises used: Exists.choose_spec, BoxIntegral.Prepartition.mem_biUnion, And.left, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
pos : ∀ (hJ : J ∈ π.biUnion πi), π.biUnionIndex πi J ≤ I
neg : ∀ (hJ : J ∉ π.biUnion πi), π.biUnionIndex πi J ≤ I
⊢ π.biUnionIndex πi J ≤ I

Tactic:
by_cases hJ : J ∈ π.biUnion πi

Premises used: BoxIntegral.Prepartition.biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J ≤ I

Tactic:
π.le_of_mem (π.biUnionIndex_mem hJ)

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Prepartition.biUnionIndex_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J ≤ I

Tactic:
exact π.le_of_mem (π.biUnionIndex_mem hJ)

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Prepartition.biUnionIndex_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∉ π.biUnion πi
neg : (if hJ : J ∈ π.biUnion πi then ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J') else I) ≤ I
neg₁ neg₂ : I ≤ I
⊢ π.biUnionIndex πi J ≤ I

Tactic:
rw [biUnionIndex, dif_neg hJ]

Premises used: BoxIntegral.Prepartition.biUnionIndex, dif_neg
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ Membership.mem (γ := Prepartition (⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')))
    (πi (⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J'))) J

Tactic:
(π.mem_biUnion.1 hJ).choose_spec.2

Premises used: Exists.choose_spec, BoxIntegral.Prepartition.mem_biUnion, And.right, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
h : π.biUnionIndex πi J = ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')
h₁ h₂ :
  Prepartition (π.biUnionIndex πi J) = Prepartition (⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')) →
    π.biUnionIndex πi J = ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')
⊢ Membership.mem (γ := Prepartition (π.biUnionIndex πi J)) (πi (π.biUnionIndex πi J)) J

Tactic:
convert! (π.mem_biUnion.1 hJ).choose_spec.2

Premises used: Exists.choose_spec, BoxIntegral.Prepartition.mem_biUnion, And.right, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J = ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')

Tactic:
dif_pos hJ

Premises used: BoxIntegral.Prepartition.biUnionIndex, dif_pos
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J = ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')

Tactic:
exact dif_pos hJ

Premises used: dif_pos
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
e_2 : Prepartition (π.biUnionIndex πi J) = Prepartition (⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J'))
⊢ π.biUnionIndex πi J = ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')

Tactic:
dif_pos hJ

Premises used: BoxIntegral.Prepartition.biUnionIndex, dif_pos
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
e_2 : Prepartition (π.biUnionIndex πi J) = Prepartition (⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J'))
⊢ π.biUnionIndex πi J = ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')

Tactic:
exact dif_pos hJ

Premises used: dif_pos
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ J ≤ π.biUnionIndex πi J

Tactic:
le_of_mem _ (π.mem_biUnionIndex hJ)

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Prepartition.mem_biUnionIndex