-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c x ε) : ℝ) →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c x ε) : ℝ) →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
set set₁ :
  ∃ (ia : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀ (x : TaggedPrepartition I),
        Membership.mem (γ := Set (TaggedPrepartition I))
            {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π ∧ π.IsPartition} x →
          Membership.mem (γ := Set F) (Metric.closedBall ((g : (a : Box ι) → F) I) ε : Set F) (integralSum f vol x)
set₂ :
  let δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦
    if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε';
  ∀ (x : TaggedPrepartition I),
    Membership.mem (γ := Set (TaggedPrepartition I))
        {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (δ c) π ∧ π.IsPartition} x →
      Membership.mem (γ := Set F) (Metric.closedBall ((g : (a : Box ι) → F) I) ε : Set F) (integralSum f vol x)
set₃ :
  let δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦
    if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε';
  ∀ (x : TaggedPrepartition I),
    (∃ (c : ℝ≥0), l.MemBaseSet I c (δ c) x ∧ x.IsPartition) →
      Membership.mem (γ := Set F) (Metric.closedBall ((g : (a : Box ι) → F) I) ε : Set F) (integralSum f vol x)
set₄ :
  let δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦
    if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε';
  ∀ (π : TaggedPrepartition I) (c : ℝ≥0) (hπδ : l.MemBaseSet I c (δ c) π) (hπp : π.IsPartition),
    Membership.mem (γ := Set F) (Metric.closedBall ((g : (a : Box ι) → F) I) ε : Set F) (integralSum f vol π)
set₅ :
  let δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦
    if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε';
  ∀ (π : TaggedPrepartition I) (c : ℝ≥0) (hπδ : l.MemBaseSet I c (δ c) π) (hπp : π.IsPartition),
    dist
        (HAdd.hAdd (α := F)
          (∑ x ∈ π.boxes with π.tag x ∈ s,
            (((vol : (a : Box ι) → E →L[ℝ] F) x : E →L[ℝ] F) : (a : E) → F) (f (π.tag x)))
          (∑ x ∈ π.boxes with π.tag x ∉ s,
            (((vol : (a : Box ι) → E →L[ℝ] F) x : E →L[ℝ] F) : (a : E) → F) (f (π.tag x))))
        (HAdd.hAdd (α := F) (∑ x ∈ π.boxes with π.tag x ∈ s, (g : (a : Box ι) → F) x)
          (∑ x ∈ π.boxes with π.tag x ∉ s, (g : (a : Box ι) → F) x)) ≤
      ε / 2 + ε / 2
refine_1 :
  let δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦
    if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε';
  ∀ (π : TaggedPrepartition I) (c : ℝ≥0) (hπδ : l.MemBaseSet I c (δ c) π) (hπp : π.IsPartition),
    dist.{w} (α := F)
        (∑ x ∈ π.boxes with π.tag x ∈ s, (((vol : (a : Box ι) → E →L[ℝ] F) x : E →L[ℝ] F) : (a : E) → F) (f (π.tag x)))
        (∑ x ∈ π.boxes with π.tag x ∈ s, (g : (a : Box ι) → F) x) ≤
      ε / 2
refine_2 refine_2₁ :
  let δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦
    if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε';
  ∀ (π : TaggedPrepartition I) (c : ℝ≥0) (hπδ : l.MemBaseSet I c (δ c) π) (hπp : π.IsPartition),
    dist.{w} (α := F)
        (∑ x ∈ π.boxes with π.tag x ∉ s, (((vol : (a : Box ι) → E →L[ℝ] F) x : E →L[ℝ] F) : (a : E) → F) (f (π.tag x)))
        (∑ x ∈ π.boxes with π.tag x ∉ s, (g : (a : Box ι) → F) x) ≤
      ε / 2
⊢ ∃ (ia : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀ (x : TaggedPrepartition I),
        Membership.mem (γ := Set (TaggedPrepartition I))
            {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π ∧ π.IsPartition} x →
          Membership.mem (γ := Set F) (Metric.closedBall ((g : (a : Box ι) → F) I) ε : Set F) (integralSum f vol x)

Tactic:
classical
  set δ : ℝ≥0 → ℝⁿ → Ioi (0 : ℝ) := fun c x => if x ∈ s then δ₁ c x (εs x) else (δ₂ c) x ε'
  refine ⟨δ, fun c => l.rCond_of_bRiemann_eq_false hl, ?_⟩
  simp only [mem_setOf_eq]
  rintro π ⟨c, hπδ, hπp⟩
  -- Now we split the sum into two parts based on whether `π.tag J` belongs to `s` or not.
  rw [← g.sum_partition_boxes le_rfl hπp, Metric.mem_closedBall, integralSum,
    ← sum_filter_add_sum_filter_not π.boxes fun J => π.tag J ∈ s,
    ← sum_filter_add_sum_filter_not π.boxes fun J => π.tag J ∈ s, ← add_halves ε]
  refine dist_add_add_le_of_le ?_ ?_
  · rcases s.eq_empty_or_nonempty with (rfl | hsne); · simp [ε0'.le]
    /- For the boxes such that `π.tag J ∈ s`, we use the fact that at most `2 ^ #ι` boxes have the
        same tag. -/
    specialize hlH hsne
    have : ∀ J ∈ {J ∈ π.boxes | π.tag J ∈ s},
        dist (vol J (f <| π.tag J)) (g J) ≤ εs (π.tag J) := fun J hJ ↦ by
      rw [Finset.mem_filter] at hJ; obtain ⟨hJ, hJs⟩ := hJ
      refine Hδ₁ c _ ⟨π.tag_mem_Icc _, hJs⟩ _ (hεs0 _) _ (π.le_of_mem' _ hJ) ?_
        (hπδ.2 hlH J hJ) fun hD => (Finset.le_sup hJ).trans (hπδ.3 hD)
      convert! hπδ.1 J hJ using 3; exact (if_pos hJs).symm
    refine (dist_sum_sum_le_of_le _ this).trans ?_
    rw [sum_comp]
    refine (sum_le_sum ?_).trans (hεs _ ?_)
    · rintro b -
      rw [← Nat.cast_two, ← Nat.cast_pow, ← nsmul_eq_mul]
      refine nsmul_le_nsmul_left (hεs0 _).le ?_
      refine (Finset.card_le_card ?_).trans ((hπδ.isHenstock hlH).card_filter_tag_eq_le b)
      exact filter_subset_filter _ (filter_subset _ _)
    · rw [Finset.coe_image, Set.image_subset_iff]
      exact fun J hJ => (Finset.mem_filter.1 hJ).2
  /- Now we deal with boxes such that `π.tag J ∉ s`.
    In this case the estimate is straightforward. -/
  calc
    dist (∑ J ∈ π.boxes with tag π J ∉ s, vol J (f (tag π J)))
      (∑ J ∈ π.boxes with tag π J ∉ s, g J)
      ≤ ∑ J ∈ π.boxes with tag π J ∉ s, ε' * B J := dist_sum_sum_le_of_le _ fun J hJ ↦ by
      rw [Finset.mem_filter] at hJ; obtain ⟨hJ, hJs⟩ := hJ
      refine Hδ₂ c _ ⟨π.tag_mem_Icc _, hJs⟩ _ ε'0 _ (π.le_of_mem' _ hJ) ?_ (fun hH => hπδ.2 hH J hJ)
        fun hD => (Finset.le_sup hJ).trans (hπδ.3 hD)
      convert! hπδ.1 J hJ using 3; exact (if_neg hJs).symm
    _ ≤ ∑ J ∈ π.boxes, ε' * B J := by
      gcongr
      · exact fun _ _ _ ↦ mul_nonneg ε'0.le (hB0 _)
      · apply filter_subset
    _ = B I * ε' := by rw [← mul_sum, B.sum_partition_boxes le_rfl hπp, mul_comm]
    _ ≤ ε / 2 := hεI.le

Premises used: Finset.filter_subset_filter, add_halves, BoxIntegral.integralSum, Finset.filter_subset, Finset.coe_image, Finset.sum_comp, LT.lt.le, Set.mem_setOf_eq, nsmul_le_nsmul_left, dist_add_add_le_of_le, Set.eq_empty_or_nonempty, And.right, dist_sum_sum_le_of_le, Iff.mp, nsmul_eq_mul, Finset.mem_filter, Finset.sum_le_sum, Set.image_subset_iff, Metric.mem_closedBall, Nat.cast_pow, LE.le.trans, DFunLike.coe, Nat.cast_two, rfl