awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h :
  ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)
have refine_2 : T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
Tactic: rw [Finset.sum_insert has, ← h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h :
  ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
refine_2 : T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
⊢ T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)
have refine_2₁ : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Finset.sum_insert has, ← h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h :
  ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
refine_2 : T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
refine_2₁ : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)
have refine_2₂ : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)
Tactic: rw [Finset.sum_insert has, ← h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h :
  ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
have refine_2 : T (⋃ i ∈ insert a s, S i) = T (S a ∪ ⋃ i ∈ s, S i)
Tactic: 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))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h :
  ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
refine_2 : T (⋃ i ∈ insert a s, S i) = T (S a ∪ ⋃ i ∈ s, S i)
⊢ T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
have refine_2₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: 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))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h :
  ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
refine_2 : T (⋃ i ∈ insert a s, S i) = T (S a ∪ ⋃ i ∈ s, S i)
refine_2₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
have refine_2₂ : Disjoint (S a) (⋃ i ∈ s, S i)
Tactic: 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))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h :
  ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ i ∈ insert a s, S i) = T (S a ∪ ⋃ i ∈ s, S i)
have refine_2 : ⋃ i ∈ insert a s, S i = S a ∪ ⋃ i ∈ s, S i
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h :
  ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
⊢ Disjoint (S a) (⋃ i ∈ s, S i)
have refine_2 : ∀ (i : ι) (i_1 : i ∈ s), Disjoint (S a) (S i)
Tactic: simp_rw [Set.disjoint_iUnion_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h :
  ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
i : ι
hi : i ∈ s
⊢ Disjoint (S a) (S i)
have refine_2 : ∀ (hai : a = i), False
Tactic: refine h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h :
  ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
i : ι
hi : i ∈ s
hai : a = i
⊢ False
have hi₁ : a ∈ s
Tactic: rw [← hai] at hi
Cleared hypotheses: hi, hai
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
have revert : ∀ (hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
  (h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
Tactic: classical
  revert hSp h_disj
  refine Finset.induction_on sι ?_ ?_
  · simp only [Finset.notMem_empty, IsEmpty.forall_iff, iUnion_false, iUnion_empty, sum_empty,
      imp_true_iff, T_empty]
  intro a s has h hps h_disj
  rw [Finset.sum_insert has, ← h]
  swap; · exact fun i hi => hps i (Finset.mem_insert_of_mem hi)
  swap
  · exact fun i hi j hj hij =>
      h_disj i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij
  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))]
  · congr; convert! Finset.iSup_insert a s S
  · exact (measure_biUnion_lt_top s.finite_toSet fun i hi ↦
      (hps i <| Finset.mem_insert_of_mem hi).lt_top).ne
  · simp_rw [Set.disjoint_iUnion_right]
    intro i hi
    refine h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai ↦ ?_
    rw [← hai] at hi
    exact has hi
Cleared hypotheses: hSp, h_disj
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)
revert :
  ∀ (hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
⊢ T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
have refine_1 : ∀
  (hSp :
    ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
  (h_disj :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → Disjoint (S i) (S j)),
  T (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), S i) = ∑ i ∈ ∅, T (S i)
Tactic: classical
  revert hSp h_disj
  refine Finset.induction_on sι ?_ ?_
  · simp only [Finset.notMem_empty, IsEmpty.forall_iff, iUnion_false, iUnion_empty, sum_empty,
      imp_true_iff, T_empty]
  intro a s has h hps h_disj
  rw [Finset.sum_insert has, ← h]
  swap; · exact fun i hi => hps i (Finset.mem_insert_of_mem hi)
  swap
  · exact fun i hi j hj hij =>
      h_disj i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij
  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))]
  · congr; convert! Finset.iSup_insert a s S
  · exact (measure_biUnion_lt_top s.finite_toSet fun i hi ↦
      (hps i <| Finset.mem_insert_of_mem hi).lt_top).ne
  · simp_rw [Set.disjoint_iUnion_right]
    intro i hi
    refine h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai ↦ ?_
    rw [← hai] at hi
    exact has hi
Cleared hypotheses: hSp, h_disj
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)
revert :
  ∀ (hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
refine_1 :
  ∀
    (hSp :
      ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → Disjoint (S i) (S j)),
    T (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), S i) = ∑ i ∈ ∅, T (S i)
⊢ T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)) →
      ∀ (hSp : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
        T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)
