awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
n : ℕ
ih : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
succ : ∀ (i : ℕ) (i_1 : i < n), Disjoint (f n) (f i)
⊢ Disjoint (f n) (⋃ x ∈ Finset.range n, f x)

Tactic:
simp only [Finset.mem_range, Set.disjoint_iUnion_right]

Premises used: Set.disjoint_iUnion_right, Finset.mem_range
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
n : ℕ
ih : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
i : ℕ
hi : i < n
⊢ Disjoint (f n) (f i)

Tactic:
f_disj hi.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
n : ℕ
ih : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
i : ℕ
hi : i < n
⊢ Disjoint (f n) (f i)

Tactic:
exact f_disj hi.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
n : ℕ
zero : m (⋃ i ∈ Finset.range 0, f i) = ∑ i ∈ Finset.range 0, m (f i)
succ :
  ∀ (n : ℕ) (ih : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)),
    m (⋃ i ∈ Finset.range (n + 1), f i) = ∑ i ∈ Finset.range (n + 1), m (f i)
⊢ m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)

Tactic:
induction n with
      | zero => simpa using h'm ∅ ∅ MeasurableSet.empty MeasurableSet.empty (by simp)
      | succ n ih =>
        simp only [Finset.range_add_one]
        rw [Finset.sum_insert (by simp)]
        simp only [Finset.mem_insert, Set.iUnion_iUnion_eq_or_left]
        rw [h'm _ _ (f_meas n), ih]
        · exact Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i)
        · simp only [Finset.mem_range, Set.disjoint_iUnion_right]
          intro i hi
          exact f_disj hi.ne'

Premises used: MeasurableSet.empty, Finset.range_add_one, Finset.mem_insert, Set.disjoint_iUnion_right, Finset.mem_range, Set.iUnion_iUnion_eq_or_left, EmptyCollection.emptyCollection, Finset.sum_insert, Finset.measurableSet_biUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
⊢ ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)

Tactic:
have A n : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i) := by
      induction n with
      | zero => simpa using h'm ∅ ∅ MeasurableSet.empty MeasurableSet.empty (by simp)
      | succ n ih =>
        simp only [Finset.range_add_one]
        rw [Finset.sum_insert (by simp)]
        simp only [Finset.mem_insert, Set.iUnion_iUnion_eq_or_left]
        rw [h'm _ _ (f_meas n), ih]
        · exact Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i)
        · simp only [Finset.mem_range, Set.disjoint_iUnion_right]
          intro i hi
          exact f_disj hi.ne'
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x ↔
      Membership.mem (γ := Set α) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i) x
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)

Tactic:
ext
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
x : α
h : (∃ (i : ℕ), x ∈ f i) ↔ (∃ i < n, x ∈ f i) ∨ ∃ (i : ℕ), n ≤ i ∧ x ∈ f i
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x ↔
    Membership.mem (γ := Set α) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i) x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
x : α
⊢ (∃ (i : ℕ), x ∈ f i) ↔ (∃ i < n, x ∈ f i) ∨ ∃ (i : ℕ), n ≤ i ∧ x ∈ f i

Tactic:
grind
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)

Tactic:
have : ⋃ i, f i = (⋃ i ∈ Finset.range n, f i) ∪ (⋃ i ∈ Set.Ici n, f i) := by
        ext; simp; grind
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
rw : m ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
⊢ m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
a : MeasurableSet.{u_1} (α := α) (⋃ i ∈ Finset.range n, f i)
a₁ : MeasurableSet.{u_1} (α := α) (⋃ i ∈ Set.Ici n, f i)
a₂ : Disjoint.{u_1} (α := Set α) (⋃ i ∈ Finset.range n, f i) (⋃ i ∈ Set.Ici n, f i)
⊢ m ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)

Tactic:
apply h'm
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ i ∈ Finset.range n, f i)

Tactic:
Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i)

Premises used: Finset.measurableSet_biUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ i ∈ Finset.range n, f i)

Tactic:
exact Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i)

Premises used: Finset.measurableSet_biUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ i ∈ Set.Ici n, f i)

