awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
π : TaggedPrepartition I
h : π.IsSubordinate r
hJ : J ∈ π.boxes
⊢ diam.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J) ≤ 2 * (↑(r (π.tag J)) : ℝ)

Tactic:
calc
    diam (Box.Icc J) ≤ diam (closedBall (π.tag J) (r <| π.tag J)) :=
      diam_mono (h J hJ) isBounded_closedBall
    _ ≤ 2 * r (π.tag J) := diam_closedBall (le_of_lt (r _).2)

Premises used: Metric.isBounded_closedBall, Metric.diam_mono, Trans.trans, le_of_lt, Metric.diam_closedBall, Subtype.property
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
x : ι → ℝ
J' : Box ι
hJ : J ≤ I
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
⊢ J' ∈ single I J hJ x h ↔ J' = J

Tactic:
Finset.mem_singleton

Premises used: Finset.mem_singleton, Set.Mem, setOf
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
x : ι → ℝ
hJ : J ≤ I
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
⊢ (single I J hJ x h).IsPartition ↔ J = I

Tactic:
Prepartition.isPartition_single_iff hJ

Premises used: BoxIntegral.Prepartition.single, BoxIntegral.TaggedPrepartition.IsPartition, BoxIntegral.Prepartition.isPartition_single_iff
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
x : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
⊢ (single I I ⋯ x h).IsPartition

Tactic:
Prepartition.isPartitionTop I

Premises used: BoxIntegral.Prepartition.isPartitionTop, BoxIntegral.TaggedPrepartition.IsPartition
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
x : ι → ℝ
p : (ι → ℝ) → Box ι → Prop
hJ : J ≤ I
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
⊢ (∀ J' ∈ single I J hJ x h, p ((single I J hJ x h).tag J') J') ↔ p x J

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
x : ι → ℝ
hJ : J ≤ I
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
⊢ (single I J hJ x h).IsHenstock ↔
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x

Tactic:
forall_mem_single (fun x J => x ∈ Box.Icc J) hJ h

Premises used: BoxIntegral.Box.Icc, Membership.mem, BoxIntegral.TaggedPrepartition.forall_mem_single, BoxIntegral.TaggedPrepartition.IsHenstock, DFunLike.coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
x : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
⊢ (single I I ⋯ x h).IsHenstock

Tactic:
(isHenstock_single_iff (le_refl I) h).2 h

Premises used: Iff.mpr, le_refl, BoxIntegral.TaggedPrepartition.isHenstock_single_iff
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
x : ι → ℝ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
hJ : J ≤ I
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
⊢ (single I J hJ x h).IsSubordinate r ↔ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall x (↑(r x) : ℝ)

Tactic:
forall_mem_single (fun x J => Box.Icc J ⊆ closedBall x (r x)) hJ h

Premises used: BoxIntegral.Box.Icc, BoxIntegral.TaggedPrepartition.IsSubordinate, HasSubset.Subset, BoxIntegral.TaggedPrepartition.forall_mem_single, Metric.closedBall, Subtype.val, DFunLike.coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
x : ι → ℝ
hJ : J ≤ I
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
⊢ (single I J hJ x h).iUnion = (↑J : Set (ι → ℝ))

Tactic:
Prepartition.iUnion_single hJ

Premises used: BoxIntegral.Prepartition.single, BoxIntegral.TaggedPrepartition.iUnion, BoxIntegral.Prepartition.iUnion_single
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J_1 : Box ι
π π₁_1 π₂_1 : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
pos :
  J ∈ π₁.boxes → Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (π₁.tag J)
neg :
  J ∉ π₁.boxes → Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (π₂.tag J)
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))
    (if J ∈ π₁.boxes then π₁.tag J else π₂.tag J)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J_1 : Box ι
π π₁_1 π₂_1 : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
h_1 : J ∈ π₁.boxes
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (π₁.tag J)

Tactic:
π₁.tag_mem_Icc J

Premises used: BoxIntegral.TaggedPrepartition.tag_mem_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J_1 : Box ι
π π₁_1 π₂_1 : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
h_1 : J ∉ π₁.boxes
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (π₂.tag J)

Tactic:
π₂.tag_mem_Icc J