Tactic: classical
  revert hSp h_disj
  refine Finset.induction_on sι ?_ ?_
  · simp only [Finset.notMem_empty, IsEmpty.forall_iff, iUnion_false, iUnion_empty, sum_empty,
      imp_true_iff, T_empty]
  intro a s has h hps h_disj
  rw [Finset.sum_insert has, ← h]
  swap; · exact fun i hi => hps i (Finset.mem_insert_of_mem hi)
  swap
  · exact fun i hi j hj hij =>
      h_disj i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij
  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))]
  · congr; convert! Finset.iSup_insert a s S
  · exact (measure_biUnion_lt_top s.finite_toSet fun i hi ↦
      (hps i <| Finset.mem_insert_of_mem hi).lt_top).ne
  · simp_rw [Set.disjoint_iUnion_right]
    intro i hi
    refine h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai ↦ ?_
    rw [← hai] at hi
    exact has hi
Cleared hypotheses: hSp, h_disj
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)
revert :
  ∀ (hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
refine_1 :
  ∀
    (hSp :
      ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → Disjoint (S i) (S j)),
    T (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), S i) = ∑ i ∈ ∅, T (S i)
refine_2 refine_2₁ refine_2₂ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)
⊢ T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
have refine_2₃ : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (h :
    ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
      (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
  (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
  (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
  T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
Tactic: classical
  revert hSp h_disj
  refine Finset.induction_on sι ?_ ?_
  · simp only [Finset.notMem_empty, IsEmpty.forall_iff, iUnion_false, iUnion_empty, sum_empty,
      imp_true_iff, T_empty]
  intro a s has h hps h_disj
  rw [Finset.sum_insert has, ← h]
  swap; · exact fun i hi => hps i (Finset.mem_insert_of_mem hi)
  swap
  · exact fun i hi j hj hij =>
      h_disj i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij
  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))]
  · congr; convert! Finset.iSup_insert a s S
  · exact (measure_biUnion_lt_top s.finite_toSet fun i hi ↦
      (hps i <| Finset.mem_insert_of_mem hi).lt_top).ne
  · simp_rw [Set.disjoint_iUnion_right]
    intro i hi
    refine h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai ↦ ?_
    rw [← hai] at hi
    exact has hi
Cleared hypotheses: hSp, h_disj
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddGroup β
hT : FinMeasAdditive μ T
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
⊢ T s + T t = T t + T s
have rw : T (s ∪ t) = T t + T s
Tactic: rw [← hT s t hs ht hμs hμt hst, ← hT t s ht hs hμt hμs hst.symm, union_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddGroup β
hT : FinMeasAdditive μ T
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
rw : T (s ∪ t) = T t + T s
⊢ T s + T t = T t + T s
have rw₁ : T (s ∪ t) = T (t ∪ s)
Tactic: rw [← hT s t hs ht hμs hμt hst, ← hT t s ht hs hμt hμs hst.symm, union_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddGroup β
hT : FinMeasAdditive μ T
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
rw : T (s ∪ t) = T t + T s
rw₁ : T (s ∪ t) = T (t ∪ s)
⊢ T s + T t = T t + T s
have rw₂ : T (t ∪ s) = T (t ∪ s)
Tactic: rw [← hT s t hs ht hμs hμt hst, ← hT t s ht hs hμt hμs hst.symm, union_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddGroup β
hT : FinMeasAdditive μ T
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
⊢ (-T) (s ∪ t) = (-T) s + (-T) t
have h_comm : T s + T t = T t + T s
Tactic: have h_comm : T s + T t = T t + T s := by
    rw [← hT s t hs ht hμs hμt hst, ← hT t s ht hs hμt hμs hst.symm, union_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
β : Type u_7
inst : SeminormedAddCommGroup β
C : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive.{u_1, u_7} (β := β) μ 0 C
have refine : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → norm.{u_7} (E := β) (0 s) ≤ C * μ.real s
Tactic: refine ⟨FinMeasAdditive.zero, fun s _ _ => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
β : Type u_7
inst : SeminormedAddCommGroup β
C : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ norm.{u_7} (E := β) (0 s) ≤ C * μ.real s
have rw : 0 ≤ C * μ.real s
Tactic: rw [Pi.zero_apply, norm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ T s = 0
have refine : ‖T s‖ = 0
Tactic: refine norm_eq_zero.mp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ‖T s‖ = 0
have refine : C * μ.real s = 0
Tactic: refine ((hT.2 s hs (by simp [hs_zero])).trans (le_of_eq ?_)).antisymm (norm_nonneg _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ C * μ.real s = 0
have rw : C * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) = 0
Tactic: rw [measureReal_def, hs_zero, ENNReal.toReal_zero, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : C * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) = 0
⊢ C * μ.real s = 0
have rw₁ : C * ENNReal.toReal 0 = 0
Tactic: rw [measureReal_def, hs_zero, ENNReal.toReal_zero, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : C * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) = 0
rw₁ : C * ENNReal.toReal 0 = 0
⊢ C * μ.real s = 0
have rw₂ : C * 0 = 0
Tactic: rw [measureReal_def, hs_zero, ENNReal.toReal_zero, mul_zero]