awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ ≠ ⊥
hJ₂ : ∃ a ∈ π₁.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = J₁
⊢ J₁ ≠ ⊥

Tactic:
rw [Finset.mem_image] at hJ₁

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

Tactic:
rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩

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

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

Tactic:
⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩

Premises used: Iff.mpr, inf_le_inf_left, WithBot.coe_le_coe, And.intro, Exists.intro, Finset.mem_image_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : Box ι
hJ₁ : J₁ ∈ π₁.boxes
hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ ⊥
J₂ : Box ι
hJ₂ : J₂ ∈ π₂
hle : J₁ ≤ J₂
⊢ ∃ (J' : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
      (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≤ J'

Tactic:
exact ⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩
-- 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'
refine₁ refine₂ :
  ∀ (J₁ : WithBot (Box ι)) (hJ₁ : ∃ a ∈ π₁.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = 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'
refine₃ :
  ∀ (J₁ : Box ι) (hJ₁ : J₁ ∈ π₁.boxes) (hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ ⊥),
    ∃ (J' : WithBot (Box ι)),
      Membership.mem (γ := Finset (WithBot (Box ι)))
          (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
        (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≤ J'
refine₄ :
  ∀ (J₁ : Box ι) (hJ₁ : J₁ ∈ π₁.boxes) (hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ ⊥) (J₂ : Box ι)
    (hJ₂ : J₂ ∈ π₂) (hle : J₁ ≤ J₂),
    ∃ (J' : WithBot (Box ι)),
      Membership.mem (γ := Finset (WithBot (Box ι)))
          (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
        (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≤ J'
⊢ π₁.restrict J ≤ π₂.restrict J

Tactic:
classical
  refine ofWithBot_mono fun J₁ hJ₁ hne => ?_
  rw [Finset.mem_image] at hJ₁; rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩
  rcases Hle hJ₁ with ⟨J₂, hJ₂, hle⟩
  exact ⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩

Premises used: Finset.mem_image, BoxIntegral.Prepartition.ofWithBot_mono, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ Monotone (β := Prepartition J) fun (π : Prepartition I) ↦ π.restrict J

Tactic:
fun _ _ => restrict_mono

Premises used: Set.Mem, Monotone, setOf, BoxIntegral.Prepartition.restrict_mono
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
simp :
  Finset.biUnion (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
      Option.toFinset =
    π.boxes
⊢ (π.restrict J).boxes = π.boxes

Tactic:
simp only [restrict, ofWithBot, eraseNone_eq_biUnion]

Premises used: BoxIntegral.Prepartition.ofWithBot, BoxIntegral.Prepartition.restrict, Finset.eraseNone_eq_biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ Finset.biUnion (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
      Option.toFinset =
    π.boxes

Tactic:
Finset.image_biUnion.trans ?_

Premises used: WithBot, Finset.image_biUnion, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
refine : (π.boxes.biUnion fun (a : Box ι) ↦ Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)))) = π.boxes
⊢ Finset.biUnion (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
      Option.toFinset =
    π.boxes

Tactic:
refine Finset.image_biUnion.trans ?_

Premises used: Finset.image_biUnion, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ (π.boxes.biUnion fun (a : Box ι) ↦ Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)))) = π.boxes

Tactic:
(Finset.biUnion_congr rfl ?_).trans Finset.biUnion_singleton_eq_self

Premises used: Finset.biUnion_singleton_eq_self, Finset.biUnion_congr, rfl, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
refine : ∀ a ∈ π.boxes, Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι))) = {a}
⊢ (π.boxes.biUnion fun (a : Box ι) ↦ Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)))) = π.boxes

Tactic:
refine (Finset.biUnion_congr rfl ?_).trans Finset.biUnion_singleton_eq_self