Premises used: BoxIntegral.TaggedPrepartition.tag_mem_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J_1 : Box ι
π π₁_1 π₂_1 : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
h_1 : J ∈ π₁.boxes
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (π₁.tag J)

Tactic:
exacts [π₁.tag_mem_Icc J, π₂.tag_mem_Icc J]

Premises used: BoxIntegral.TaggedPrepartition.tag_mem_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).boxes = π₁.boxes ∪ π₂.boxes

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : TaggedPrepartition 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.Tagged
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : TaggedPrepartition 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.Tagged
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : TaggedPrepartition 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.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion

Tactic:
Prepartition.iUnion_disjUnion h

Premises used: BoxIntegral.Prepartition.iUnion_disjUnion, BoxIntegral.TaggedPrepartition.iUnion, BoxIntegral.Prepartition.disjUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
hJ : J ∈ π₁
⊢ (π₁.disjUnion π₂ h).tag J = π₁.tag J

Tactic:
dif_pos hJ

Premises used: dif_pos, Finset.piecewise, dite, ite
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
hJ : J ∈ π₂
⊢ (π₁.disjUnion π₂ h).tag J = π₂.tag J

Tactic:
dif_neg fun h₁ => h.le_bot ⟨π₁.subset_iUnion h₁ J.upper_mem, π₂.subset_iUnion hJ J.upper_mem⟩

Premises used: Disjoint.le_bot, Finset.piecewise, dif_neg, dite, BoxIntegral.TaggedPrepartition.subset_iUnion, And.intro, BoxIntegral.Box.upper_mem, ite
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).IsSubordinate r

Tactic:
fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_

Premises used: BoxIntegral.TaggedPrepartition.IsSubordinate, Iff.mp, Finset.mem_union, Or.elim
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
refine_1 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
      closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
refine_2 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₂.boxes),
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
      closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
⊢ (π₁.disjUnion π₂ h).IsSubordinate r

Tactic:
refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_

Premises used: Iff.mp, Finset.mem_union, Or.elim
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
refine_1 : (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall (π₁.tag J) (↑(r (π₁.tag J)) : ℝ)
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
    closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)

Tactic:
rw [disjUnion_tag_of_mem_left _ hJ]

Premises used: BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall (π₁.tag J) (↑(r (π₁.tag J)) : ℝ)

Tactic:
h₁ _ hJ
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall (π₁.tag J) (↑(r (π₁.tag J)) : ℝ)

Tactic:
exact h₁ _ hJ
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
refine_2 : (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall (π₂.tag J) (↑(r (π₂.tag J)) : ℝ)
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
    closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)

Tactic:
rw [disjUnion_tag_of_mem_right _ hJ]

Premises used: BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_right
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall (π₂.tag J) (↑(r (π₂.tag J)) : ℝ)

Tactic:
h₂ _ hJ
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall (π₂.tag J) (↑(r (π₂.tag J)) : ℝ)

Tactic:
exact h₂ _ hJ
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
refine_1 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
      closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
refine_2 refine_2₁ :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₂.boxes),
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
      closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
⊢ (π₁.disjUnion π₂ h).IsSubordinate r

Tactic:
classical
  refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
  · rw [disjUnion_tag_of_mem_left _ hJ]
    exact h₁ _ hJ
  · rw [disjUnion_tag_of_mem_right _ hJ]
    exact h₂ _ hJ

Premises used: Iff.mp, Finset.mem_union, Or.elim
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).IsHenstock

Tactic:
fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_

Premises used: Iff.mp, Finset.mem_union, Or.elim, BoxIntegral.TaggedPrepartition.IsHenstock
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
refine_1 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((π₁.disjUnion π₂ h).tag J)
refine_2 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₂.boxes),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((π₁.disjUnion π₂ h).tag J)
⊢ (π₁.disjUnion π₂ h).IsHenstock

Tactic:
refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_

Premises used: Iff.mp, Finset.mem_union, Or.elim
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
refine_1 : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π₁.tag J)
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) ((π₁.disjUnion π₂ h).tag J)

Tactic:
rw [disjUnion_tag_of_mem_left _ hJ]

Premises used: BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π₁.tag J)

Tactic:
h₁ _ hJ
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π₁.tag J)

