awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
hf : Integrable f μ
⊢ Integrable (ε := E × F)
    (fun (x : X) ↦ (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)) μ

Tactic:
exact (ContinuousLinearEquiv.integrable_comp_iff _).2 hf

Premises used: Iff.mpr, ContinuousLinearEquiv.integrable_comp_iff
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace E
hf : Integrable f μ
enter : WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)
| Eq.{u_3 + 1} (α := F) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).2 (∫ (x : X), (f x).snd ∂μ)

Tactic:
enter [1, 1]
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace E
hf : Integrable f μ
enter : (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)
| Eq.{u_3 + 1} (α := F) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).2 (∫ (x : X), (f x).snd ∂μ)

Tactic:
enter [1, 1]; change WithLp.prodContinuousLinearEquiv q ℝ E F _

Premises used: Real, WithLp.prodContinuousLinearEquiv, DFunLike.coe
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace E
hf : Integrable f μ
conv :
  Eq.{u_3 + 1} (α := F)
    ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)).2
    (∫ (x : X), (f x).snd ∂μ)
⊢ Eq.{u_3 + 1} (α := F) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).2 (∫ (x : X), (f x).snd ∂μ)

Tactic:
conv => enter [1, 1]; change WithLp.prodContinuousLinearEquiv q ℝ E F _

Premises used: Real, WithLp.prodContinuousLinearEquiv, DFunLike.coe
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace E
hf : Integrable f μ
rw :
  Eq.{u_3 + 1} (α := F)
    (∫ (x : X), ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)).2 ∂μ)
    (∫ (x : X), (f x).snd ∂μ)
rw₁ :
  Integrable (ε := E × F)
    (fun (x : X) ↦ (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)) μ
⊢ Eq.{u_3 + 1} (α := F)
    ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)).2
    (∫ (x : X), (f x).snd ∂μ)

Tactic:
rw [← ContinuousLinearEquiv.integral_comp_comm, snd_integral]

Premises used: ContinuousLinearEquiv.integral_comp_comm, snd_integral
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace E
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := F)
    (∫ (x : X), ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)).2 ∂μ)
    (∫ (x : X), (f x).snd ∂μ)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace E
hf : Integrable f μ
⊢ Integrable (ε := E × F)
    (fun (x : X) ↦ (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)) μ

Tactic:
(ContinuousLinearEquiv.integrable_comp_iff _).2 hf

Premises used: Iff.mpr, setOf, ContinuousLinearEquiv.integrable_comp_iff
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace E
hf : Integrable f μ
⊢ Integrable (ε := E × F)
    (fun (x : X) ↦ (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)) μ

Tactic:
exact (ContinuousLinearEquiv.integrable_comp_iff _).2 hf

Premises used: Iff.mpr, ContinuousLinearEquiv.integrable_comp_iff
-- Module: Mathlib.MeasureTheory.Topology
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
μ : Measure α
inst_3 : NoAtoms μ
U : Set α
hU : MeasurableSet U
s : Set α
hs : s ∈ codiscreteWithin U
⊢ DiscreteTopology.{u_1} (↑(sᶜ ∩ U) : Type u_1)

Tactic:
have : DiscreteTopology ↑(sᶜ ∩ U) := isDiscrete_iff_discreteTopology.mp
    <| isDiscrete_of_codiscreteWithin ((compl_compl s).symm ▸ hs)
-- Module: Mathlib.MeasureTheory.Topology
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
μ : Measure α
inst_3 : NoAtoms μ
U : Set α
hU : MeasurableSet U
s : Set α
hs : s ∈ codiscreteWithin U
this : DiscreteTopology.{u_1} (↑(sᶜ ∩ U) : Type u_1)
rw : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (sᶜ ∩ U) : ENNReal) (0 : ENNReal)
⊢ s ∈ ae (μ.restrict U)

