-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_finset_biUnion {ι : Type*} (t : Finset ι) {s : ι → Set X}
    (hs : ∀ i ∈ t, MeasurableSet (s i)) (h's : Set.Pairwise (↑t) (Disjoint on s))
    (hf : ∀ i ∈ t, IntegrableOn f (s i) μ) :
    ∫ x in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ x in s i, f x ∂μ

Proof state:
case insert
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a) ∧ ∀ x ∈ t, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ t, IntegrableOn f (s x) μ
h's : (↑t).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑t, a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ ∫ (x : X) in s a ∪ ⋃ x ∈ t, s x, f x ∂μ = ∑ i ∈ insert a t, ∫ (x : X) in s i, f x ∂μ

Tactic:
rw [setIntegral_union _ _ hf.1 (integrableOn_finset_iUnion.2 hf.2)]

Result:
case insert
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a) ∧ ∀ x ∈ t, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ t, IntegrableOn f (s x) μ
h's : (↑t).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑t, a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ ∫ (x : X) in s a, f x ∂μ + ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ insert a t, ∫ (x : X) in s i, f x ∂μ

X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a) ∧ ∀ x ∈ t, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ t, IntegrableOn f (s x) μ
h's : (↑t).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑t, a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ Disjoint (s a) (⋃ i ∈ t, s i)

X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a) ∧ ∀ x ∈ t, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ t, IntegrableOn f (s x) μ
h's : (↑t).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑t, a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ MeasurableSet (⋃ i ∈ t, s i)

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
h's : (↑t).Pairwise (Disjoint on s)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ

Tactic:
induction' t using Finset.induction_on with a t hat IH hs h's

Result:
case empty
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
hs : ∀ i ∈ ∅, MeasurableSet (s i)
h's : (↑∅).Pairwise (Disjoint on s)
hf : ∀ i ∈ ∅, IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i ∈ ∅, s i, f x ∂μ = ∑ i ∈ ∅, ∫ (x : X) in s i, f x ∂μ

case insert
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : ∀ i ∈ insert a t, MeasurableSet (s i)
h's : (↑(insert a t)).Pairwise (Disjoint on s)
hf : ∀ i ∈ insert a t, IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i ∈ insert a t, s i, f x ∂μ = ∑ i ∈ insert a t, ∫ (x : X) in s i, f x ∂μ

Proof state:
case insert
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : ∀ i ∈ insert a t, MeasurableSet (s i)
h's : (↑(insert a t)).Pairwise (Disjoint on s)
hf : ∀ i ∈ insert a t, IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i ∈ insert a t, s i, f x ∂μ = ∑ i ∈ insert a t, ∫ (x : X) in s i, f x ∂μ

Tactic:
simp only [Finset.coe_insert, Finset.forall_mem_insert, Set.pairwise_insert,
  Finset.set_biUnion_insert] at hs hf h's ⊢

Result:
case insert
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a) ∧ ∀ x ∈ t, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ t, IntegrableOn f (s x) μ
h's : (↑t).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑t, a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ ∫ (x : X) in s a ∪ ⋃ x ∈ t, s x, f x ∂μ = ∑ i ∈ insert a t, ∫ (x : X) in s i, f x ∂μ

Proof state:
case insert
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a) ∧ ∀ x ∈ t, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ t, IntegrableOn f (s x) μ
h's : (↑t).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑t, a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ ∫ (x : X) in s a, f x ∂μ + ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ insert a t, ∫ (x : X) in s i, f x ∂μ

Tactic:
rw [Finset.sum_insert hat, IH hs.2 h's.1 hf.2]

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a) ∧ ∀ x ∈ t, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ t, IntegrableOn f (s x) μ
h's : (↑t).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑t, a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ ∀ i ∈ t, Disjoint (s a) (s i)

Tactic:
exact fun i hi => (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1

Result:
no goals

Proof state:
case empty
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
hs : ∀ i ∈ ∅, MeasurableSet (s i)
h's : (↑∅).Pairwise (Disjoint on s)
hf : ∀ i ∈ ∅, IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i ∈ ∅, s i, f x ∂μ = ∑ i ∈ ∅, ∫ (x : X) in s i, f x ∂μ

Tactic:
simp

Result:
no goals