-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem tendsto_integralSum_sum_integral (h : Integrable I l f vol) (π₀ : Prepartition I) :
    Tendsto (integralSum f vol) (l.toFilteriUnion I π₀)
      (𝓝 <| ∑ J ∈ π₀.boxes, integral J l f vol)

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
ε : ℝ
ε0 : 0 < ε
⊢ ∃ ia,
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.iUnion = π₀.iUnion},
        integralSum f vol x ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε

Tactic:
refine ⟨h.convergenceR ε, h.convergenceR_cond ε, ?_⟩

Result:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
ε : ℝ
ε0 : 0 < ε
⊢ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR ε c) π ∧ π.iUnion = π₀.iUnion},
    integralSum f vol x ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
ε : ℝ
ε0 : 0 < ε
⊢ ∀ (x : TaggedPrepartition I),
    (∃ c, l.MemBaseSet I c (h.convergenceR ε c) x ∧ x.iUnion = π₀.iUnion) →
      integralSum f vol x ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε

Tactic:
rintro π ⟨c, hc, hU⟩

Result:
case intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
ε : ℝ
ε0 : 0 < ε
π : TaggedPrepartition I
c : ℝ≥0
hc : l.MemBaseSet I c (h.convergenceR ε c) π
hU : π.iUnion = π₀.iUnion
⊢ integralSum f vol π ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
ε : ℝ
ε0 : 0 < ε
⊢ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR ε c) π ∧ π.iUnion = π₀.iUnion},
    integralSum f vol x ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε

Tactic:
simp only [mem_inter_iff, Set.mem_iUnion, mem_setOf_eq]

Result:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
ε : ℝ
ε0 : 0 < ε
⊢ ∀ (x : TaggedPrepartition I),
    (∃ c, l.MemBaseSet I c (h.convergenceR ε c) x ∧ x.iUnion = π₀.iUnion) →
      integralSum f vol x ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε

Proof state:
case intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
ε : ℝ
ε0 : 0 < ε
π : TaggedPrepartition I
c : ℝ≥0
hc : l.MemBaseSet I c (h.convergenceR ε c) π
hU : π.iUnion = π₀.iUnion
⊢ integralSum f vol π ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε

Tactic:
exact h.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq ε0 hc hU

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Tendsto (integralSum f vol) (toFilteriUnion I π₀) (𝓝 (∑ J ∈ π₀.boxes, integral J l f vol))

Tactic:
refine ((l.hasBasis_toFilteriUnion I π₀).tendsto_iff nhds_basis_closedBall).2 fun ε ε0 => ?_

Result:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
ε : ℝ
ε0 : 0 < ε
⊢ ∃ ia,
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.iUnion = π₀.iUnion},
        integralSum f vol x ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε