awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
⊢ J ∈ π₁ ⊓ π₂ ↔ ∃ J₁ ∈ π₁, ∃ J₂ ∈ π₂, (↑J : WithBot (Box ι)) = (↑J₁ : WithBot (Box ι)) ⊓ (↑J₂ : WithBot (Box ι))

Tactic:
simp only [inf_def, mem_biUnion, mem_restrict]

Premises used: BoxIntegral.Prepartition.mem_biUnion, BoxIntegral.Prepartition.inf_def, BoxIntegral.Prepartition.mem_restrict
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
⊢ (π₁ ⊓ π₂).iUnion = π₁.iUnion ∩ π₂.iUnion

Tactic:
simp only [inf_def, iUnion_biUnion, iUnion_restrict, ← iUnion_inter, ← iUnion_def]

Premises used: BoxIntegral.Prepartition.iUnion_def, Set.iUnion_inter, BoxIntegral.Prepartition.iUnion_biUnion, BoxIntegral.Prepartition.iUnion_restrict, BoxIntegral.Prepartition.inf_def
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ J ∈ π.filter p ↔ J ∈ π ∧ p J

Tactic:
Finset.mem_filter

Premises used: Set.Mem, setOf, Finset.mem_filter
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ J ∈ π.filter p ↔ J ∈ π ∧ p J

Tactic:
exact Finset.mem_filter

Premises used: Finset.mem_filter
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ J ∈ π.filter p ↔ J ∈ π ∧ p J

Tactic:
classical
  exact Finset.mem_filter

Premises used: Finset.mem_filter
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ π.filter p ≤ π

Tactic:
fun J hJ =>
  let ⟨hπ, _⟩ := π.mem_filter.1 hJ
  ⟨J, hπ, le_rfl⟩

Premises used: le_rfl, Membership.mem, Exists, BoxIntegral.Prepartition.mem_filter, LE.le, And, _private.0.BoxIntegral.Prepartition.filter_le.match_1, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
hp : ∀ J ∈ π, p J
h : ∀ (J : Box ι), J ∈ π.filter p ↔ J ∈ π
⊢ π.filter p = π

Tactic:
ext J
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
hp : ∀ J ∈ π, p J
J : Box ι
⊢ J ∈ π.filter p ↔ J ∈ π

Tactic:
simpa using hp J
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ (π.filter fun (x : Box ι) ↦ True) = π

Tactic:
π.filter_of_true fun _ _ => trivial

Premises used: trivial, BoxIntegral.Prepartition.filter_of_true
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ))
    (⋃ i ∈ (↑π.boxes : Set (Box ι)) \ (↑(π.filter p).boxes : Set (Box ι)), (↑i : Set (ι → ℝ)))
    ((⋃ i ∈ (↑π.boxes : Set (Box ι)), (↑i : Set (ι → ℝ))) \
      ⋃ i ∈ (↑(π.filter p).boxes : Set (Box ι)), (↑i : Set (ι → ℝ)))

Tactic:
(@Set.biUnion_diff_biUnion_eq (ι → ℝ) (Box ι) π.boxes (π.filter p).boxes (↑) _).symm

Premises used: Eq.symm, Set.biUnion_diff_biUnion_eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
h :
  ∀ (x : Box ι),
    (x ∈ π.filter fun (J : Box ι) ↦ ¬p J) ↔ x ∈ (↑π.boxes : Set (Box ι)) \ (↑(π.filter p).boxes : Set (Box ι))
using : ((↑π.boxes : Set (Box ι)) ∪ (↑(π.filter p).boxes : Set (Box ι))).PairwiseDisjoint Box.toSet
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ J ∈ π.filter fun (J : Box ι) ↦ ¬p J, (↑J : Set (ι → ℝ)))
    ((⋃ J ∈ π, (↑J : Set (ι → ℝ))) \ ⋃ J ∈ π.filter p, (↑J : Set (ι → ℝ)))

Tactic:
convert!
    (@Set.biUnion_diff_biUnion_eq (ι → ℝ) (Box ι) π.boxes (π.filter p).boxes (↑) _).symm using 4

Premises used: Eq.symm, Set.biUnion_diff_biUnion_eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
x : Box ι
⊢ (x ∈ π.filter fun (J : Box ι) ↦ ¬p J) ↔ x ∈ (↑π.boxes : Set (Box ι)) \ (↑(π.filter p).boxes : Set (Box ι))

Tactic:
simp +contextual
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ (↑π.boxes : Set (Box ι)).Pairwise (Disjoint on Box.toSet)

Tactic:
π.pairwiseDisjoint

