awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ r₁ π₁
h₂ : l.MemBaseSet I c₂ r₂ π₂
hU : π₁.iUnion = π₂.iUnion
inr :
  ∀
    (H :
      ∀ {ι : Type u_1} [inst : Fintype ι] {I : Box ι} {c₁ c₂ : ℝ≥0} {l : IntegrationParams}
        {r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)} {π₁ π₂ : TaggedPrepartition I} (h₁ : l.MemBaseSet I c₁ r₁ π₁)
        (h₂ : l.MemBaseSet I c₂ r₂ π₂) (hU : π₁.iUnion = π₂.iUnion) (hc : c₁ ≤ c₂),
        ∃ (π : Prepartition I),
          π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
            (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂))
    (hc : ¬c₁ ≤ c₂),
    ∃ (π : Prepartition I),
      π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
        (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
wlog :
  ∀ {ι : Type u_1} [inst : Fintype ι] {I : Box ι} {c₁ c₂ : ℝ≥0} {l : IntegrationParams}
    {r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)} {π₁ π₂ : TaggedPrepartition I} (h₁ : l.MemBaseSet I c₁ r₁ π₁)
    (h₂ : l.MemBaseSet I c₂ r₂ π₂) (hU : π₁.iUnion = π₂.iUnion) (hc : c₁ ≤ c₂),
    ∃ (π : Prepartition I),
      π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
        (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)

Tactic:
wlog hc : c₁ ≤ c₂ with H
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ r₁ π₁
h₂ : l.MemBaseSet I c₂ r₂ π₂
hU : π₁.iUnion = π₂.iUnion
H :
  ∀ {ι : Type u_1} [inst : Fintype ι] {I : Box ι} {c₁ c₂ : ℝ≥0} {l : IntegrationParams}
    {r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)} {π₁ π₂ : TaggedPrepartition I} (h₁ : l.MemBaseSet I c₁ r₁ π₁)
    (h₂ : l.MemBaseSet I c₂ r₂ π₂) (hU : π₁.iUnion = π₂.iUnion) (hc : c₁ ≤ c₂),
    ∃ (π : Prepartition I),
      π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
        (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
hc : ¬c₁ ≤ c₂
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)

Tactic:
simpa [hU, _root_.and_comm] using
      @H _ _ I c₂ c₁ l r₂ r₁ π₂ π₁ h₂ h₁ hU.symm (le_of_not_ge hc)

Premises used: le_of_not_ge, and_comm, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι_1 : Type u_1
inst : Fintype ι_1
I_1 : Box ι_1
c₁_1 c₂_1 : ℝ≥0
l_1 : IntegrationParams
r₁_1 r₂_1 : (ι_1 → ℝ) → (↑(Set.Ioi 0) : Type)
π₁_1 π₂_1 : TaggedPrepartition I_1
ι : Type u_1
inst_1 : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ r₁ π₁
h₂ : l.MemBaseSet I c₂ r₂ π₂
hU : π₁.iUnion = π₂.iUnion
hc : c₁ ≤ c₂
pos :
  ∀ (hD : l.bDistortion = true),
    ∃ (π : Prepartition I),
      π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
        (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
neg :
  ∀ (hD : ¬l.bDistortion = true),
    ∃ (π : Prepartition I),
      π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
        (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)

Tactic:
by_cases hD : (l.bDistortion : Prop)

Premises used: Bool.true, BoxIntegral.IntegrationParams.bDistortion, Eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι_1 : Type u_1
inst : Fintype ι_1
I_1 : Box ι_1
c₁_1 c₂_1 : ℝ≥0
l_1 : IntegrationParams
r₁_1 r₂_1 : (ι_1 → ℝ) → (↑(Set.Ioi 0) : Type)
π₁_1 π₂_1 : TaggedPrepartition I_1
ι : Type u_1
inst_1 : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ r₁ π₁
h₂ : l.MemBaseSet I c₂ r₂ π₂
hU : π₁.iUnion = π₂.iUnion
hc : c₁ ≤ c₂
hD : l.bDistortion = true
pos :
  ∀ (π : Prepartition I) (hπU : π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion) (hπc : π.distortion ≤ c₁),
    ∃ (π : Prepartition I),
      π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
        (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)

Tactic:
rcases h₁.4 hD with ⟨π, hπU, hπc⟩

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.exists_compl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι_1 : Type u_1
inst : Fintype ι_1
I_1 : Box ι_1
c₁_1 c₂_1 : ℝ≥0
l_1 : IntegrationParams
r₁_1 r₂_1 : (ι_1 → ℝ) → (↑(Set.Ioi 0) : Type)
π₁_1 π₂_1 : TaggedPrepartition I_1
ι : Type u_1
inst_1 : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ r₁ π₁
h₂ : l.MemBaseSet I c₂ r₂ π₂
hU : π₁.iUnion = π₂.iUnion
hc : c₁ ≤ c₂
hD : l.bDistortion = true
π : Prepartition I
hπU : π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
hπc : π.distortion ≤ c₁
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)

Tactic:
⟨π, hπU, fun _ => hπc, fun _ => hπc.trans hc⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι_1 : Type u_1
inst : Fintype ι_1
I_1 : Box ι_1
c₁_1 c₂_1 : ℝ≥0
l_1 : IntegrationParams
r₁_1 r₂_1 : (ι_1 → ℝ) → (↑(Set.Ioi 0) : Type)
π₁_1 π₂_1 : TaggedPrepartition I_1
ι : Type u_1
inst_1 : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ r₁ π₁
h₂ : l.MemBaseSet I c₂ r₂ π₂
hU : π₁.iUnion = π₂.iUnion
hc : c₁ ≤ c₂
hD : l.bDistortion = true
π : Prepartition I
hπU : π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
hπc : π.distortion ≤ c₁
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)

Tactic:
exact ⟨π, hπU, fun _ => hπc, fun _ => hπc.trans hc⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι_1 : Type u_1
inst : Fintype ι_1
I_1 : Box ι_1
c₁_1 c₂_1 : ℝ≥0
l_1 : IntegrationParams
r₁_1 r₂_1 : (ι_1 → ℝ) → (↑(Set.Ioi 0) : Type)
π₁_1 π₂_1 : TaggedPrepartition I_1
ι : Type u_1
inst_1 : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ r₁ π₁
h₂ : l.MemBaseSet I c₂ r₂ π₂
hU : π₁.iUnion = π₂.iUnion
hc : c₁ ≤ c₂
hD : ¬l.bDistortion = true
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)

Tactic:
⟨π₁.toPrepartition.compl, π₁.toPrepartition.iUnion_compl,
      fun h => (hD h).elim, fun h => (hD h).elim⟩

Premises used: False.elim, BoxIntegral.Prepartition.compl, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.Prepartition.iUnion_compl, And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι_1 : Type u_1
inst : Fintype ι_1
I_1 : Box ι_1
c₁_1 c₂_1 : ℝ≥0
l_1 : IntegrationParams
r₁_1 r₂_1 : (ι_1 → ℝ) → (↑(Set.Ioi 0) : Type)
π₁_1 π₂_1 : TaggedPrepartition I_1
ι : Type u_1
inst_1 : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ r₁ π₁
h₂ : l.MemBaseSet I c₂ r₂ π₂
hU : π₁.iUnion = π₂.iUnion
hc : c₁ ≤ c₂
hD : ¬l.bDistortion = true
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)

Tactic:
exact ⟨π₁.toPrepartition.compl, π₁.toPrepartition.iUnion_compl,
      fun h => (hD h).elim, fun h => (hD h).elim⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ : TaggedPrepartition I
hπ₁ : l.MemBaseSet I c r₁ π₁
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → r₂ x ≤ r₁ x
π₂ : Prepartition I
hU : π₂.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
hc : l.bDistortion = true → π₂.distortion ≤ c
h : l.bDistortion = true
⊢ Prepartition.iUnion (I := I) ⊥ = (↑I : Set (ι → ℝ)) \ (π₁.unionComplToSubordinate π₂ hU r₂).iUnion ∧
    Prepartition.distortion.{u_1} (ι := ι) (I := I) ⊥ ≤ c

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
⊢ l.MemBaseSet I c r (π.filter p)

Tactic:
⟨fun J hJ => hπ.1 J (π.mem_filter.1 hJ).1, fun hH J hJ => hπ.2 hH J (π.mem_filter.1 hJ).1,
    fun hD => (distortion_filter_le _ _).trans (hπ.3 hD), fun hD => ?_⟩

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate, BoxIntegral.IntegrationParams.MemBaseSet.mk, BoxIntegral.IntegrationParams.MemBaseSet.distortion_le, BoxIntegral.IntegrationParams.MemBaseSet.isHenstock, BoxIntegral.TaggedPrepartition.mem_filter, BoxIntegral.TaggedPrepartition.distortion_filter_le, And.left, Iff.mp, LE.le.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
refine :
  ∀ (hD : l.bDistortion = true),
    ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c
⊢ l.MemBaseSet I c r (π.filter p)

Tactic:
refine ⟨fun J hJ => hπ.1 J (π.mem_filter.1 hJ).1, fun hH J hJ => hπ.2 hH J (π.mem_filter.1 hJ).1,
    fun hD => (distortion_filter_le _ _).trans (hπ.3 hD), fun hD => ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
rcases :
  ∀ (π₁ : Prepartition I) (hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion) (hc : π₁.distortion ≤ c),
    ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c
⊢ ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c

Tactic:
rcases hπ.4 hD with ⟨π₁, hπ₁U, hc⟩

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.exists_compl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
⊢ Disjoint π₁.iUnion π₂.iUnion

Tactic:
simpa [π₂, hπ₁U] using disjoint_sdiff_self_left.mono_right sdiff_le

Premises used: sdiff_le, Disjoint.mono_right, disjoint_sdiff_self_left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
⊢ Disjoint π₁.iUnion π₂.iUnion

Tactic:
have : Disjoint π₁.iUnion π₂.iUnion := by
    simpa [π₂, hπ₁U] using disjoint_sdiff_self_left.mono_right sdiff_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
⊢ ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c

Tactic:
⟨π₁.disjUnion π₂.toPrepartition this, ?_, ?_⟩

Premises used: BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.Prepartition.disjUnion, And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
refine_1 : (π₁.disjUnion π₂.toPrepartition this).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
refine_2 : (π₁.disjUnion π₂.toPrepartition this).distortion ≤ c
⊢ ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c

Tactic:
refine ⟨π₁.disjUnion π₂.toPrepartition this, ?_, ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this_1 : Disjoint π₁.iUnion π₂.iUnion
this : (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
⊢ (π₁.disjUnion π₂.toPrepartition this_1).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion

Tactic:
simp [π₂, *]
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
refine_1 : (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
⊢ (π₁.disjUnion π₂.toPrepartition this).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion

Tactic:
suffices ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = ↑I \ (π.filter p).iUnion by
      simp [π₂, *]
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
⊢ (π.filter p).iUnion ⊆ π.iUnion

Tactic:
have h : (π.filter p).iUnion ⊆ π.iUnion :=
      biUnion_subset_biUnion_left (Finset.filter_subset _ _)
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
h : (π.filter p).iUnion ⊆ π.iUnion
refine_1 :
  ∀ (x : ι → ℝ),
    x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion ↔ x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
⊢ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion

Tactic:
ext x
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
h : (π.filter p).iUnion ⊆ π.iUnion
x : ι → ℝ
refine_1 :
  x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion → x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
refine_1₁ :
  x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion → x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion
⊢ x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion ↔ x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion

Tactic:
fconstructor
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
h : (π.filter p).iUnion ⊆ π.iUnion
x : ι → ℝ
hxI : x ∈ (↑I : Set (ι → ℝ))
hxπ : x ∉ π.iUnion
⊢ x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion

Tactic:
⟨hxI, mt (@h x) hxπ⟩

Premises used: Set.Mem, Set.diff, setOf, mt, And.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
h : (π.filter p).iUnion ⊆ π.iUnion
x : ι → ℝ
hxπ : x ∈ π.iUnion
hxp : x ∉ (π.filter p).iUnion
⊢ x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion

Tactic:
⟨π.iUnion_subset hxπ, hxp⟩

Premises used: Set.Mem, Set.diff, setOf, BoxIntegral.TaggedPrepartition.iUnion_subset, And.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
h : (π.filter p).iUnion ⊆ π.iUnion
x : ι → ℝ
hxI : x ∈ (↑I : Set (ι → ℝ))
hxπ : x ∉ π.iUnion
⊢ x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion

Tactic:
exacts [⟨hxI, mt (@h x) hxπ⟩, ⟨π.iUnion_subset hxπ, hxp⟩]
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
h : (π.filter p).iUnion ⊆ π.iUnion
x : ι → ℝ
hxI : x ∈ (↑I : Set (ι → ℝ))
hxp : x ∉ (π.filter p).iUnion
pos : ∀ (hxπ : x ∈ π.iUnion), x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion
neg : ∀ (hxπ : x ∉ π.iUnion), x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion
⊢ x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion

Tactic:
by_cases hxπ : x ∈ π.iUnion

Premises used: BoxIntegral.TaggedPrepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
h : (π.filter p).iUnion ⊆ π.iUnion
x : ι → ℝ
hxI : x ∈ (↑I : Set (ι → ℝ))
hxp : x ∉ (π.filter p).iUnion
hxπ : x ∈ π.iUnion
⊢ x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion

Tactic:
Or.inr ⟨hxπ, hxp⟩

Premises used: Set.union, Set.Mem, setOf, And.intro, Or.inr
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
h : (π.filter p).iUnion ⊆ π.iUnion
x : ι → ℝ
hxI : x ∈ (↑I : Set (ι → ℝ))
hxp : x ∉ (π.filter p).iUnion
hxπ : x ∉ π.iUnion
⊢ x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion

Tactic:
Or.inl ⟨hxI, hxπ⟩

Premises used: Set.union, Set.Mem, setOf, And.intro, Or.inl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
h : (π.filter p).iUnion ⊆ π.iUnion
x : ι → ℝ
hxI : x ∈ (↑I : Set (ι → ℝ))
hxp : x ∉ (π.filter p).iUnion
hxπ : x ∈ π.iUnion
⊢ x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion

Tactic:
exacts [Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩]

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
⊢ (π.filter fun (J : Box ι) ↦ ¬p J).distortion ≤ c

Tactic:
have : (π.filter fun J => ¬p J).distortion ≤ c := (distortion_filter_le _ _).trans (hπ.3 hD)
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun (J : Box ι) ↦ ¬p J
this_1 : Disjoint π₁.iUnion π₂.iUnion
this : (π.filter fun (J : Box ι) ↦ ¬p J).distortion ≤ c
⊢ (π₁.disjUnion π₂.toPrepartition this_1).distortion ≤ c

Tactic:
simpa [hc]