Premises used: Finset.biUnion_singleton_eq_self, Finset.biUnion_congr, rfl, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
J' : Box ι
hJ' : J' ∈ π.boxes
rw : (↑J' : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))
⊢ Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) = {J'}

Tactic:
rw [inf_of_le_right, ← WithBot.some_eq_coe, Option.toFinset_some]

Premises used: Option.toFinset_some, inf_of_le_right, WithBot.some_eq_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
J' : Box ι
hJ' : J' ∈ π.boxes
⊢ (↑J' : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))

Tactic:
WithBot.coe_le_coe.2 ((π.le_of_mem hJ').trans h)

Premises used: Iff.mpr, BoxIntegral.Prepartition.le_of_mem, WithBot.coe_le_coe, LE.le.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
J' : Box ι
hJ' : J' ∈ π.boxes
⊢ (↑J' : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))

Tactic:
exact WithBot.coe_le_coe.2 ((π.le_of_mem hJ').trans h)

Premises used: Iff.mpr, BoxIntegral.Prepartition.le_of_mem, WithBot.coe_le_coe, LE.le.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
simp :
  Finset.biUnion (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
      Option.toFinset =
    π.boxes
simp₁ : (π.boxes.biUnion fun (a : Box ι) ↦ Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)))) = π.boxes
simp₂ simp₃ :
  ∀ (J' : Box ι) (hJ' : J' ∈ π.boxes), Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) = {J'}
simp₄ : ∀ (J' : Box ι) (hJ' : J' ∈ π.boxes), (↑J' : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))
⊢ (π.restrict J).boxes = π.boxes

Tactic:
classical
  simp only [restrict, ofWithBot, eraseNone_eq_biUnion]
  refine Finset.image_biUnion.trans ?_
  refine (Finset.biUnion_congr rfl ?_).trans Finset.biUnion_singleton_eq_self
  intro J' hJ'
  rw [inf_of_le_right, ← WithBot.some_eq_coe, Option.toFinset_some]
  exact WithBot.coe_le_coe.2 ((π.le_of_mem hJ').trans h)

Premises used: Option.toFinset_some, inf_of_le_right, BoxIntegral.Prepartition.ofWithBot, Finset.biUnion_singleton_eq_self, BoxIntegral.Prepartition.restrict, Finset.eraseNone_eq_biUnion, Finset.image_biUnion, WithBot.some_eq_coe, Finset.biUnion_congr, rfl, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π.restrict I = π

Tactic:
injective_boxes <| restrict_boxes_of_le π le_rfl

Premises used: le_rfl, BoxIntegral.Prepartition.injective_boxes, BoxIntegral.Prepartition.restrict_boxes_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
⊢ (π.restrict J).iUnion = (↑J : Set (ι → ℝ)) ∩ π.iUnion

Tactic:
simp [restrict, ← inter_iUnion, ← iUnion_def]

Premises used: BoxIntegral.Prepartition.iUnion_def, BoxIntegral.Prepartition.restrict, Set.inter_iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ (π.biUnion πi).restrict J = πi J

Tactic:
(eq_of_boxes_subset_iUnion_superset (fun J₁ h₁ => ?_) ?_).symm

Premises used: BoxIntegral.Prepartition.eq_of_boxes_subset_iUnion_superset, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
refine_1 : ∀ (J₁ : Box ι) (h₁ : J₁ ∈ (πi J).boxes), J₁ ∈ ((π.biUnion πi).restrict J).boxes
refine_2 : ((π.biUnion πi).restrict J).iUnion ⊆ (πi J).iUnion
⊢ (π.biUnion πi).restrict J = πi J

Tactic:
refine (eq_of_boxes_subset_iUnion_superset (fun J₁ h₁ => ?_) ?_).symm

Premises used: BoxIntegral.Prepartition.eq_of_boxes_subset_iUnion_superset, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ J₁ ∈ ((π.biUnion πi).restrict J).boxes

Tactic:
(mem_restrict _).2 ⟨J₁, π.mem_biUnion.2 ⟨J, hJ, h₁⟩, (inf_of_le_right ?_).symm⟩

Premises used: Iff.mpr, BoxIntegral.Prepartition.mem_biUnion, inf_of_le_right, And.intro, Exists.intro, BoxIntegral.Prepartition.mem_restrict, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
refine_1 : (↑J₁ : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))
⊢ J₁ ∈ ((π.biUnion πi).restrict J).boxes

Tactic:
refine (mem_restrict _).2 ⟨J₁, π.mem_biUnion.2 ⟨J, hJ, h₁⟩, (inf_of_le_right ?_).symm⟩

Premises used: Iff.mpr, BoxIntegral.Prepartition.mem_biUnion, inf_of_le_right, And.intro, Exists.intro, BoxIntegral.Prepartition.mem_restrict, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ (↑J₁ : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))

Tactic:
WithBot.coe_le_coe.2 (le_of_mem _ h₁)

Premises used: Iff.mpr, BoxIntegral.Prepartition.le_of_mem, WithBot.coe_le_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ (↑J₁ : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))

Tactic:
exact WithBot.coe_le_coe.2 (le_of_mem _ h₁)

Premises used: Iff.mpr, BoxIntegral.Prepartition.le_of_mem, WithBot.coe_le_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
refine_2 : ∀ (x : ι → ℝ), (x ∈ (↑J : Set (ι → ℝ)) ∧ ∃ (i : Box ι) (_ : i ∈ π), x ∈ (πi i).iUnion) → x ∈ (πi J).iUnion
⊢ ((π.biUnion πi).restrict J).iUnion ⊆ (πi J).iUnion

Tactic:
simp only [iUnion_restrict, iUnion_biUnion, Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion]

Premises used: Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion, BoxIntegral.Prepartition.iUnion_biUnion, BoxIntegral.Prepartition.iUnion_restrict
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ (↑J : Set (ι → ℝ))
J₁ : Box ι
h₁ : J₁ ∈ π
hx : x ∈ (πi J₁).iUnion
⊢ J = J₁

Tactic:
π.eq_of_mem_of_mem hJ h₁ hxJ (iUnion_subset _ hx)

Premises used: BoxIntegral.Prepartition.eq_of_mem_of_mem, BoxIntegral.Prepartition.iUnion_subset
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ (↑J : Set (ι → ℝ))
J₁ : Box ι
h₁ : J₁ ∈ π
hx : x ∈ (πi J₁).iUnion
⊢ J ∈ π

Tactic:
obtain rfl : J = J₁ := π.eq_of_mem_of_mem hJ h₁ hxJ (iUnion_subset _ hx)

Premises used: BoxIntegral.Prepartition.eq_of_mem_of_mem, BoxIntegral.Prepartition.iUnion_subset, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ (↑J : Set (ι → ℝ))
J₁ : Box ι
h₁ : J₁ ∈ π
hx : x ∈ (πi J₁).iUnion
h₂ : J ∈ π
⊢ x ∈ (πi J).iUnion

Tactic:
obtain rfl : J = J₁ := π.eq_of_mem_of_mem hJ h₁ hxJ (iUnion_subset _ hx)

Premises used: BoxIntegral.Prepartition.eq_of_mem_of_mem, BoxIntegral.Prepartition.iUnion_subset, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ (↑J : Set (ι → ℝ))
h₁ : J ∈ π
hx : x ∈ (πi J).iUnion
⊢ x ∈ (πi J).iUnion

Tactic:
hx
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ (↑J : Set (ι → ℝ))
h₁ : J ∈ π
hx : x ∈ (πi J).iUnion
⊢ x ∈ (πi J).iUnion

Tactic:
exact hx
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
mp : π.biUnion πi ≤ π' → ∀ J ∈ π, πi J ≤ π'.restrict J
mpr : (∀ J ∈ π, πi J ≤ π'.restrict J) → π.biUnion πi ≤ π'
⊢ π.biUnion πi ≤ π' ↔ ∀ J ∈ π, πi J ≤ π'.restrict J

Tactic:
constructor
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π.biUnion πi ≤ π'
J : Box ι
hJ : J ∈ π
mp : (π.biUnion πi).restrict J ≤ π'.restrict J
⊢ πi J ≤ π'.restrict J

Tactic:
rw [← π.restrict_biUnion πi hJ]

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

Tactic:
restrict_mono H

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

Tactic:
exact restrict_mono H

Premises used: BoxIntegral.Prepartition.restrict_mono
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J : Box ι
hJ : J ∈ π.biUnion πi
⊢ ∃ J' ∈ π, J ∈ πi J'

Tactic:
rw [mem_biUnion] at hJ

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
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J : Box ι
hJ : ∃ J' ∈ π, J ∈ πi J'
mpr : ∀ (J₁ : Box ι) (h₁ : J₁ ∈ π) (hJ : J ∈ πi J₁), ∃ I' ∈ π', J ≤ I'
⊢ ∃ I' ∈ π', J ≤ I'

Tactic:
rcases hJ with ⟨J₁, h₁, hJ⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
mpr : ∀ (J₂ : Box ι) (h₂ : J₂ ∈ π'.restrict J₁) (Hle : J ≤ J₂), ∃ I' ∈ π', J ≤ I'
⊢ ∃ I' ∈ π', J ≤ I'

Tactic:
rcases H J₁ h₁ hJ with ⟨J₂, h₂, Hle⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ π'.restrict J₁
Hle : J ≤ J₂
mpr :
  ∀ (J₃ : Box ι) (h₃ : J₃ ∈ π') (H : (↑J₂ : WithBot (Box ι)) = (↑J₁ : WithBot (Box ι)) ⊓ (↑J₃ : WithBot (Box ι))),
    ∃ I' ∈ π', J ≤ I'
⊢ ∃ I' ∈ π', J ≤ I'

Tactic:
rcases π'.mem_restrict.mp h₂ with ⟨J₃, h₃, H⟩

Premises used: Iff.mp, BoxIntegral.Prepartition.mem_restrict
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H_1 : ∀ J ∈ π, πi J ≤ π'.restrict J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ π'.restrict J₁
Hle : J ≤ J₂
J₃ : Box ι
h₃ : J₃ ∈ π'
H : (↑J₂ : WithBot (Box ι)) = (↑J₁ : WithBot (Box ι)) ⊓ (↑J₃ : WithBot (Box ι))
⊢ ∃ I' ∈ π', J ≤ I'

Tactic:
⟨J₃, h₃, Hle.trans <| WithBot.coe_le_coe.1 <| H.trans_le inf_le_right⟩

Premises used: inf_le_right, Eq.trans_le, WithBot.coe_le_coe, And.intro, Exists.intro, Iff.mp, LE.le.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H_1 : ∀ J ∈ π, πi J ≤ π'.restrict J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ π'.restrict J₁
Hle : J ≤ J₂
J₃ : Box ι
h₃ : J₃ ∈ π'
H : (↑J₂ : WithBot (Box ι)) = (↑J₁ : WithBot (Box ι)) ⊓ (↑J₃ : WithBot (Box ι))
⊢ ∃ I' ∈ π', J ≤ I'

Tactic:
exact ⟨J₃, h₃, Hle.trans <| WithBot.coe_le_coe.1 <| H.trans_le inf_le_right⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ π' ≤ π.biUnion πi ↔ π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J

Tactic:
⟨fun H => ⟨H.trans (π.biUnion_le πi), fun J hJ => ?_⟩, ?_⟩

Premises used: BoxIntegral.Prepartition.biUnion_le, And.intro, Iff.intro, LE.le.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
refine_1 : ∀ (H : π' ≤ π.biUnion πi) (J : Box ι) (hJ : J ∈ π), π'.restrict J ≤ πi J
refine_2 : (π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J) → π' ≤ π.biUnion πi
⊢ π' ≤ π.biUnion πi ↔ π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J

Tactic:
refine ⟨fun H => ⟨H.trans (π.biUnion_le πi), fun J hJ => ?_⟩, ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π.biUnion πi
J : Box ι
hJ : J ∈ π
refine_1 : π'.restrict J ≤ (π.biUnion πi).restrict J
⊢ π'.restrict J ≤ πi J

Tactic:
rw [← π.restrict_biUnion πi hJ]

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

Tactic:
restrict_mono H

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

Tactic:
exact restrict_mono H

Premises used: BoxIntegral.Prepartition.restrict_mono
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
refine_2 : ∀ (J : Box ι) (hJ : J ∈ π) (hle : J' ≤ J), ∃ I' ∈ π.biUnion πi, J' ≤ I'
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Tactic:
rcases H hJ' with ⟨J, hJ, hle⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
⊢ J' ∈ π'.restrict J

Tactic:
have : J' ∈ π'.restrict J :=
      π'.mem_restrict.2 ⟨J', hJ', (inf_of_le_right <| WithBot.coe_le_coe.2 hle).symm⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ π'.restrict J
refine_2 : ∀ (Ji : Box ι) (hJi : Ji ∈ πi J) (hlei : J' ≤ Ji), ∃ I' ∈ π.biUnion πi, J' ≤ I'
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Tactic:
rcases Hi J hJ this with ⟨Ji, hJi, hlei⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ π'.restrict J
Ji : Box ι
hJi : Ji ∈ πi J
hlei : J' ≤ Ji
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Tactic:
⟨Ji, π.mem_biUnion.2 ⟨J, hJ, hJi⟩, hlei⟩

Premises used: Iff.mpr, BoxIntegral.Prepartition.mem_biUnion, And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ π'.restrict J
Ji : Box ι
hJi : Ji ∈ πi J
hlei : J' ≤ Ji
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Tactic:
exact ⟨Ji, π.mem_biUnion.2 ⟨J, hJ, hJi⟩, hlei⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
⊢ π₁ ⊓ π₂ = π₁.biUnion fun (J : Box ι) ↦ π₂.restrict J

Tactic:
rfl

Premises used: rfl