Tactic:
rw [mem_ae_iff, Measure.restrict_apply' hU]

Premises used: MeasureTheory.mem_ae_iff, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Topology
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
μ : Measure α
inst_3 : NoAtoms μ
U : Set α
hU : MeasurableSet U
s : Set α
hs : s ∈ codiscreteWithin U
this : DiscreteTopology.{u_1} (↑(sᶜ ∩ U) : Type u_1)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (sᶜ ∩ U) : ENNReal) (0 : ENNReal)

Tactic:
apply Set.Countable.measure_zero (TopologicalSpace.separableSpace_iff_countable.1 inferInstance)

Premises used: inferInstance, Set.Countable.measure_zero, Iff.mp, TopologicalSpace.separableSpace_iff_countable
-- 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
⊢ Disjoint.{u_1} (α := Set α) ∅ ∅

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
⊢ m ∅ = 0

Tactic:
simpa using h'm ∅ ∅ MeasurableSet.empty MeasurableSet.empty (by simp)

Premises used: MeasurableSet.empty, EmptyCollection.emptyCollection
-- 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)
rw : Filter.Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, m (f i)) Filter.atTop (nhds (m (⋃ (i : ℕ), f i)))
rw₁ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖m (f i)‖
⊢ HasSum (fun (i : ℕ) ↦ m (f i)) (m (⋃ (i : ℕ), f i))

Tactic:
rw [hasSum_iff_tendsto_nat_of_summable_norm]

Premises used: hasSum_iff_tendsto_nat_of_summable_norm
-- 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)
simp : Summable (α := ℝ) fun (i : ℕ) ↦ ‖m (f i)‖ₑ.toReal
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖m (f i)‖

Tactic:
simp only [← toReal_enorm]

Premises used: toReal_enorm
-- 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)
hsum : Ne (α := ENNReal) (∑' (x : ℕ), ‖m (f x)‖ₑ) ⊤
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖m (f i)‖ₑ.toReal

Tactic:
apply ENNReal.summable_toReal

Premises used: ENNReal.summable_toReal
-- 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)
hsum : LT.lt (α := ENNReal) (∑' (x : ℕ), ‖m (f x)‖ₑ) ⊤
⊢ Ne (α := ENNReal) (∑' (x : ℕ), ‖m (f x)‖ₑ) ⊤

Tactic:
apply ne_of_lt

Premises used: ne_of_lt
-- 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)
h : ∀ (i : ℕ), ‖m (f i)‖ₑ ≤ (μ : (a : Set α) → ENNReal) (f i)
⊢ LE.le (α := ENNReal) (∑' (i : ℕ), ‖m (f i)‖ₑ) (∑' (i : ℕ), (μ : (a : Set α) → ENNReal) (f i))

Tactic:
gcongr
-- 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)
i : ℕ
⊢ ‖m (f i)‖ₑ ≤ (μ : (a : Set α) → ENNReal) (f i)

Tactic:
apply hm
-- 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)
⊢ Eq (α := ENNReal) (∑' (i : ℕ), (μ : (a : Set α) → ENNReal) (f i) : ENNReal)
    ((μ : (a : Set α) → ENNReal) (⋃ (i : ℕ), f i) : ENNReal)

Tactic:
(measure_iUnion f_disj f_meas).symm

Premises used: MeasureTheory.measure_iUnion, Eq.symm
-- 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)
⊢ LT.lt (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋃ (i : ℕ), f i) : ENNReal) (⊤ : ENNReal)

Tactic:
measure_lt_top μ (⋃ i, f i)

Premises used: MeasureTheory.measure_lt_top, Set.iUnion
-- 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)
calc : LE.le (α := ENNReal) (∑' (i : ℕ), ‖m (f i)‖ₑ) (∑' (i : ℕ), (μ : (a : Set α) → ENNReal) (f i))
⊢ LT.lt (α := ENNReal) (∑' (x : ℕ), ‖m (f x)‖ₑ) ⊤

Tactic:
calc ∑' i, ‖m (f i)‖ₑ
      _ ≤ ∑' i, μ (f i) := by gcongr; apply hm
      _ = μ (⋃ i, f i) := (measure_iUnion f_disj f_meas).symm
      _ < ⊤ := measure_lt_top μ (⋃ i, f i)

Premises used: MeasureTheory.measure_lt_top, MeasureTheory.measure_iUnion, Eq.symm, DFunLike.coe, Set.iUnion
-- 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)
apply :
  Filter.Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖∑ i ∈ Finset.range e, m (f i) - m (⋃ (i : ℕ), f i)‖) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, m (f i)) Filter.atTop (nhds (m (⋃ (i : ℕ), f i)))

