-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integrableOn_iUnion_of_summable_integral_norm {f : X → E} {s : ι → Set X}
    (hs : ∀ i : ι, MeasurableSet (s i)) (hi : ∀ i : ι, IntegrableOn f (s i) μ)
    (h : Summable fun i : ι => ∫ x : X in s i, ‖f x‖ ∂μ) : IntegrableOn f (iUnion s) μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
⊢ ∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤

Tactic:
have S' :
  Summable fun i : ι =>
    (⟨∫ x : X in s i, ‖f x‖₊ ∂μ, setIntegral_nonneg (hs i) fun x _ => NNReal.coe_nonneg _⟩ :
      NNReal) := by
  rw [← NNReal.summable_coe]; exact h

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
S' : Summable fun i => ⟨∫ (x : X) in s i, ↑‖f x‖₊ ∂μ, ⋯⟩
⊢ ∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
S' : Summable fun i => ⟨∫ (x : X) in s i, ↑‖f x‖₊ ∂μ, ⋯⟩
S'' : ∑' (a : ι), ↑⟨∫ (x : X) in s a, ↑‖f x‖₊ ∂μ, ⋯⟩ = ↑(∑' (b : ι), ⟨∫ (x : X) in s b, ↑‖f x‖₊ ∂μ, ⋯⟩)
⊢ ∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤

Tactic:
simp_rw [ENNReal.coe_nnreal_eq, NNReal.coe_mk, coe_nnnorm] at S''

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
S' : Summable fun i => ⟨∫ (x : X) in s i, ↑‖f x‖₊ ∂μ, ⋯⟩
S'' :
  ∑' (a : ι), ENNReal.ofReal (∫ (x : X) in s a, ‖f x‖ ∂μ) =
    ENNReal.ofReal ↑(∑' (b : ι), ⟨∫ (x : X) in s b, ‖f x‖ ∂μ, ⋯⟩)
⊢ ∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
⊢ ∑' (i : ι), ∫⁻ (a : X) in s i, ‖f a‖ₑ ∂μ < ⊤

Tactic:
have B := fun i => lintegral_coe_eq_integral (fun x : X => ‖f x‖₊) (hi i).norm

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
⊢ ∑' (i : ι), ∫⁻ (a : X) in s i, ‖f a‖ₑ ∂μ < ⊤

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
⊢ IntegrableOn f (iUnion s) μ

Tactic:
refine ⟨AEStronglyMeasurable.iUnion fun i => (hi i).1, (lintegral_iUnion_le _ _).trans_lt ?_⟩

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
⊢ ∑' (i : ι), ∫⁻ (a : X) in s i, ‖f a‖ₑ ∂μ < ⊤

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
⊢ ∑' (i : ι), ∫⁻ (a : X) in s i, ‖f a‖ₑ ∂μ < ⊤

Tactic:
simp_rw [enorm_eq_nnnorm, tsum_congr B]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
⊢ ∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
⊢ Summable fun i => ⟨∫ (x : X) in s i, ↑‖f x‖₊ ∂μ, ⋯⟩

Tactic:
rw [← NNReal.summable_coe]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
⊢ Summable fun a => ↑⟨∫ (x : X) in s a, ↑‖f x‖₊ ∂μ, ⋯⟩

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
S' : Summable fun i => ⟨∫ (x : X) in s i, ↑‖f x‖₊ ∂μ, ⋯⟩
S'' :
  ∑' (a : ι), ENNReal.ofReal (∫ (x : X) in s a, ‖f x‖ ∂μ) =
    ENNReal.ofReal ↑(∑' (b : ι), ⟨∫ (x : X) in s b, ‖f x‖ ∂μ, ⋯⟩)
⊢ ∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤

Tactic:
convert ENNReal.ofReal_lt_top

Result:
no goals