Tactic:
MeasurableSet.biUnion (Set.to_countable _) (fun i hi ↦ f_meas i)

Premises used: Set.to_countable, MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ i ∈ Set.Ici n, f i)

Tactic:
exact MeasurableSet.biUnion (Set.to_countable _) (fun i hi ↦ f_meas i)

Premises used: Set.to_countable, MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
a : ∀ (i : ℕ) (i_1 : n ≤ i) (i_2 : ℕ) (i_3 : i_2 < n), Disjoint (f i_2) (f i)
⊢ Disjoint.{u_1} (α := Set α) (⋃ i ∈ Finset.range n, f i) (⋃ i ∈ Set.Ici n, f i)

Tactic:
simp only [Finset.mem_range, Set.mem_Ici, Set.disjoint_iUnion_right,
          Set.disjoint_iUnion_left]

Premises used: Set.disjoint_iUnion_left, Set.disjoint_iUnion_right, Finset.mem_range, Set.mem_Ici
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
i : ℕ
hi : n ≤ i
j : ℕ
hj : j < n
⊢ Disjoint (f j) (f i)

Tactic:
f_disj (hj.trans_le hi).ne

Premises used: LT.lt.trans_le, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
i : ℕ
hi : n ≤ i
j : ℕ
hj : j < n
⊢ Disjoint (f j) (f i)

Tactic:
exact f_disj (hj.trans_le hi).ne

Premises used: LT.lt.trans_le, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
⊢ ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)

Tactic:
have B n : m (⋃ i, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i) := by
      have : ⋃ i, f i = (⋃ i ∈ Finset.range n, f i) ∪ (⋃ i ∈ Set.Ici n, f i) := by
        ext; simp; grind
      rw [this]
      apply h'm
      · exact Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i)
      · exact MeasurableSet.biUnion (Set.to_countable _) (fun i hi ↦ f_meas i)
      · simp only [Finset.mem_range, Set.mem_Ici, Set.disjoint_iUnion_right,
          Set.disjoint_iUnion_left]
        intro i hi j hj
        exact f_disj (hj.trans_le hi).ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
n : ℕ
rw : ∑ i ∈ Finset.range n, m (f i) + m (⋃ i ∈ Set.Ici n, f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
⊢ m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)

Tactic:
rw [B n, A]
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
n : ℕ
⊢ ∑ i ∈ Finset.range n, m (f i) + m (⋃ i ∈ Set.Ici n, f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
⊢ ∀ (n : ℕ), m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)

Tactic:
have C n : m (⋃ i, f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i) := by
      rw [B n, A]; simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
C : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
simp : Filter.Tendsto (β := ENNReal) (fun (e : ℕ) ↦ ‖m (⋃ i ∈ Set.Ici e, f i)‖ₑ) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (β := ENNReal) (fun (e : ℕ) ↦ ‖m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ) Filter.atTop
    (nhds 0)

Tactic:
simp only [C]
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
C : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
apply :
  Filter.Tendsto (β := ENNReal) (fun (n : ℕ) ↦ (μ : (a : Set α) → ENNReal) (⋃ i ∈ Set.Ici n, f i)) Filter.atTop (nhds ⊥)
⊢ Filter.Tendsto (β := ENNReal) (fun (e : ℕ) ↦ ‖m (⋃ i ∈ Set.Ici e, f i)‖ₑ) Filter.atTop (nhds 0)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
      (h := fun n ↦ μ (⋃ i ∈ Set.Ici n, f i)) ?_ (fun i ↦ bot_le) (fun i ↦ hm _)

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, Set.iUnion, bot_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
C : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
⊢ Filter.Tendsto (β := ENNReal) (fun (n : ℕ) ↦ (μ : (a : Set α) → ENNReal) (⋃ i ∈ Set.Ici n, f i)) Filter.atTop (nhds ⊥)

Tactic:
tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint
      (fun i ↦ (f_meas i).nullMeasurableSet) f_disj

Premises used: Set.Ici, Set.Mem, MeasurableSet.nullMeasurableSet, setOf, MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint