awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ π'.restrict J
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'
have refine_2 : ∀ (Ji : Box ι) (hJi : Ji ∈ πi J) (hlei : J' ≤ Ji), ∃ I' ∈ π.biUnion πi, J' ≤ I'
Tactic: rcases Hi J hJ this with ⟨Ji, hJi, hlei⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
hp : ∀ J ∈ π, p J
⊢ π.filter p = π
have h : ∀ (J : Box ι), J ∈ π.filter p ↔ J ∈ π
Tactic: ext J
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ J ∈ π.filter fun (J : Box ι) ↦ ¬p J, (↑J : Set (ι → ℝ)))
    ((⋃ J ∈ π, (↑J : Set (ι → ℝ))) \ ⋃ J ∈ π.filter p, (↑J : Set (ι → ℝ)))
have h : ∀ (x : Box ι),
  (x ∈ π.filter fun (J : Box ι) ↦ ¬p J) ↔ x ∈ (↑π.boxes : Set (Box ι)) \ (↑(π.filter p).boxes : Set (Box ι))
Tactic: convert!
    (@Set.biUnion_diff_biUnion_eq (ι → ℝ) (Box ι) π.boxes (π.filter p).boxes (↑) _).symm using 4
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
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 ι))
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ J ∈ π.filter fun (J : Box ι) ↦ ¬p J, (↑J : Set (ι → ℝ)))
    ((⋃ J ∈ π, (↑J : Set (ι → ℝ))) \ ⋃ J ∈ π.filter p, (↑J : Set (ι → ℝ)))
have using : ((↑π.boxes : Set (Box ι)) ∪ (↑(π.filter p).boxes : Set (Box ι))).PairwiseDisjoint Box.toSet
Tactic: convert!
    (@Set.biUnion_diff_biUnion_eq (ι → ℝ) (Box ι) π.boxes (π.filter p).boxes (↑) _).symm using 4
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ ((↑π.boxes : Set (Box ι)) ∪ (↑(π.filter p).boxes : Set (Box ι))).Pairwise (Disjoint on Box.toSet)
have h : (↑π.boxes : Set (Box ι)) ∪ (↑(π.filter p).boxes : Set (Box ι)) = (↑π.boxes : Set (Box ι))
Tactic: convert! π.pairwiseDisjoint
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ (↑π.boxes : Set (Box ι)) ∪ (↑(π.filter p).boxes : Set (Box ι)) = (↑π.boxes : Set (Box ι))
have h : {x : Box ι | x ∈ π.boxes ∧ p x} ⊆ (↑π.boxes : Set (Box ι))
Tactic: rw [Set.union_eq_left, filter_boxes, coe_filter]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π.IsPartition ↔ π.iUnion = (↑I : Set (ι → ℝ))
have simp_rw : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ π.iUnion = (↑I : Set (ι → ℝ))
Tactic: simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and, Set.subset_def,
    mem_iUnion, Box.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
simp_rw : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ π.iUnion = (↑I : Set (ι → ℝ))
⊢ π.IsPartition ↔ π.iUnion = (↑I : Set (ι → ℝ))
have simp_rw₁ : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ π.iUnion ⊆ (↑I : Set (ι → ℝ)) ∧ (↑I : Set (ι → ℝ)) ⊆ π.iUnion
Tactic: simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and, Set.subset_def,
    mem_iUnion, Box.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
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
⊢ π.IsPartition ↔ π.iUnion = (↑I : Set (ι → ℝ))
have simp_rw₂ : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ True ∧ (↑I : Set (ι → ℝ)) ⊆ π.iUnion
Tactic: simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and, Set.subset_def,
    mem_iUnion, Box.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
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
⊢ π.IsPartition ↔ π.iUnion = (↑I : Set (ι → ℝ))
have simp_rw₃ : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ (↑I : Set (ι → ℝ)) ⊆ π.iUnion
Tactic: simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and, Set.subset_def,
    mem_iUnion, Box.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
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
⊢ π.IsPartition ↔ π.iUnion = (↑I : Set (ι → ℝ))
have simp_rw₄ : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ ∀ x ∈ (↑I : Set (ι → ℝ)), x ∈ π.iUnion
Tactic: simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and, Set.subset_def,
    mem_iUnion, Box.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
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
⊢ π.IsPartition ↔ π.iUnion = (↑I : Set (ι → ℝ))
have simp_rw₅ : (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ ∀ x ∈ (↑I : Set (ι → ℝ)), ∃ J ∈ π, x ∈ J
Tactic: simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and, Set.subset_def,
    mem_iUnion, Box.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
h : π.IsPartition
hx : x ∈ I
⊢ ∃! J : Box ι, J ∈ π ∧ x ∈ J
have rcases : ∀ (J : Box ι) (h : J ∈ π) (hx : x ∈ J), ∃! J : Box ι, J ∈ π ∧ x ∈ J
Tactic: rcases h x hx with ⟨J, h, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
Goal:
⊢ Henstock ≤ Riemann
have left : LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
  ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Riemann).1
Tactic: trivial
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
Goal:
left :
  LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Riemann).1
⊢ Henstock ≤ Riemann
have right : LE.le (α := Boolᵒᵈ × Boolᵒᵈ) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).2
  ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Riemann).2
Tactic: trivial
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
Goal:
⊢ Henstock ≤ McShane
have left : LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
  ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) McShane).1
Tactic: trivial
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
Goal:
left :
  LE.le (α := Bool) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).1
    ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) McShane).1
⊢ Henstock ≤ McShane
have right : LE.le (α := Boolᵒᵈ × Boolᵒᵈ) ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) Henstock).2
  ((equivProd : (a : IntegrationParams) → Bool × Boolᵒᵈ × Boolᵒᵈ) McShane).2
Tactic: trivial
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
have 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₂)
Tactic: wlog hc : c₁ ≤ c₂ with H
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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₂)
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
have 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₂)
Tactic: wlog hc : c₁ ≤ c₂ with H
Cleared hypotheses: h₁, h₂, hU
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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₂
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
have pos : ∀ (hD : l.bDistortion = true),
  ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
Tactic: by_cases hD : (l.bDistortion : Prop)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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₂)
⊢ ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
have neg : ∀ (hD : ¬l.bDistortion = true),
  ∃ (π : Prepartition I),
    π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion ∧
      (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
Tactic: by_cases hD : (l.bDistortion : Prop)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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₂)
have 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₂)
Tactic: rcases h₁.4 hD with ⟨π, hπU, hπc⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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)
have refine : ∀ (hD : l.bDistortion = true),
  ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c
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 => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c
have rcases : ∀ (π₁ : Prepartition I) (hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion) (hc : π₁.distortion ≤ c),
  ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c
Tactic: rcases hπ.4 hD with ⟨π₁, hπ₁U, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (hypothesis)
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
⊢ ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c
have this : Disjoint π₁.iUnion π₂.iUnion
Tactic: have : Disjoint π₁.iUnion π₂.iUnion := by
    simpa [π₂, hπ₁U] using disjoint_sdiff_self_left.mono_right sdiff_le
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
have refine_1 : (π₁.disjUnion π₂.toPrepartition this).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
Tactic: refine ⟨π₁.disjUnion π₂.toPrepartition this, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c
have refine_2 : (π₁.disjUnion π₂.toPrepartition this).distortion ≤ c
Tactic: refine ⟨π₁.disjUnion π₂.toPrepartition this, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ (π₁.disjUnion π₂.toPrepartition this).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
have refine_1 : (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
Tactic: suffices ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = ↑I \ (π.filter p).iUnion by
      simp [π₂, *]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (hypothesis)
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
⊢ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
have h : (π.filter p).iUnion ⊆ π.iUnion
Tactic: have h : (π.filter p).iUnion ⊆ π.iUnion :=
      biUnion_subset_biUnion_left (Finset.filter_subset _ _)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
have refine_1 : ∀ (x : ι → ℝ),
  x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion ↔ x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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 : ι → ℝ
⊢ x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion ↔ x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
have refine_1 : x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion → x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion ↔ x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
have refine_1₁ : x ∈ (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion → x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion
have pos : ∀ (hxπ : x ∈ π.iUnion), x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion
Tactic: by_cases hxπ : x ∈ π.iUnion
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion
have neg : ∀ (hxπ : x ∉ π.iUnion), x ∈ (↑I : Set (ι → ℝ)) \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion
Tactic: by_cases hxπ : x ∈ π.iUnion
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (hypothesis)
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
⊢ (π₁.disjUnion π₂.toPrepartition this).distortion ≤ c
have this₁ : (π.filter fun (J : Box ι) ↦ ¬p J).distortion ≤ c
Tactic: have : (π.filter fun J => ¬p J).distortion ≤ c := (distortion_filter_le _ _).trans (hπ.3 hD)