awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : AddCancelMonoid β
T : Set α → β
h_empty : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
hT : T ∅ = T ∅ + T ∅
⊢ T ∅ + 0 = T ∅ + T ∅

Tactic:
nth_rw 1 [← add_zero (T ∅)] at hT

Premises used: EmptyCollection.emptyCollection, add_zero
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : AddCancelMonoid β
T : Set α → β
h_empty : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
hT : T ∅ + 0 = T ∅ + T ∅
⊢ T ∅ = 0

Tactic:
(add_left_cancel hT).symm

Premises used: add_left_cancel, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : AddCancelMonoid β
T : Set α → β
h_empty : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
hT : T ∅ + 0 = T ∅ + T ∅
⊢ T ∅ = 0

Tactic:
exact (add_left_cancel hT).symm

Premises used: add_left_cancel, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T T' : Set α → β
inst : AddCommMonoid β
hT : FinMeasAdditive μ T
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
simp : T s + T t + (T' s + T' t) = T s + T' s + (T t + T' t)
⊢ (T + T') (s ∪ t) = (T + T') s + (T + T') t

Tactic:
simp only [hT s t hs ht hμs hμt hst, hT' s t hs ht hμs hμt hst, Pi.add_apply]

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T T' : Set α → β
inst : AddCommMonoid β
hT : FinMeasAdditive μ T
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' s + T' t) = T s + T' s + (T t + T' t)

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T T' : Set α → β
inst : AddCommMonoid β
ν : Measure α
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive ν T'
⊢ FinMeasAdditive (μ + ν) (T + T')

Tactic:
hT.add_right_measure.add (hT'.add_left_measure)

Premises used: MeasureTheory.FinMeasAdditive.add, MeasureTheory.FinMeasAdditive.add_left_measure, MeasureTheory.FinMeasAdditive.add_right_measure
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)

Tactic:
revert hSp h_disj
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)

Tactic:
Finset.induction_on sι ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
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 :
  ∀ (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)
⊢ ∀ (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:
refine Finset.induction_on sι ?_ ?_
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 : ι), 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:
simp only [Finset.notMem_empty, IsEmpty.forall_iff, iUnion_false, iUnion_empty, sum_empty,
      imp_true_iff, T_empty]

Premises used: imp_true_iff, Finset.notMem_empty, Set.iUnion_false, Finset.sum_empty, Set.iUnion_empty, IsEmpty.forall_iff
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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∞)
refine_2₂ : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)

Tactic:
rw [Finset.sum_insert has, ← h]

Premises used: Finset.sum_insert
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
fun i hi => hps i (Finset.mem_insert_of_mem hi)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact fun i hi => hps i (Finset.mem_insert_of_mem hi)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)

Tactic:
fun i hi j hj hij =>
      h_disj i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)

Tactic:
exact fun i hi j hj hij =>
      h_disj i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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∞)
refine_2₂ : Disjoint (S a) (⋃ i ∈ s, S i)
⊢ T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ 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))]

Premises used: Finset.mem_insert_self, Set.iUnion, Finset.measurableSet_biUnion
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 : ⋃ i ∈ insert a s, S i = S a ∪ ⋃ i ∈ s, S i
⊢ T (⋃ i ∈ insert a s, S i) = T (S a ∪ ⋃ i ∈ s, S i)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
⊢ ⨆ x ∈ insert a s, S x = S a ⊔ ⨆ x ∈ s, S x

Tactic:
Finset.iSup_insert a s S

Premises used: Finset.iSup_insert
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 ∈ insert a s, S i = S a ∪ ⋃ i ∈ s, S i

Tactic:
convert! Finset.iSup_insert a s S

Premises used: Finset.iSup_insert
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, S i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_biUnion_lt_top s.finite_toSet fun i hi ↦
      (hps i <| Finset.mem_insert_of_mem hi).lt_top).ne

Premises used: MeasureTheory.measure_biUnion_lt_top, Finset.mem_insert_of_mem, Ne.lt_top, Finset.finite_toSet, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, S i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact (measure_biUnion_lt_top s.finite_toSet fun i hi ↦
      (hps i <| Finset.mem_insert_of_mem hi).lt_top).ne

Premises used: MeasureTheory.measure_biUnion_lt_top, Finset.mem_insert_of_mem, Ne.lt_top, Finset.finite_toSet, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 : ∀ (i : ι) (i_1 : i ∈ s), Disjoint (S a) (S i)
⊢ Disjoint (S a) (⋃ i ∈ s, S i)

Tactic:
simp_rw [Set.disjoint_iUnion_right]

Premises used: Set.disjoint_iUnion_right
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)

Tactic:
h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai ↦ ?_

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
refine_2 : ∀ (hai : a = i), False
⊢ Disjoint (S a) (S i)

Tactic:
refine h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai ↦ ?_

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
⊢ a ∈ s

Tactic:
rw [← hai] at hi
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
hi₁ : a ∈ s
⊢ a = i

Tactic:
rw [← hai] at hi
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 : a ∈ s
hai : a = i
⊢ False

Tactic:
has hi
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 : a ∈ s
hai : a = i
⊢ False

Tactic:
exact has hi
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
rw₂ rw₃ : T (t ∪ s) = T (t ∪ s)
⊢ T s + T 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]

Premises used: Set.union_comm, Disjoint.symm
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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

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]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_comm : T s + T t = T t + T s
⊢ (-T) (s ∪ t) = (-T) s + (-T) t

Tactic:
simp_all [hT s t hs ht hμs hμt hst, neg_add_rev]

Premises used: neg_add_rev
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T T' : Set α → β
inst : AddCommGroup β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
⊢ FinMeasAdditive μ (T - T')

Tactic:
sub_eq_add_neg T T' ▸ hT.add hT'.neg

Premises used: sub_eq_add_neg, MeasureTheory.FinMeasAdditive.add, Eq.rec, MeasureTheory.FinMeasAdditive.neg, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
β : Type u_7
inst : SeminormedAddCommGroup β
C : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive.{u_1, u_7} (β := β) μ 0 C

Tactic:
⟨FinMeasAdditive.zero, fun s _ _ => ?_⟩

Premises used: MeasureTheory.DominatedFinMeasAdditive, And.intro, MeasureTheory.FinMeasAdditive.zero