Tactic:
apply tendsto_iff_norm_sub_tendsto_zero.2

Premises used: Iff.mpr, tendsto_iff_norm_sub_tendsto_zero
-- 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)
simp_rw :
  Filter.Tendsto (fun (e : ℕ) ↦ ‖m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ.toReal) Filter.atTop
    (nhds (ENNReal.toReal 0))
⊢ Filter.Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖∑ i ∈ Finset.range e, m (f i) - m (⋃ (i : ℕ), f i)‖) Filter.atTop (nhds 0)

Tactic:
simp_rw [norm_sub_rev, ← toReal_enorm, ← ENNReal.toReal_zero]

Premises used: toReal_enorm, ENNReal.toReal_zero, norm_sub_rev
-- 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)
apply :
  Filter.Tendsto (β := ENNReal) (fun (e : ℕ) ↦ ‖m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ) Filter.atTop
    (nhds 0)
⊢ Filter.Tendsto (fun (e : ℕ) ↦ ‖m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ.toReal) Filter.atTop
    (nhds (ENNReal.toReal 0))

Tactic:
apply (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp

Premises used: ENNReal.tendsto_toReal, ENNReal.zero_ne_top, Filter.Tendsto.comp
-- 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)
⊢ Disjoint.{u_1} (α := Set α) ∅ ∅

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)
⊢ m (⋃ i ∈ Finset.range 0, f i) = ∑ i ∈ Finset.range 0, m (f i)

Tactic:
simpa using h'm ∅ ∅ MeasurableSet.empty MeasurableSet.empty (by simp)

Premises used: MeasurableSet.empty, EmptyCollection.emptyCollection
-- 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 : m (⋃ i ∈ insert n (Finset.range n), f i) = ∑ x ∈ insert n (Finset.range n), m (f x)
⊢ m (⋃ i ∈ Finset.range (n + 1), f i) = ∑ i ∈ Finset.range (n + 1), m (f i)

Tactic:
simp only [Finset.range_add_one]

Premises used: Finset.range_add_one
-- 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)
⊢ n ∉ Finset.range n

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)
n : ℕ
ih : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
succ : m (⋃ i ∈ insert n (Finset.range n), f i) = m (f n) + ∑ x ∈ Finset.range n, m (f x)
⊢ m (⋃ i ∈ insert n (Finset.range n), f i) = ∑ x ∈ insert n (Finset.range n), m (f x)

Tactic:
rw [Finset.sum_insert (by simp)]

Premises used: Finset.sum_insert
-- 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 : m (f n ∪ ⋃ x ∈ Finset.range n, f x) = m (f n) + ∑ x ∈ Finset.range n, m (f x)
⊢ m (⋃ i ∈ insert n (Finset.range n), f i) = m (f n) + ∑ x ∈ Finset.range n, m (f x)

Tactic:
simp only [Finset.mem_insert, Set.iUnion_iUnion_eq_or_left]

Premises used: Finset.mem_insert, Set.iUnion_iUnion_eq_or_left
-- 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 : MeasurableSet.{u_1} (α := α) (⋃ x ∈ Finset.range n, f x)
succ₁ : Disjoint (f n) (⋃ x ∈ Finset.range n, f x)
⊢ m (f n ∪ ⋃ x ∈ Finset.range n, f x) = m (f n) + ∑ x ∈ Finset.range n, m (f x)

Tactic:
rw [h'm _ _ (f_meas n), ih]
-- 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)
⊢ MeasurableSet.{u_1} (α := α) (⋃ x ∈ Finset.range n, f x)

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)
n : ℕ
ih : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ x ∈ Finset.range n, f x)

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

Premises used: Finset.measurableSet_biUnion