awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
s : Finset (Box ι)
h₁ : ∀ J ∈ s, J ≤ I
h₂ : (↑s : Set (Box ι)).Pairwise (Disjoint on Box.toSet)
⊢ J ∈ { boxes := s, le_of_mem' := h₁, pairwiseDisjoint := h₂ : Prepartition I } ↔ J ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J₁ J₂ : Box ι
π : Prepartition I
h₁ : J₁ ∈ π
h₂ : J₂ ∈ π
h : J₁ ≠ J₂
⊢ Disjoint (↑J₁ : Set (ι → ℝ)) (↑J₂ : Set (ι → ℝ))

Tactic:
π.pairwiseDisjoint h₁ h₂ h

Premises used: BoxIntegral.Prepartition.pairwiseDisjoint
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J₁ J₂ : Box ι
π : Prepartition I
x : ι → ℝ
h₁ : J₁ ∈ π
h₂ : J₂ ∈ π
hx₁ : x ∈ J₁
hx₂ : x ∈ J₂
⊢ J₁ = J₂

Tactic:
by_contra fun H => (π.disjoint_coe_of_mem h₁ h₂ H).le_bot ⟨hx₁, hx₂⟩

Premises used: Disjoint.le_bot, And.intro, by_contra, BoxIntegral.Prepartition.disjoint_coe_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁ J₂ : Box ι
π : Prepartition I
h₁ : J₁ ∈ π
h₂ : J₂ ∈ π
hle₁ : J ≤ J₁
hle₂ : J ≤ J₂
⊢ J₁ = J₂

Tactic:
π.eq_of_mem_of_mem h₁ h₂ (hle₁ J.upper_mem) (hle₂ J.upper_mem)

Premises used: BoxIntegral.Prepartition.eq_of_mem_of_mem, BoxIntegral.Box.upper_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J₁ J₂ : Box ι
π : Prepartition I
h₁ : J₁ ∈ π
h₂ : J₂ ∈ π
hle : J₁ ≤ J₂
⊢ J₁ = J₂

Tactic:
π.eq_of_le_of_le h₁ h₂ le_rfl hle

Premises used: le_rfl, BoxIntegral.Prepartition.eq_of_le_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
hJ : J ∈ π
⊢ J ≤ I

Tactic:
π.le_of_mem' J hJ

Premises used: BoxIntegral.Prepartition.le_of_mem'
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
hJ : J ∈ π
⊢ I.lower ≤ J.lower

Tactic:
Box.antitone_lower (π.le_of_mem hJ)

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Box.antitone_lower
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
hJ : J ∈ π
⊢ J.upper ≤ I.upper

Tactic:
Box.monotone_upper (π.le_of_mem hJ)

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.Box.monotone_upper
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
s₁ : Finset (Box ι)
h₁ : ∀ J ∈ s₁, J ≤ I
h₁' : (↑s₁ : Set (Box ι)).Pairwise (Disjoint on Box.toSet)
h₂ : ∀ J ∈ s₁, J ≤ I
h₂' : (↑s₁ : Set (Box ι)).Pairwise (Disjoint on Box.toSet)
⊢ { boxes := s₁, le_of_mem' := h₁, pairwiseDisjoint := h₁' : Prepartition I } =
    { boxes := s₁, le_of_mem' := h₂, pairwiseDisjoint := h₂' }

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

Tactic:
injective_boxes <| Finset.ext h

Premises used: BoxIntegral.Prepartition.injective_boxes, Finset.ext
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I_1 J_1 J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I_1
x : ι → ℝ
I J : Box ι
h : J ≤ I
⊢ ∀ (J_2 : Box ι), Membership.mem (γ := Finset (Box ι)) {J} J_2 → J_2 ≤ I

Tactic:
simpa
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I_1 J_1 J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I_1
x : ι → ℝ
I J : Box ι
h : J ≤ I
⊢ (↑{J} : Set (Box ι)).Pairwise (Disjoint on Box.toSet)

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J' : Box ι
h : J ≤ I
⊢ J' ∈ single I J h ↔ J' = J

Tactic:
mem_singleton

Premises used: Finset.mem_singleton, Set.Mem, setOf
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
suffices : ∀ {π₁ π₂ : Prepartition I}, π₁ ≤ π₂ → π₂ ≤ π₁ → π₁.boxes ⊆ π₂.boxes
⊢ ∀ (a b : Prepartition I), a ≤ b → b ≤ a → a = b

Tactic:
suffices ∀ {π₁ π₂ : Prepartition I}, π₁ ≤ π₂ → π₂ ≤ π₁ → π₁.boxes ⊆ π₂.boxes from
      fun π₁ π₂ h₁ h₂ => injective_boxes (Subset.antisymm (this h₁ h₂) (this h₂ h₁))
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
rcases : ∀ (J' : Box ι) (hJ' : J' ∈ π₂) (hle : J ≤ J'), J ∈ π₂.boxes
⊢ J ∈ π₂.boxes

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

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

Tactic:
π₁.eq_of_le hJ hJ'' (hle.trans hle')

Premises used: LE.le.trans, BoxIntegral.Prepartition.eq_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
J'' : Box ι
hJ'' : J'' ∈ π₁
hle' : J' ≤ J''
⊢ J ∈ π₁

Tactic:
obtain rfl : J = J'' := π₁.eq_of_le hJ hJ'' (hle.trans hle')

Premises used: LE.le.trans, rfl, BoxIntegral.Prepartition.eq_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
J'' : Box ι
hJ'' : J'' ∈ π₁
hle' : J' ≤ J''
hJ''₁ : J ∈ π₁
⊢ J' ≤ J

Tactic:
obtain rfl : J = J'' := π₁.eq_of_le hJ hJ'' (hle.trans hle')

Premises used: LE.le.trans, rfl, BoxIntegral.Prepartition.eq_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
hJ'' : J ∈ π₁
hle' : J' ≤ J
⊢ J' = J

Tactic:
le_antisymm ‹_› ‹_›

Premises used: le_antisymm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
hJ'' : J ∈ π₁
hle' : J' ≤ J
obtain : ∀ (hJ : J' ∈ π₁.boxes) (hle : J' ≤ J') (hJ'' : J' ∈ π₁) (hle' : J' ≤ J'), J' ∈ π₂.boxes
⊢ J ∈ π₂.boxes

Tactic:
obtain rfl : J' = J := le_antisymm ‹_› ‹_›

Premises used: le_antisymm, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J' : Box ι
hJ' : J' ∈ π₂
hJ : J' ∈ π₁.boxes
hle : J' ≤ J'
hJ'' : J' ∈ π₁
hle' : J' ≤ J'
⊢ J' ∈ π₂.boxes

Tactic:
assumption
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁ J₂ : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
π : Prepartition I
x_1 : Box ι
hJ : x_1 ∈ π
⊢ I ∈ single I I ⋯

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
⊢ π₁ ≤ π₂ ↔ ∀ J ∈ π₁, ∃ J' ∈ π₂, J ≤ J'

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ Membership.mem (γ := Prepartition I) ⊤ J ↔ J = I

Tactic:
mem_singleton

Premises used: Finset.mem_singleton, Set.Mem, setOf
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ Eq (α := Finset (Box ι)) (boxes (I := I) ⊤) {I}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ J ∉ ⊥

Tactic:
Finset.notMem_empty _

Premises used: Set.Mem, setOf, Finset.notMem_empty
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ Eq.{u_1 + 1} (α := Finset (Box ι)) (boxes (I := I) ⊥) ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
H : Eq.{u_1 + 1} (α := Set ι) {i : ι | J₁.lower i = x i} {i : ι | J₂.lower i = x i}
this : ∀ (i : ι), (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
choose :
  ∀ (y : (i : ι) → ℝ) (hy₁ : ∀ (i : ι), y i ∈ Set.Ioc (J₁.lower i) (J₁.upper i))
    (hy₂ : ∀ (i : ι), y i ∈ Set.Ioc (J₂.lower i) (J₂.upper i)), J₁ = J₂
⊢ J₁ = J₂

Tactic:
choose y hy₁ hy₂ using this
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
H : Eq.{u_1 + 1} (α := Set ι) {i : ι | J₁.lower i = x i} {i : ι | J₂.lower i = x i}
y : (i : ι) → ℝ
hy₁ : ∀ (i : ι), y i ∈ Set.Ioc (J₁.lower i) (J₁.upper i)
hy₂ : ∀ (i : ι), y i ∈ Set.Ioc (J₂.lower i) (J₂.upper i)
⊢ J₁ = J₂

Tactic:
π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂

Premises used: BoxIntegral.Prepartition.eq_of_mem_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
H : Eq.{u_1 + 1} (α := Set ι) {i : ι | J₁.lower i = x i} {i : ι | J₂.lower i = x i}
y : (i : ι) → ℝ
hy₁ : ∀ (i : ι), y i ∈ Set.Ioc (J₁.lower i) (J₁.upper i)
hy₂ : ∀ (i : ι), y i ∈ Set.Ioc (J₂.lower i) (J₂.upper i)
⊢ J₁ = J₂

Tactic:
exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂

Premises used: BoxIntegral.Prepartition.eq_of_mem_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
H : Eq.{u_1 + 1} (α := Set ι) {i : ι | J₁.lower i = x i} {i : ι | J₂.lower i = x i}
suffices : ∀ (i : ι), (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
⊢ J₁ = J₂

Tactic:
suffices ∀ i, (Ioc (J₁.lower i) (J₁.upper i) ∩ Ioc (J₂.lower i) (J₂.upper i)).Nonempty by
    choose y hy₁ hy₂ using this
    exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
H : Eq.{u_1 + 1} (α := Set ι) {i : ι | J₁.lower i = x i} {i : ι | J₂.lower i = x i}
i : ι
⊢ ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1

Tactic:
simp only [Set.ext_iff, mem_setOf] at H

Premises used: Set.mem_setOf, Set.ext_iff
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
inl : ∀ (hi₁ : J₁.lower i = x i), (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
inr : ∀ (hi₁ : J₁.lower i < x i), (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty

Tactic:
rcases (hx₁.1 i).eq_or_lt with hi₁ | hi₁

Premises used: LE.le.eq_or_lt, And.left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
⊢ J₂.lower i = x i

Tactic:
have hi₂ : J₂.lower i = x i := (H _).1 hi₁
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
⊢ x i < J₁.upper i

Tactic:
simpa only [hi₁] using J₁.lower_lt_upper i

Premises used: BoxIntegral.Box.lower_lt_upper
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
⊢ x i < J₁.upper i

Tactic:
have H₁ : x i < J₁.upper i := by simpa only [hi₁] using J₁.lower_lt_upper i
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
H₁ : x i < J₁.upper i
⊢ x i < J₂.upper i

Tactic:
simpa only [hi₂] using J₂.lower_lt_upper i

Premises used: BoxIntegral.Box.lower_lt_upper
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
H₁ : x i < J₁.upper i
⊢ x i < J₂.upper i

Tactic:
have H₂ : x i < J₂.upper i := by simpa only [hi₂] using J₂.lower_lt_upper i
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
H₁ : x i < J₁.upper i
H₂ : x i < J₂.upper i
inl : x i < min (J₁.upper i) (J₂.upper i)
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty

Tactic:
rw [Set.Ioc_inter_Ioc, hi₁, hi₂, sup_idem, Set.nonempty_Ioc]

Premises used: Set.nonempty_Ioc, sup_idem, Set.Ioc_inter_Ioc
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
H₁ : x i < J₁.upper i
H₂ : x i < J₂.upper i
⊢ x i < min (J₁.upper i) (J₂.upper i)

Tactic:
lt_min H₁ H₂

Premises used: lt_min
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
H₁ : x i < J₁.upper i
H₂ : x i < J₂.upper i
⊢ x i < min (J₁.upper i) (J₂.upper i)

Tactic:
exact lt_min H₁ H₂

Premises used: lt_min
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i < x i
⊢ J₂.lower i < x i

Tactic:
have hi₂ : J₂.lower i < x i := (hx₂.1 i).lt_of_ne (mt (H _).2 hi₁.ne)
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i < x i
hi₂ : J₂.lower i < x i
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty

Tactic:
⟨x i, ⟨hi₁, hx₁.2 i⟩, ⟨hi₂, hx₂.2 i⟩⟩

Premises used: Set.Nonempty, And.right, And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i < x i
hi₂ : J₂.lower i < x i
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty

Tactic:
exact ⟨x i, ⟨hi₁, hx₁.2 i⟩, ⟨hi₂, hx₂.2 i⟩⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
inst : Fintype ι
x : ι → ℝ
rw :
  #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}) ≤
    Fintype.card.{u_1} (Set ι)
⊢ #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card ι)

Tactic:
rw [← Fintype.card_set]

Premises used: Fintype.card_set
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
inst : Fintype ι
x : ι → ℝ
⊢ #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}) ≤
    Fintype.card.{u_1} (Set ι)

Tactic:
Finset.card_le_card_of_injOn (fun J : Box ι => { i | J.lower i = x i })
    (fun _ _ => Finset.mem_univ _) ?_

Premises used: Finset.mem_univ, setOf, Finset.card_le_card_of_injOn, Fintype.card, BoxIntegral.Box.lower, Eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
inst : Fintype ι
x : ι → ℝ
refine :
  InjOn (β := Set ι) (fun (J : Box ι) ↦ {i : ι | J.lower i = x i})
    (↑({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}) :
      Set (Box ι))
⊢ #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}) ≤
    Fintype.card.{u_1} (Set ι)

Tactic:
refine Finset.card_le_card_of_injOn (fun J : Box ι => { i | J.lower i = x i })
    (fun _ _ => Finset.mem_univ _) ?_

Premises used: Finset.mem_univ, setOf, Finset.card_le_card_of_injOn, BoxIntegral.Box.lower, Eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
inst : Fintype ι
x : ι → ℝ
⊢ InjOn (β := Set ι) (fun (J : Box ι) ↦ {i : ι | J.lower i = x i})
    (↑({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}) :
      Set (Box ι))

Tactic:
simpa using π.injOn_setOf_mem_Icc_setOf_lower_eq x

Premises used: BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π.iUnion = ⋃ J ∈ π, (↑J : Set (ι → ℝ))

Tactic:
rfl

Premises used: rfl, BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π.iUnion = ⋃ J ∈ π.boxes, (↑J : Set (ι → ℝ))

Tactic:
rfl

Premises used: rfl, BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
⊢ Membership.mem (γ := Set (ι → ℝ)) (⋃ i ∈ π, (↑i : Set (ι → ℝ))) x ↔ ∃ (i : Box ι) (_ : i ∈ π), x ∈ (↑i : Set (ι → ℝ))

Tactic:
Set.mem_iUnion₂

Premises used: Set.mem_iUnion₂
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
h : ∀ (x_1 : Box ι), x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π), x ∈ (↑x_1 : Set (ι → ℝ))
⊢ x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J

Tactic:
convert! Set.mem_iUnion₂

Premises used: Set.mem_iUnion₂
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
x_1 : Box ι
h : x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π), x ∈ x_1
h₁ h₂ : x_1 ∈ π ∧ x ∈ x_1 ↔ x_1 ∈ π ∧ x ∈ x_1
⊢ x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π), x ∈ (↑x_1 : Set (ι → ℝ))

Tactic:
rw [Box.mem_coe, exists_prop]

Premises used: BoxIntegral.Box.mem_coe, exists_prop
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
h : J ≤ I
⊢ (single I J h).iUnion = (↑J : Set (ι → ℝ))

Tactic:
simp [iUnion_def]

Premises used: BoxIntegral.Prepartition.iUnion_def
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ Prepartition.iUnion (I := I) ⊤ = (↑I : Set (ι → ℝ))

Tactic:
simp [Prepartition.iUnion]

Premises used: BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
⊢ π₁.iUnion = ∅ ↔ π₁ = ⊥

Tactic:
simp [← injective_boxes.eq_iff, Finset.ext_iff, Prepartition.iUnion, imp_false]

Premises used: imp_false, BoxIntegral.Prepartition.injective_boxes, Function.Injective.eq_iff, Finset.ext_iff, BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (Prepartition.iUnion (I := I) ⊥) ∅

Tactic:
iUnion_eq_empty.2 rfl

Premises used: Iff.mpr, BoxIntegral.Prepartition.iUnion_eq_empty, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : J ∈ π
⊢ (↑J : Set (ι → ℝ)) ⊆ π.iUnion

Tactic:
subset_biUnion_of_mem h

Premises used: Set.subset_biUnion_of_mem, BoxIntegral.Prepartition.iUnion