-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
set set₁ :
  ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
set₂ set₃ :
  let r := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs';
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π) (hπp : π.IsPartition),
    dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
        (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
      ‖y‖ * (↑ε : ℝ)
set₄ :
  let r := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs';
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π) (hπp : π.IsPartition),
    dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
        (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
      (↑ε : ℝ) * ‖y‖
set₅ :
  let r := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs';
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π) (hπp : π.IsPartition),
    dist (∑ J ∈ π.boxes, HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) (s.indicator (fun (x : ι → ℝ) ↦ y) (π.tag J)))
        (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
      (↑ε : ℝ) * ‖y‖
set₆ :
  let r := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs';
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π) (hπp : π.IsPartition),
    |μ.real (π.filter fun (i : Box ι) ↦ π.tag i ∈ s).iUnion - μ.real (s ∩ (↑I : Set (ι → ℝ)))| * ‖y‖ ≤ (↑ε : ℝ) * ‖y‖
hbc hbc₁ :
  let r := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs';
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π) (hπp : π.IsPartition),
    |μ.real (π.filter fun (i : Box ι) ↦ π.tag i ∈ s).iUnion - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)
hbc₂ :
  let r := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs';
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π) (hπp : π.IsPartition),
    let t := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion;
    |μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)
hbc₃ :
  let r := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs';
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π) (hπp : π.IsPartition),
    let t := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion;
    ∀ (htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))), |μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)
hbc₄ :
  let r := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs';
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π) (hπp : π.IsPartition),
    let t := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion;
    ∀ (htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))), μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ))) ≤ (↑ε : ℝ)
hbc₅ hbc₆ :
  let r := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs';
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π) (hπp : π.IsPartition),
    let t := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion;
    ∀ (htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))), μ.real (s ∩ (↑I : Set (ι → ℝ))) - μ.real t ≤ (↑ε : ℝ)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)

Tactic:
classical
  set r : (ι → ℝ) → Ioi (0 : ℝ) := s.piecewise rs rs'
  refine ⟨fun _ => r, fun c => l.rCond_of_bRiemann_eq_false hl, fun c π hπ hπp => ?_⟩; rw [mul_comm]
  /- Then the union of boxes `J ∈ π` such that `π.tag ∈ s` includes `F` and is included by `U`,
    hence its measure is `ε`-close to the measure of `s`. -/
  dsimp [integralSum]
  simp only [dist_eq_norm, ← indicator_const_smul_apply, sum_indicator_eq_sum_filter, ← sum_smul,
    ← sub_smul, norm_smul, Real.norm_eq_abs, ← Prepartition.filter_boxes,
    ← Prepartition.measure_iUnion_toReal]
  gcongr
  set t := (π.filter (π.tag · ∈ s)).iUnion
  change abs (μ.real t - μ.real (s ∩ I)) ≤ ε
  have htU : t ⊆ U ∩ I := by
    simp only [t, TaggedPrepartition.iUnion_def, iUnion_subset_iff, TaggedPrepartition.mem_filter,
      and_imp]
    refine fun J hJ hJs x hx => ⟨hrsU _ ⟨hJs, π.tag_mem_Icc J⟩ ?_, π.le_of_mem' J hJ hx⟩
    simpa only [r, s.piecewise_eq_of_mem _ _ hJs] using hπ.1 J hJ (Box.coe_subset_Icc hx)
  refine abs_sub_le_iff.2 ⟨?_, ?_⟩
  · refine (ENNReal.le_toReal_sub B).trans (ENNReal.toReal_le_coe_of_le_coe ?_)
    refine (tsub_le_tsub (measure_mono htU) le_rfl).trans (le_measure_diff.trans ?_)
    refine (measure_mono fun x hx => ?_).trans hμU.le
    exact ⟨hx.1.1, fun hx' => hx.2 ⟨hx'.1, hx.1.2⟩⟩
  · have hμt : μ t ≠ ∞ := ((measure_mono (htU.trans inter_subset_left)).trans_lt hUt).ne
    refine (ENNReal.le_toReal_sub hμt).trans (ENNReal.toReal_le_coe_of_le_coe ?_)
    refine le_measure_diff.trans ((measure_mono ?_).trans hμF.le)
    rintro x ⟨⟨hxs, hxI⟩, hxt⟩
    refine ⟨⟨hxs, Box.coe_subset_Icc hxI⟩, fun hxF => hxt ?_⟩
    simp only [t, TaggedPrepartition.iUnion_def, TaggedPrepartition.mem_filter, Set.mem_iUnion]
    rcases hπp x hxI with ⟨J, hJπ, hxJ⟩
    refine ⟨J, ⟨hJπ, ?_⟩, hxJ⟩
    contrapose hxF
    refine hrs'F _ ⟨π.tag_mem_Icc J, hxF⟩ ?_
    simpa only [r, s.piecewise_eq_of_notMem _ _ hxF] using hπ.1 J hJπ (Box.coe_subset_Icc hxJ)

Premises used: Iff.mpr, BoxIntegral.Prepartition.measure_iUnion_toReal, Finset.sum_smul, dist_eq_norm, norm_smul, ENNReal.le_toReal_sub, BoxIntegral.Prepartition.filter_boxes, Set.mem_iUnion, sub_smul, abs_sub_le_iff, BoxIntegral.integralSum, LT.lt.le, BoxIntegral.TaggedPrepartition.mem_filter, ENNReal.toReal_le_coe_of_le_coe, And.intro, MeasureTheory.measure_mono, Finset.sum_indicator_eq_sum_filter, mul_comm, Set.indicator_const_smul_apply, BoxIntegral.TaggedPrepartition.iUnion_def, LE.le.trans, MeasureTheory.le_measure_diff, Real.norm_eq_abs