Tactic:
exact h₁ _ hJ
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
refine_2 : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π₂.tag J)
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) ((π₁.disjUnion π₂ h).tag J)

Tactic:
rw [disjUnion_tag_of_mem_right _ hJ]

Premises used: BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_right
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π₂.tag J)

Tactic:
h₂ _ hJ
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π₂.tag J)

Tactic:
exact h₂ _ hJ
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
refine_1 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((π₁.disjUnion π₂ h).tag J)
refine_2 refine_2₁ :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₂.boxes),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((π₁.disjUnion π₂ h).tag J)
⊢ (π₁.disjUnion π₂ h).IsHenstock

Tactic:
classical
  refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
  · rw [disjUnion_tag_of_mem_left _ hJ]
    exact h₁ _ hJ
  · rw [disjUnion_tag_of_mem_right _ hJ]
    exact h₂ _ hJ

Premises used: Iff.mp, Finset.mem_union, Or.elim
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I_1 J_1 : Box ι
π π₁ π₂ : TaggedPrepartition I_1
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
I J : Box ι
h : I ≤ J
t₁ : Box ι → ι → ℝ
ht₁ : ∀ (J : Box ι), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (t₁ J)
b₁ : Finset (Box ι)
h₁le : ∀ J ∈ b₁, J ≤ I
h₁d : (↑b₁ : Set (Box ι)).Pairwise (Disjoint on Box.toSet)
t₂ : Box ι → ι → ℝ
ht₂ : ∀ (J : Box ι), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (t₂ J)
b₂ : Finset (Box ι)
h₂le : ∀ J ∈ b₂, J ≤ I
h₂d : (↑b₂ : Set (Box ι)).Pairwise (Disjoint on Box.toSet)
H :
  Eq.{u_1 + 1} (α := TaggedPrepartition J)
    ((fun (π : TaggedPrepartition I) ↦
        ({ boxes := π.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯, tag := π.tag, tag_mem_Icc := ⋯ } :
          TaggedPrepartition J))
      { boxes := b₁, le_of_mem' := h₁le, pairwiseDisjoint := h₁d, tag := t₁, tag_mem_Icc := ht₁ })
    ((fun (π : TaggedPrepartition I) ↦
        ({ boxes := π.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯, tag := π.tag, tag_mem_Icc := ⋯ } :
          TaggedPrepartition J))
      { boxes := b₂, le_of_mem' := h₂le, pairwiseDisjoint := h₂d, tag := t₂, tag_mem_Icc := ht₂ })
⊢ { boxes := b₁, le_of_mem' := h₁le, pairwiseDisjoint := h₁d, tag := t₁, tag_mem_Icc := ht₁ : TaggedPrepartition I } =
    { boxes := b₂, le_of_mem' := h₂le, pairwiseDisjoint := h₂d, tag := t₂, tag_mem_Icc := ht₂ }

Tactic:
simpa using H
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : J ∈ π
⊢ J.distortion ≤ π.distortion

Tactic:
le_sup h

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

Tactic:
Finset.sup_le_iff

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

Tactic:
sup_biUnion _ _

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

Tactic:
exact sup_biUnion _ _

Premises used: Finset.sup_biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
inst : Fintype ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (π.biUnionTagged π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.Tagged
Goal:
ι : Type u_1
I : Box ι
inst : Fintype ι
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnionPrepartition πi).distortion = π.boxes.sup fun (J : Box ι) ↦ (πi J).distortion

Tactic:
sup_biUnion _ _

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

Tactic:
exact sup_biUnion _ _

Premises used: Finset.sup_biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
inst : Fintype ι
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnionPrepartition π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.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
inst : Fintype ι
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion

Tactic:
sup_union

Premises used: BoxIntegral.Prepartition.distortion, Finset.sup_union, BoxIntegral.TaggedPrepartition.distortion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition 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.Tagged
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition 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.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition 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, BoxIntegral.TaggedPrepartition.distortion, Finset.sup_congr, rfl, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I J : Box ι
x : ι → ℝ
inst : Fintype ι
hJ : J ≤ I
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
⊢ (single I J hJ x h).distortion = J.distortion

Tactic:
sup_singleton

Premises used: Finset.sup_singleton, BoxIntegral.Prepartition.distortion, BoxIntegral.TaggedPrepartition.distortion