awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
π : Prepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ (π.toSubordinate r).IsHenstock

Tactic:
(π.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r).choose_spec.2.1

Premises used: Exists.choose_spec, BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq, And.right, And.left, BoxIntegral.Prepartition.toSubordinate
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
π : Prepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ (π.toSubordinate r).IsSubordinate r

Tactic:
(π.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r).choose_spec.2.2.1

Premises used: Exists.choose_spec, BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq, And.right, And.left, BoxIntegral.Prepartition.toSubordinate
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
π : Prepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ (π.toSubordinate r).distortion = π.distortion

Tactic:
(π.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r).choose_spec.2.2.2.1

Premises used: Exists.choose_spec, BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq, And.right, And.left, BoxIntegral.Prepartition.toSubordinate
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
π : Prepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ (π.toSubordinate r).iUnion = π.iUnion

Tactic:
(π.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r).choose_spec.2.2.2.2

Premises used: Exists.choose_spec, BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq, And.right, BoxIntegral.Prepartition.toSubordinate
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
π₁ : TaggedPrepartition I
π₂ : Prepartition I
hU : π₂.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
r : (ι → ℝ) → (↑(Ioi 0) : Type)
⊢ (π₁.unionComplToSubordinate π₂ hU r).IsPartition

Tactic:
Prepartition.isPartitionDisjUnionOfEqDiff ((π₂.iUnion_toSubordinate r).trans hU)

Premises used: BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff, BoxIntegral.Prepartition.disjUnion, BoxIntegral.TaggedPrepartition.IsPartition, BoxIntegral.Prepartition.iUnion_toSubordinate, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
π₁ : TaggedPrepartition I
π₂ : Prepartition I
hU : π₂.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
r : (ι → ℝ) → (↑(Ioi 0) : Type)
⊢ (π₁.unionComplToSubordinate π₂ hU r).boxes = π₁.boxes ∪ (π₂.toSubordinate r).boxes

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
π₁ : TaggedPrepartition I
π₂ : Prepartition I
hU : π₂.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
r : (ι → ℝ) → (↑(Ioi 0) : Type)
⊢ (π₁.unionComplToSubordinate π₂ hU r).iUnion = (↑I : Set (ι → ℝ))

Tactic:
(isPartition_unionComplToSubordinate _ _ _ _).iUnion_eq

Premises used: BoxIntegral.Prepartition.IsPartition.iUnion_eq, BoxIntegral.TaggedPrepartition.iUnion, BoxIntegral.TaggedPrepartition.isPartition_unionComplToSubordinate
-- Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
π₁ : TaggedPrepartition I
π₂ : Prepartition I
hU : π₂.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
r : (ι → ℝ) → (↑(Ioi 0) : Type)
⊢ (π₁.unionComplToSubordinate π₂ hU r).distortion = max π₁.distortion π₂.distortion

Tactic:
simp [unionComplToSubordinate]

Premises used: BoxIntegral.TaggedPrepartition.unionComplToSubordinate
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π : TaggedPrepartition I
⊢ J ∈ π.toPrepartition ↔ J ∈ π

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
f : Box ι → ι → ℝ
h : ∀ (J : Box ι), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (f J)
⊢ J ∈ { toPrepartition := π, tag := f, tag_mem_Icc := h : TaggedPrepartition I } ↔ J ∈ π

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
⊢ π.iUnion = ⋃ J ∈ π, (↑J : Set (ι → ℝ))

Tactic:
rfl

Premises used: BoxIntegral.TaggedPrepartition.iUnion, rfl, BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
f : Box ι → ι → ℝ
h : ∀ (J : Box ι), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (f J)
⊢ { toPrepartition := π, tag := f, tag_mem_Icc := h : TaggedPrepartition I }.iUnion = π.iUnion

Tactic:
rfl

Premises used: BoxIntegral.TaggedPrepartition.iUnion, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
⊢ π.iUnion = π.iUnion

Tactic:
rfl

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

Tactic:
Set.mem_iUnion₂

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

Tactic:
convert! Set.mem_iUnion₂

Premises used: Set.mem_iUnion₂
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
x_1 : Box ι
h : x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π.toPrepartition), x ∈ x_1
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 ∈ π.toPrepartition), x ∈ (↑x_1 : Set (ι → ℝ))

Tactic:
rw [Box.mem_coe, mem_toPrepartition, exists_prop]

