no goals
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
l : IntegrationParams
f g✝ : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ ↑B J
g : ι →ᵇᵃ[↑I] F
H :
  ℝ≥0 →
    ∀ (x : ι → ℝ),
      x ∈ ↑Box.Icc I →
        ∀ (ε : ℝ),
          ε > 0 →
            ∃ δ, δ > 0 ∧ ∀ (J : Box ι), J ≤ I → ↑Box.Icc J ⊆ closedBall x δ → dist (↑(↑vol J) (f x)) (↑g J) ≤ ε * ↑B J
⊢ ∀ (c : ℝ≥0) (x : ι → ℝ),
    x ∈ ↑Box.Icc I \ ∅ →
      ∀ (ε : ℝ),
        ε > 0 →
          ∃ δ,
            δ > 0 ∧
              ∀ (J : Box ι),
                J ≤ I →
                  ↑Box.Icc J ⊆ closedBall x δ →
                    (McShane.bHenstock = true → x ∈ ↑Box.Icc J) →
                      (McShane.bDistortion = true → Box.distortion J ≤ c) → dist (↑(↑vol J) (f x)) (↑g J) ≤ ε * ↑B J
simpa only [McShane, Bool.coe_sort_false, false_imp_iff, true_imp_iff, diff_empty] using H