Premises used: BoxIntegral.Prepartition.pairwiseDisjoint
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
h : (↑π.boxes : Set (Box ι)) ∪ (↑(π.filter p).boxes : Set (Box ι)) = (↑π.boxes : Set (Box ι))
⊢ ((↑π.boxes : Set (Box ι)) ∪ (↑(π.filter p).boxes : Set (Box ι))).Pairwise (Disjoint on Box.toSet)

Tactic:
convert! π.pairwiseDisjoint

Premises used: BoxIntegral.Prepartition.pairwiseDisjoint
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
h : {x : Box ι | x ∈ π.boxes ∧ p x} ⊆ (↑π.boxes : Set (Box ι))
⊢ (↑π.boxes : Set (Box ι)) ∪ (↑(π.filter p).boxes : Set (Box ι)) = (↑π.boxes : Set (Box ι))

Tactic:
rw [Set.union_eq_left, filter_boxes, coe_filter]

Premises used: Set.union_eq_left, Finset.coe_filter, BoxIntegral.Prepartition.filter_boxes
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ {x : Box ι | x ∈ π.boxes ∧ p x} ⊆ (↑π.boxes : Set (Box ι))

Tactic:
fun _ ⟨h, _⟩ => h

Premises used: Membership.mem, BoxIntegral.Prepartition.boxes, Set.Subset, _private.0.BoxIntegral.Prepartition.iUnion_filter_not.match_1, SetLike.coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ {x : Box ι | x ∈ π.boxes ∧ p x} ⊆ (↑π.boxes : Set (Box ι))

Tactic:
exact fun _ ⟨h, _⟩ => h
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
α : Type u_2
M : Type u_3
inst : AddCommMonoid M
π : Prepartition I
f : Box ι → α
g : Box ι → M
⊢ Eq.{u_3 + 1} (α := M) (∑ j ∈ Finset.image f π.boxes, ∑ i ∈ π.boxes with f i = j, g i) (∑ i ∈ π.boxes, g i)

Tactic:
sum_fiberwise_of_maps_to (fun _ => Finset.mem_image_of_mem f) g

Premises used: Finset.sum_fiberwise_of_maps_to, Finset.mem_image_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
α : Type u_2
M : Type u_3
inst : AddCommMonoid M
π : Prepartition I
f : Box ι → α
g : Box ι → M
⊢ Eq.{u_3 + 1} (α := M) (∑ y ∈ Finset.image f π.boxes, ∑ J ∈ (π.filter fun (J : Box ι) ↦ f J = y).boxes, g J)
    (∑ J ∈ π.boxes, g J)

Tactic:
convert! sum_fiberwise_of_maps_to (fun _ => Finset.mem_image_of_mem f) g

Premises used: Finset.sum_fiberwise_of_maps_to, Finset.mem_image_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
h : Disjoint π₁.iUnion π₂.iUnion
this : ∀ J₁ ∈ π₁, ∀ J₂ ∈ π₂, J₁ ≠ J₂ → Disjoint (↑J₁ : Set (ι → ℝ)) (↑J₂ : Set (ι → ℝ))
⊢ (↑(π₁.boxes ∪ π₂.boxes) : Set (Box ι)).Pairwise (Disjoint on Box.toSet)

Tactic:
simpa [pairwise_union_of_symmetric (symmetric_disjoint.comap _), pairwiseDisjoint]

Premises used: Symmetric.comap, BoxIntegral.Prepartition.pairwiseDisjoint, Set.pairwise_union_of_symmetric, symmetric_disjoint
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
H : Disjoint π₁.iUnion π₂.iUnion
⊢ J ∈ π₁.disjUnion π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂

Tactic:
Finset.mem_union

Premises used: Set.Mem, setOf, Finset.mem_union
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
H : Disjoint π₁.iUnion π₂.iUnion
⊢ J ∈ π₁.disjUnion π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂

Tactic:
exact Finset.mem_union

Premises used: Finset.mem_union
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
H : Disjoint π₁.iUnion π₂.iUnion
⊢ J ∈ π₁.disjUnion π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂

Tactic:
classical exact Finset.mem_union

Premises used: Finset.mem_union
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion

Tactic:
simp [disjUnion, Prepartition.iUnion, iUnion_or, iUnion_union_distrib]

Premises used: Set.iUnion_union_distrib, BoxIntegral.Prepartition.disjUnion, Set.iUnion_or, BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
M : Type u_2
inst : AddCommMonoid M
h : Disjoint π₁.iUnion π₂.iUnion
f : Box ι → M
⊢ ∑ J ∈ π₁.boxes ∪ π₂.boxes, f J = HAdd.hAdd (α := M) (∑ J ∈ π₁.boxes, f J) (∑ J ∈ π₂.boxes, f J)

Tactic:
sum_union <| disjoint_boxes_of_disjoint_iUnion h

Premises used: Finset.sum_union, BoxIntegral.Prepartition.disjoint_boxes_of_disjoint_iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
inst : Fintype ι
h : J ∈ π
⊢ J.distortion ≤ π.distortion

Tactic:
le_sup h

Premises used: BoxIntegral.Prepartition.distortion, Finset.le_sup
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
inst : Fintype ι
c : ℝ≥0
⊢ π.distortion ≤ c ↔ ∀ J ∈ π, J.distortion ≤ c

Tactic:
Finset.sup_le_iff

Premises used: BoxIntegral.Prepartition.distortion, Finset.sup_le_iff
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
inst : Fintype ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnion πi).distortion = π.boxes.sup fun (J : Box ι) ↦ (πi J).distortion

Tactic:
sup_biUnion _ _

Premises used: Multiset.toFinset, Finset.biUnion, BoxIntegral.Prepartition.distortion, Finset.sup_biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
inst : Fintype ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnion πi).distortion = π.boxes.sup fun (J : Box ι) ↦ (πi J).distortion

Tactic:
exact sup_biUnion _ _

Premises used: Finset.sup_biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
inst : Fintype ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnion πi).distortion = π.boxes.sup fun (J : Box ι) ↦ (πi J).distortion

Tactic:
classical exact sup_biUnion _ _

Premises used: Finset.sup_biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
inst : Fintype ι
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion

Tactic:
sup_union

Premises used: BoxIntegral.Prepartition.distortion, Finset.sup_union
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
inst : Fintype ι
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion

Tactic:
exact sup_union

Premises used: Finset.sup_union
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
inst : Fintype ι
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion

Tactic:
classical exact sup_union

Premises used: Finset.sup_union
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
inst : Fintype ι
c : ℝ≥0
h₁ : π.boxes.Nonempty
h₂ : ∀ J ∈ π, J.distortion = c
⊢ π.distortion = c

Tactic:
(sup_congr rfl h₂).trans (sup_const h₁ _)

Premises used: Finset.sup_const, BoxIntegral.Prepartition.distortion, Finset.sup_congr, rfl, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
⊢ distortion.{u_1} (ι := ι) (I := I) ⊤ = I.distortion

Tactic:
sup_singleton

Premises used: Finset.sup_singleton, BoxIntegral.Prepartition.distortion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
⊢ distortion.{u_1} (ι := ι) (I := I) ⊥ = 0

Tactic:
sup_empty

Premises used: Finset.sup_empty, BoxIntegral.Prepartition.distortion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
simp_rw : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ π.iUnion = (↑I : Set (ι → ℝ))
simp_rw₁ : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ π.iUnion ⊆ (↑I : Set (ι → ℝ)) ∧ (↑I : Set (ι → ℝ)) ⊆ π.iUnion
simp_rw₂ : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ True ∧ (↑I : Set (ι → ℝ)) ⊆ π.iUnion
simp_rw₃ : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ (↑I : Set (ι → ℝ)) ⊆ π.iUnion
simp_rw₄ : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ ∀ x ∈ (↑I : Set (ι → ℝ)), x ∈ π.iUnion
simp_rw₅ : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ ∀ x ∈ (↑I : Set (ι → ℝ)), ∃ J ∈ π, x ∈ J
⊢ π.IsPartition ↔ π.iUnion = (↑I : Set (ι → ℝ))

Tactic:
simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and, Set.subset_def,
    mem_iUnion, Box.mem_coe]

Premises used: Set.subset_def, Set.Subset.antisymm_iff, BoxIntegral.Prepartition.iUnion_subset, BoxIntegral.Box.mem_coe, BoxIntegral.Prepartition.IsPartition, true_and, BoxIntegral.Prepartition.mem_iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
h : J ≤ I
⊢ (single I J h).IsPartition ↔ J = I

Tactic:
simp [isPartition_iff_iUnion_eq]

Premises used: BoxIntegral.Prepartition.isPartition_iff_iUnion_eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ IsPartition.{u_1} (ι := ι) (I := I) ⊤

Tactic:
fun _ hx => ⟨I, mem_top.2 rfl, hx⟩

Premises used: Iff.mpr, BoxIntegral.Prepartition.IsPartition, And.intro, Exists.intro, BoxIntegral.Prepartition.mem_top, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
h : π.IsPartition
⊢ π.iUnion = (↑I : Set (ι → ℝ))

Tactic:
isPartition_iff_iUnion_eq.1 h

Premises used: Iff.mp, BoxIntegral.Prepartition.isPartition_iff_iUnion_eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
h : π.IsPartition
π₁ : Prepartition I
⊢ π₁.iUnion ⊆ π.iUnion

Tactic:
h.iUnion_eq.symm ▸ π₁.iUnion_subset

Premises used: BoxIntegral.Prepartition.IsPartition.iUnion_eq, BoxIntegral.Prepartition.iUnion_subset, Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
h : π.IsPartition
hx : x ∈ I
rcases : ∀ (J : Box ι) (h : J ∈ π) (hx : x ∈ J), ∃! J : Box ι, J ∈ π ∧ x ∈ J
⊢ ∃! J : Box ι, J ∈ π ∧ x ∈ J

Tactic:
rcases h x hx with ⟨J, h, hx⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
h_1 : π.IsPartition
hx_1 : x ∈ I
J : Box ι
h : J ∈ π
hx : x ∈ J
⊢ ∃! J : Box ι, J ∈ π ∧ x ∈ J

Tactic:
ExistsUnique.intro J ⟨h, hx⟩ fun J' ⟨h', hx'⟩ => π.eq_of_mem_of_mem h' h hx' hx

Premises used: ExistsUnique.intro, BoxIntegral.Prepartition.eq_of_mem_of_mem, And.intro, _private.0.BoxIntegral.Prepartition.IsPartition.existsUnique.match_1, Eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
h_1 : π.IsPartition
hx_1 : x ∈ I
J : Box ι
h : J ∈ π
hx : x ∈ J
⊢ ∃! J : Box ι, J ∈ π ∧ x ∈ J

Tactic:
exact ExistsUnique.intro J ⟨h, hx⟩ fun J' ⟨h', hx'⟩ => π.eq_of_mem_of_mem h' h hx' hx

Premises used: ExistsUnique.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
h : π.IsPartition
⊢ π.boxes.Nonempty

Tactic:
let ⟨J, hJ, _⟩ := h _ I.upper_mem
  ⟨J, hJ⟩

Premises used: _private.0.BoxIntegral.Prepartition.IsPartition.nonempty_boxes.match_1, BoxIntegral.Box.upper, BoxIntegral.Prepartition.boxes, Exists.intro, Finset.Nonempty, BoxIntegral.Box.upper_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h₁ : π₁.IsPartition
h₂ : π₁.boxes ⊆ π₂.boxes
⊢ π₁ = π₂

Tactic:
eq_of_boxes_subset_iUnion_superset h₂ <| h₁.iUnion_subset _

Premises used: BoxIntegral.Prepartition.eq_of_boxes_subset_iUnion_superset, BoxIntegral.Prepartition.IsPartition.iUnion_subset
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h : π₂.IsPartition
⊢ π₁ ≤ π₂ ↔ ∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J'

Tactic:
le_iff_nonempty_imp_le_and_iUnion_subset.trans <| and_iff_left <| h.iUnion_subset _

Premises used: and_iff_left, BoxIntegral.Prepartition.le_iff_nonempty_imp_le_and_iUnion_subset, Iff.trans, BoxIntegral.Prepartition.IsPartition.iUnion_subset
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
h : π.IsPartition
hi : ∀ J ∈ π, (πi J).IsPartition
⊢ (π.biUnion πi).IsPartition

Tactic:
fun x hx =>
  let ⟨J, hJ, hxi⟩ := h x hx
  let ⟨Ji, hJi, hx⟩ := hi J hJ x hxi
  ⟨Ji, π.mem_biUnion.2 ⟨J, hJ, hJi⟩, hx⟩

Premises used: Iff.mpr, BoxIntegral.Prepartition.mem_biUnion, Membership.mem, Exists, _private.0.BoxIntegral.Prepartition.IsPartition.biUnion.match_1, BoxIntegral.Prepartition.IsPartition, And, And.intro, Exists.intro, _private.0.BoxIntegral.Prepartition.IsPartition.biUnion.match_2, BoxIntegral.Prepartition.biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : π.IsPartition
hJ : J ≤ I
⊢ (π.restrict J).iUnion = (↑J : Set (ι → ℝ))

Tactic:
simp [h.iUnion_eq, hJ]

Premises used: BoxIntegral.Prepartition.IsPartition.iUnion_eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ (π₁ ⊓ π₂).iUnion = (↑I : Set (ι → ℝ))

Tactic:
simp [h₁.iUnion_eq, h₂.iUnion_eq]

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

Tactic:
(iUnion_biUnion _ _).trans <|
    iUnion_congr_of_surjective id surjective_id fun J =>
      iUnion_congr_of_surjective id surjective_id fun hJ => (h J hJ).iUnion_eq