Premises used: BoxIntegral.TaggedPrepartition.mem_toPrepartition, BoxIntegral.Box.mem_coe, exists_prop
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π : TaggedPrepartition I
h : J ∈ π
⊢ (↑J : Set (ι → ℝ)) ⊆ π.iUnion

Tactic:
subset_biUnion_of_mem h

Premises used: Set.subset_biUnion_of_mem, BoxIntegral.TaggedPrepartition.iUnion, BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
⊢ π.iUnion ⊆ (↑I : Set (ι → ℝ))

Tactic:
iUnion₂_subset π.le_of_mem'

Premises used: Set.iUnion₂_subset, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.TaggedPrepartition.iUnion, BoxIntegral.Prepartition.le_of_mem', BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
⊢ π.IsPartition ↔ π.iUnion = (↑I : Set (ι → ℝ))

Tactic:
Prepartition.isPartition_iff_iUnion_eq

Premises used: BoxIntegral.TaggedPrepartition.iUnion, BoxIntegral.Prepartition.isPartition_iff_iUnion_eq, BoxIntegral.TaggedPrepartition.IsPartition
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π : TaggedPrepartition 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.Tagged
Goal:
ι : Type u_1
I J : Box ι
π : TaggedPrepartition 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.Tagged
Goal:
ι : Type u_1
I J : Box ι
π : TaggedPrepartition 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.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
p : Box ι → Prop
⊢ (π.filter fun (J : Box ι) ↦ ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion

Tactic:
π.toPrepartition.iUnion_filter_not p

Premises used: BoxIntegral.Prepartition.filter, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.TaggedPrepartition.iUnion, BoxIntegral.Prepartition.iUnion_filter_not
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ J ∈ π.biUnionTagged πi ↔ ∃ J' ∈ π, J ∈ πi J'

Tactic:
π.mem_biUnion

Premises used: Set.Mem, BoxIntegral.Prepartition.mem_biUnion, setOf
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
rw :
  (π.biUnionTagged πi).tag J' =
    TaggedPrepartition.tag (I := π.biUnionIndex (fun (J : Box ι) ↦ (πi J).toPrepartition) J')
      (πi (π.biUnionIndex (fun (J : Box ι) ↦ (πi J).toPrepartition) J')) J'
⊢ (π.biUnionTagged πi).tag J' = (πi J).tag J'

Tactic:
rw [← π.biUnionIndex_of_mem (πi := fun J => (πi J).toPrepartition) hJ hJ']

Premises used: BoxIntegral.Prepartition.biUnionIndex_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ (π.biUnionTagged πi).tag J' =
    TaggedPrepartition.tag (I := π.biUnionIndex (fun (J : Box ι) ↦ (πi J).toPrepartition) J')
      (πi (π.biUnionIndex (fun (J : Box ι) ↦ (πi J).toPrepartition) J')) J'

Tactic:
rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (π.biUnionTagged πi).iUnion = ⋃ J ∈ π, (πi J).iUnion

Tactic:
iUnion_biUnion _ _

Premises used: BoxIntegral.TaggedPrepartition.iUnion, BoxIntegral.Prepartition.iUnion_biUnion, BoxIntegral.Prepartition.biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
simp :
  (∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
⊢ (∀ J ∈ π.biUnionTagged πi, p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'

Tactic:
simp only [mem_biUnionTagged]

Premises used: BoxIntegral.Prepartition.mem_biUnionTagged
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'

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

Premises used: BoxIntegral.TaggedPrepartition.tag, Iff.intro, _private.0.BoxIntegral.Prepartition.forall_biUnionTagged.match_1, BoxIntegral.Prepartition.biUnionTagged
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
refine_1 :
  ∀ (H : ∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J) (J : Box ι) (hJ : J ∈ π) (J' : Box ι)
    (hJ' : J' ∈ πi J), p ((πi J).tag J') J'
refine_2 :
  ∀ (H : ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J') (J' : Box ι),
    (∃ J'_1 ∈ π, J' ∈ πi J'_1) → ∀ (J : Box ι) (hJ : J ∈ π) (hJ' : J' ∈ πi J), p ((π.biUnionTagged πi).tag J') J'
⊢ (∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'

Tactic:
refine ⟨fun H J hJ J' hJ' => ?_, fun H J' ⟨J, hJ, hJ'⟩ => ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
refine_1 : p ((π.biUnionTagged πi).tag J') J'
⊢ p ((πi J).tag J') J'

Tactic:
rw [← π.tag_biUnionTagged hJ hJ']

Premises used: BoxIntegral.Prepartition.tag_biUnionTagged
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p ((π.biUnionTagged πi).tag J') J'

Tactic:
H J' ⟨J, hJ, hJ'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p ((π.biUnionTagged πi).tag J') J'

Tactic:
exact H J' ⟨J, hJ, hJ'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
J' : Box ι
h : ∃ J'_1 ∈ π, J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
refine_2 : p ((πi J).tag J') J'
⊢ p ((π.biUnionTagged πi).tag J') J'

Tactic:
rw [π.tag_biUnionTagged hJ hJ']

Premises used: BoxIntegral.Prepartition.tag_biUnionTagged
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
J' : Box ι
h : ∃ J'_1 ∈ π, J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p ((πi J).tag J') J'

Tactic:
H J hJ J' hJ'
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
J' : Box ι
h : ∃ J'_1 ∈ π, J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p ((πi J).tag J') J'

Tactic:
exact H J hJ J' hJ'
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
h : π.IsPartition
πi : (J : Box ι) → TaggedPrepartition J
hi : ∀ J ∈ π, (πi J).IsPartition
⊢ (π.biUnionTagged πi).IsPartition

Tactic:
h.biUnion hi

Premises used: BoxIntegral.Prepartition.IsPartition.biUnion, BoxIntegral.TaggedPrepartition.IsPartition, BoxIntegral.Prepartition.biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
h : π.IsPartition
πi : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π, (πi J).IsPartition
⊢ (π.biUnionPrepartition πi).IsPartition

Tactic:
h.biUnion hi

Premises used: BoxIntegral.Prepartition.IsPartition.biUnion, BoxIntegral.TaggedPrepartition.IsPartition, BoxIntegral.Prepartition.biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
π' : Prepartition I
⊢ (π.infPrepartition π').toPrepartition = π.toPrepartition ⊓ π'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : TaggedPrepartition I
⊢ J ∈ π₁.infPrepartition π₂.toPrepartition ↔ J ∈ π₂.infPrepartition π₁.toPrepartition

Tactic:
simp only [← mem_toPrepartition, infPrepartition_toPrepartition, inf_comm]

Premises used: BoxIntegral.TaggedPrepartition.mem_toPrepartition, inf_comm, BoxIntegral.TaggedPrepartition.infPrepartition_toPrepartition
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ : TaggedPrepartition I
h₁ : π₁.IsPartition
π₂ : Prepartition I
h₂ : π₂.IsPartition
⊢ (π₁.infPrepartition π₂).IsPartition

Tactic:
h₁.inf h₂

Premises used: BoxIntegral.Prepartition.IsPartition.inf, BoxIntegral.TaggedPrepartition.IsPartition
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (π.biUnionTagged πi).IsHenstock ↔ ∀ J ∈ π, (πi J).IsHenstock

Tactic:
π.forall_biUnionTagged (fun x J => x ∈ Box.Icc J) πi

Premises used: BoxIntegral.Box.Icc, Membership.mem, BoxIntegral.Prepartition.forall_biUnionTagged, BoxIntegral.TaggedPrepartition.IsHenstock, DFunLike.coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
⊢ #({J ∈ π.boxes | π.tag J = x}) ≤
    #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x})

Tactic:
Finset.card_le_card fun J hJ => ?_

Premises used: Finset.card_le_card
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
refine :
  ∀ (J : Box ι) (hJ : J ∈ {J ∈ π.boxes | π.tag J = x}),
    J ∈ {J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}
⊢ #({J ∈ π.boxes | π.tag J = x}) ≤
    #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x})

Tactic:
refine Finset.card_le_card fun J hJ => ?_

Premises used: Finset.card_le_card
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J : Box ι
hJ : J ∈ {J ∈ π.boxes | π.tag J = x}
rw :
  ∀ (hJ : J ∈ π.boxes ∧ π.tag J = x),
    J ∈ π.boxes ∧ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x
⊢ J ∈ {J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}

Tactic:
rw [Finset.mem_filter] at hJ ⊢

Premises used: Finset.mem_filter
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J : Box ι
hJ : J ∈ π.boxes ∧ π.tag J = x
rcases :
  ∀ (hJ : J ∈ π.boxes),
    J ∈ π.boxes ∧ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π.tag J)
⊢ J ∈ π.boxes ∧ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x

Tactic:
rcases hJ with ⟨hJ, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
J : Box ι
hJ : J ∈ π.boxes
⊢ J ∈ π.boxes ∧ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π.tag J)

Tactic:
⟨hJ, h J hJ⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
J : Box ι
hJ : J ∈ π.boxes
⊢ J ∈ π.boxes ∧ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π.tag J)

Tactic:
exact ⟨hJ, h J hJ⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
⊢ #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card ι)

Tactic:
π.toPrepartition.card_filter_mem_Icc_le x

Premises used: BoxIntegral.Prepartition.card_filter_mem_Icc_le, BoxIntegral.TaggedPrepartition.toPrepartition
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J :
  #({J ∈ π.boxes | π.tag J = x}) ≤
    #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x})
⊢ #({J ∈ π.boxes | π.tag J = x}) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card ι)

Tactic:
calc
    #{J ∈ π.boxes | π.tag J = x} ≤ #{J ∈ π.boxes | x ∈ Box.Icc J} := by
      refine Finset.card_le_card fun J hJ => ?_
      rw [Finset.mem_filter] at hJ ⊢; rcases hJ with ⟨hJ, rfl⟩
      exact ⟨hJ, h J hJ⟩
    _ ≤ 2 ^ Fintype.card ι := π.toPrepartition.card_filter_mem_Icc_le x

Premises used: BoxIntegral.Prepartition.card_filter_mem_Icc_le, Fintype.card, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.Prepartition.boxes
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J :
  #({J ∈ π.boxes | π.tag J = x}) ≤
    #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x})
⊢ #({J ∈ π.boxes | π.tag J = x}) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card ι)

Tactic:
classical
  calc
    #{J ∈ π.boxes | π.tag J = x} ≤ #{J ∈ π.boxes | x ∈ Box.Icc J} := by
      refine Finset.card_le_card fun J hJ => ?_
      rw [Finset.mem_filter] at hJ ⊢; rcases hJ with ⟨hJ, rfl⟩
      exact ⟨hJ, h J hJ⟩
    _ ≤ 2 ^ Fintype.card ι := π.toPrepartition.card_filter_mem_Icc_le x

Premises used: BoxIntegral.Prepartition.card_filter_mem_Icc_le, Fintype.card, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.Prepartition.boxes
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (π.biUnionTagged πi).IsSubordinate r ↔ ∀ J ∈ π, (πi J).IsSubordinate r

Tactic:
π.forall_biUnionTagged (fun x J => Box.Icc J ⊆ closedBall x (r x)) πi

Premises used: BoxIntegral.Box.Icc, BoxIntegral.TaggedPrepartition.IsSubordinate, HasSubset.Subset, BoxIntegral.Prepartition.forall_biUnionTagged, Metric.closedBall, Subtype.val, DFunLike.coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h : π.IsSubordinate r
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnionPrepartition πi).IsSubordinate r

Tactic:
fun _ hJ => Subset.trans (Box.le_iff_Icc.1 <| π.toPrepartition.le_biUnionIndex hJ) <|
    h _ <| π.toPrepartition.biUnionIndex_mem hJ

Premises used: BoxIntegral.Box.le_iff_Icc, Set.Subset.trans, BoxIntegral.Prepartition.biUnionIndex, BoxIntegral.Prepartition.biUnionIndex_mem, BoxIntegral.TaggedPrepartition.IsSubordinate, BoxIntegral.Prepartition.le_biUnionIndex, BoxIntegral.TaggedPrepartition.toPrepartition, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h : π.IsSubordinate r
π' : Prepartition I
⊢ (π.infPrepartition π').IsSubordinate r

Tactic:
h.biUnionPrepartition _

Premises used: BoxIntegral.TaggedPrepartition.infPrepartition, BoxIntegral.TaggedPrepartition.IsSubordinate.biUnionPrepartition
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
π : TaggedPrepartition I
hr₁ : π.IsSubordinate r₁
h : ∀ J ∈ π, r₁ (π.tag J) ≤ r₂ (π.tag J)
⊢ π.IsSubordinate r₂

Tactic:
fun _ hJ _ hx => closedBall_subset_closedBall (h _ hJ) (hr₁ _ hJ hx)

Premises used: BoxIntegral.TaggedPrepartition.IsSubordinate, Set.Subset, Metric.closedBall_subset_closedBall
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
π : TaggedPrepartition I
hr₁ : π.IsSubordinate r₁
h :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → r₁ x ≤ r₂ x
⊢ π.IsSubordinate r₂

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

Premises used: BoxIntegral.TaggedPrepartition.IsSubordinate.mono', BoxIntegral.TaggedPrepartition.tag_mem_Icc, BoxIntegral.TaggedPrepartition.tag