α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ (∀ (i : ι), i ∈ sι → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ sι → ∀ (j : ι), j ∈ sι → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ sι), S i) = ∑ i in sι, T (S i)
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
hSp : ∀ (i : ι), i ∈ sι → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ sι → ∀ (j : ι), j ∈ sι → i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ (i : ι) (_ : i ∈ sι), S i) = ∑ i in sι, T (S i)
revert hSp h_disj
case refine'_1
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ (∀ (i : ι), i ∈ ∅ → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ ∅), S i) = ∑ i in ∅, T (S i)

case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
          (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
            T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)) →
        (∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤) →
          (∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)) →
            T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = ∑ i in insert a s, T (S i)
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ (∀ (i : ι), i ∈ sι → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ sι → ∀ (j : ι), j ∈ sι → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ sι), S i) = ∑ i in sι, T (S i)
refine' Finset.induction_on sι _ _
case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = ∑ i in insert a s, T (S i)
case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
          (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
            T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)) →
        (∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤) →
          (∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)) →
            T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = ∑ i in insert a s, T (S i)
intro a s has h hps h_disj
case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = T (S a) + T (⋃ (i : ι) (_ : i ∈ s), S i)

case refine'_2.hSp
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤

case refine'_2.h_disj
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)
case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = ∑ i in insert a s, T (S i)
rw [Finset.sum_insert has, ← h]
case refine'_2.hSp
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤

case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = T (S a) + T (⋃ (i : ι) (_ : i ∈ s), S i)

case refine'_2.h_disj
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)
case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = T (S a) + T (⋃ (i : ι) (_ : i ∈ s), S i)

case refine'_2.hSp
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤

case refine'_2.h_disj
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)
swap
case refine'_2.h_disj
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)

case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = T (S a) + T (⋃ (i : ι) (_ : i ∈ s), S i)
case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = T (S a) + T (⋃ (i : ι) (_ : i ∈ s), S i)

case refine'_2.h_disj
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)
swap
case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = T (S a ∪ ⋃ (i : ι) (_ : i ∈ s), S i)

case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ↑↑μ (⋃ (i : ι) (_ : i ∈ s), S i) ≠ ⊤

case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ (S a ∩ ⋃ (i : ι) (_ : i ∈ s), S i) = ∅
case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = T (S a) + T (⋃ (i : ι) (_ : i ∈ s), S i)
rw [←
  h_add (S a) (⋃ i ∈ s, S i) (hS_meas a) (measurableSet_biUnion _ fun i _ => hS_meas i)
    (hps a (Finset.mem_insert_self a s))]
no goals
case refine'_1
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ (∀ (i : ι), i ∈ ∅ → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ ∅), S i) = ∑ i in ∅, T (S i)
simp only [Finset.not_mem_empty, IsEmpty.forall_iff, iUnion_false, iUnion_empty, sum_empty,
  forall₂_true_iff, imp_true_iff, forall_true_left, not_false_iff, T_empty]
no goals
case refine'_2.hSp
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤
exact fun i hi => hps i (Finset.mem_insert_of_mem hi)
no goals
case refine'_2.h_disj
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)
exact fun i hi j hj hij =>
  h_disj i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij
case refine'_2.e_a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ (⋃ (i : ι) (_ : i ∈ insert a s), S i) = S a ∪ ⋃ (i : ι) (_ : i ∈ s), S i
case refine'_2
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ (i : ι) (_ : i ∈ insert a s), S i) = T (S a ∪ ⋃ (i : ι) (_ : i ∈ s), S i)
congr
no goals
case refine'_2.e_a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ (⋃ (i : ι) (_ : i ∈ insert a s), S i) = S a ∪ ⋃ (i : ι) (_ : i ∈ s), S i
convert Finset.iSup_insert a s S
no goals
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ ↑↑μ (⋃ (i : ι) (_ : i ∈ s), S i) ≠ ⊤
exact
  ((measure_biUnion_finset_le _ _).trans_lt <|
      ENNReal.sum_lt_top fun i hi => hps i <| Finset.mem_insert_of_mem hi).ne
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ (⋃ (i : ι) (_ : i ∈ s), S a ∩ S i) = ∅
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ (S a ∩ ⋃ (i : ι) (_ : i ∈ s), S i) = ∅
simp_rw [Set.inter_iUnion]
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
i : ι
hi : i ∈ s
⊢ S a ∩ S i = ∅
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
⊢ (⋃ (i : ι) (_ : i ∈ s), S a ∩ S i) = ∅
refine' iUnion_eq_empty.mpr fun i => iUnion_eq_empty.mpr fun hi => _
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
i : ι
hi : i ∈ s
⊢ Disjoint (S a) (S i)
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
i : ι
hi : i ∈ s
⊢ S a ∩ S i = ∅
rw [← Set.disjoint_iff_inter_eq_empty]
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
i : ι
hi : i ∈ s
hai : a = i
⊢ False
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
i : ι
hi : i ∈ s
⊢ Disjoint (S a) (S i)
refine' h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai => _
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
i : ι
hi : a ∈ s
hai : a = i
⊢ False
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
i : ι
hi : i ∈ s
hai : a = i
⊢ False
rw [← hai] at hi
no goals
case refine'_2.a
α : Type u_1
E : Type ?u.37144
F : Type ?u.37147
F' : Type ?u.37150
G : Type ?u.37153
𝕜 : Type ?u.37156
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T✝ T' T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_3
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : ¬a ∈ s
h :
  (∀ (i : ι), i ∈ s → ↑↑μ (S i) ≠ ⊤) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ (i : ι) (_ : i ∈ s), S i) = ∑ i in s, T (S i)
hps : ∀ (i : ι), i ∈ insert a s → ↑↑μ (S i) ≠ ⊤
h_disj : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → Disjoint (S i) (S j)
i : ι
hi : a ∈ s
hai : a = i
⊢ False
exact has hi