Premises used: Set.iUnion_congr_of_surjective, BoxIntegral.Prepartition.IsPartition.iUnion_eq, id, BoxIntegral.Prepartition.iUnion_biUnion, Function.surjective_id, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h : π₂.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
⊢ π₁.iUnion ∪ π₂.iUnion = (↑I : Set (ι → ℝ))

Tactic:
simp [h, π₁.iUnion_subset]

Premises used: BoxIntegral.Prepartition.iUnion_subset
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
left :
  LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Riemann).1
right :
  LE.le (α := Boolᵒᵈ × Boolᵒᵈ) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).2
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Riemann).2
left₁ :
  LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Riemann).1
right₁ :
  LE.le (α := Boolᵒᵈ × Boolᵒᵈ) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).2
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Riemann).2
left₂ :
  LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Riemann).1
right₂ :
  LE.le (α := Boolᵒᵈ × Boolᵒᵈ) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).2
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Riemann).2
left₃ :
  LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Riemann).1
right₃ :
  LE.le (α := Boolᵒᵈ × Boolᵒᵈ) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).2
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Riemann).2
⊢ Henstock ≤ Riemann

Tactic:
trivial
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
left :
  LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) McShane).1
right :
  LE.le (α := Boolᵒᵈ × Boolᵒᵈ) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).2
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) McShane).2
left₁ :
  LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) McShane).1
right₁ :
  LE.le (α := Boolᵒᵈ × Boolᵒᵈ) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).2
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) McShane).2
left₂ :
  LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) McShane).1
right₂ :
  LE.le (α := Boolᵒᵈ × Boolᵒᵈ) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).2
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) McShane).2
left₃ :
  LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) McShane).1
right₃ :
  LE.le (α := Boolᵒᵈ × Boolᵒᵈ) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).2
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) McShane).2
⊢ Henstock ≤ McShane

Tactic:
trivial
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
l : IntegrationParams
⊢ GP ≤ l

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_2
l : IntegrationParams
hl : l.bRiemann = false
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ l.RCond r

Tactic:
simp [RCond, hl]

Premises used: BoxIntegral.IntegrationParams.RCond
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
⊢ l.toFilter I ⊓ 𝓟 {π : TaggedPrepartition I | π.iUnion = π₀.iUnion} = toFilteriUnion (l := l) I π₀

Tactic:
(iSup_inf_principal _ _).symm

Premises used: BoxIntegral.IntegrationParams.toFilterDistortioniUnion, BoxIntegral.IntegrationParams.toFilteriUnion, Set.Mem, setOf, Eq.symm, Filter.iSup_inf_principal
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l₁ l₂ : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : TaggedPrepartition I
h : l₁ ≤ l₂
hc : c₁ ≤ c₂
hr : ∀ J ∈ π, r₁ (π.tag J) ≤ r₂ (π.tag J)
hπ : l₁.MemBaseSet I c₁ r₁ π
⊢ l₂.MemBaseSet I c₂ r₂ π

Tactic:
⟨hπ.1.mono' hr, fun h₂ => hπ.2 (le_iff_imp.1 h.2.1 h₂),
    fun hD => (hπ.3 (le_iff_imp.1 h.2.2 hD)).trans hc,
    fun hD => (hπ.4 (le_iff_imp.1 h.2.2 hD)).imp fun _ hπ => ⟨hπ.1, hπ.2.trans hc⟩⟩

Premises used: BoxIntegral.TaggedPrepartition.IsSubordinate.mono', Bool.le_iff_imp, BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate, BoxIntegral.IntegrationParams.MemBaseSet.exists_compl, BoxIntegral.IntegrationParams.MemBaseSet.mk, BoxIntegral.IntegrationParams.MemBaseSet.distortion_le, BoxIntegral.IntegrationParams.MemBaseSet.isHenstock, Exists.imp, And.right, And.left, And.intro, Iff.mp, LE.le.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l₁ l₂ : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : TaggedPrepartition I
h : l₁ ≤ l₂
hc : c₁ ≤ c₂
hr :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → r₁ x ≤ r₂ x
hπ : l₁.MemBaseSet I c₁ r₁ π
⊢ l₂.MemBaseSet I c₂ r₂ π

Tactic:
hπ.mono' I h hc fun J _ => hr _ <| π.tag_mem_Icc J

Premises used: BoxIntegral.TaggedPrepartition.tag_mem_Icc, BoxIntegral.TaggedPrepartition.tag, BoxIntegral.IntegrationParams.MemBaseSet.mono'