awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
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 μ
| Eq.{u_2 + 1} (α := E) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).1 (∫ (x : X), (f x).fst ∂μ)
have enter : (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)
Tactic: enter [1, 1]; change WithLp.prodContinuousLinearEquiv q ℝ E F _
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
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 μ
⊢ Eq.{u_2 + 1} (α := E) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).1 (∫ (x : X), (f x).fst ∂μ)
have conv : Eq.{u_2 + 1} (α := E)
  ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)).1
  (∫ (x : X), (f x).fst ∂μ)
Tactic: conv => enter [1, 1]; change WithLp.prodContinuousLinearEquiv q ℝ E F _
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
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 μ
⊢ Eq.{u_2 + 1} (α := E)
    ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)).1
    (∫ (x : X), (f x).fst ∂μ)
have rw : Eq.{u_2 + 1} (α := E)
  (∫ (x : X), ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)).1 ∂μ)
  (∫ (x : X), (f x).fst ∂μ)
Tactic: rw [← ContinuousLinearEquiv.integral_comp_comm, fst_integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
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 μ
rw :
  Eq.{u_2 + 1} (α := E)
    (∫ (x : X), ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)).1 ∂μ)
    (∫ (x : X), (f x).fst ∂μ)
⊢ Eq.{u_2 + 1} (α := E)
    ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)).1
    (∫ (x : X), (f x).fst ∂μ)
have rw₁ : Integrable (ε := E × F)
  (fun (x : X) ↦ (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)) μ
Tactic: rw [← ContinuousLinearEquiv.integral_comp_comm, fst_integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
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) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).2 (∫ (x : X), (f x).snd ∂μ)
have enter : WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)
Tactic: enter [1, 1]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
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) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).2 (∫ (x : X), (f x).snd ∂μ)
have enter : (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)
Tactic: enter [1, 1]; change WithLp.prodContinuousLinearEquiv q ℝ E F _
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
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) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).2 (∫ (x : X), (f x).snd ∂μ)
have 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 ∂μ)
Tactic: conv => enter [1, 1]; change WithLp.prodContinuousLinearEquiv q ℝ E F _
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
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)
    ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)).2
    (∫ (x : X), (f x).snd ∂μ)
have 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 ∂μ)
Tactic: rw [← ContinuousLinearEquiv.integral_comp_comm, snd_integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
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 ∂μ)
⊢ 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 ∂μ)
have rw₁ : Integrable (ε := E × F)
  (fun (x : X) ↦ (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)) μ
Tactic: rw [← ContinuousLinearEquiv.integral_comp_comm, snd_integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Topology (hypothesis)
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
⊢ s ∈ ae (μ.restrict U)
have this : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Topology (goal)
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)
⊢ s ∈ ae (μ.restrict U)
have rw : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (sᶜ ∩ U) : ENNReal) (0 : ENNReal)
Tactic: rw [mem_ae_iff, Measure.restrict_apply' hU]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ HasSum (fun (i : ℕ) ↦ m (f i)) (m (⋃ (i : ℕ), f i))
have rw : Filter.Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, m (f i)) Filter.atTop (nhds (m (⋃ (i : ℕ), f i)))
Tactic: rw [hasSum_iff_tendsto_nat_of_summable_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)))
⊢ HasSum (fun (i : ℕ) ↦ m (f i)) (m (⋃ (i : ℕ), f i))
have rw₁ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖m (f i)‖
Tactic: rw [hasSum_iff_tendsto_nat_of_summable_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖m (f i)‖
have simp : Summable (α := ℝ) fun (i : ℕ) ↦ ‖m (f i)‖ₑ.toReal
Tactic: simp only [← toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖m (f i)‖ₑ.toReal
have hsum : Ne (α := ENNReal) (∑' (x : ℕ), ‖m (f x)‖ₑ) ⊤
Tactic: apply ENNReal.summable_toReal
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ Ne (α := ENNReal) (∑' (x : ℕ), ‖m (f x)‖ₑ) ⊤
have hsum : LT.lt (α := ENNReal) (∑' (x : ℕ), ‖m (f x)‖ₑ) ⊤
Tactic: apply ne_of_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ LE.le (α := ENNReal) (∑' (i : ℕ), ‖m (f i)‖ₑ) (∑' (i : ℕ), (μ : (a : Set α) → ENNReal) (f i))
have h : ∀ (i : ℕ), ‖m (f i)‖ₑ ≤ (μ : (a : Set α) → ENNReal) (f i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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) (∑' (x : ℕ), ‖m (f x)‖ₑ) ⊤
have calc : LE.le (α := ENNReal) (∑' (i : ℕ), ‖m (f i)‖ₑ) (∑' (i : ℕ), (μ : (a : Set α) → ENNReal) (f i))
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ Filter.Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, m (f i)) Filter.atTop (nhds (m (⋃ (i : ℕ), f i)))
have apply : Filter.Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖∑ i ∈ Finset.range e, m (f i) - m (⋃ (i : ℕ), f i)‖) Filter.atTop (nhds 0)
Tactic: apply tendsto_iff_norm_sub_tendsto_zero.2
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ Filter.Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖∑ i ∈ Finset.range e, m (f i) - m (⋃ (i : ℕ), f i)‖) Filter.atTop (nhds 0)
have simp_rw : Filter.Tendsto (fun (e : ℕ) ↦ ‖m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ.toReal) Filter.atTop
  (nhds (ENNReal.toReal 0))
Tactic: simp_rw [norm_sub_rev, ← toReal_enorm, ← ENNReal.toReal_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ Filter.Tendsto (fun (e : ℕ) ↦ ‖m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ.toReal) Filter.atTop
    (nhds (ENNReal.toReal 0))
have apply : Filter.Tendsto (β := ENNReal) (fun (e : ℕ) ↦ ‖m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ) Filter.atTop
  (nhds 0)
Tactic: apply (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ m (⋃ i ∈ Finset.range (n + 1), f i) = ∑ i ∈ Finset.range (n + 1), m (f i)
have succ : m (⋃ i ∈ insert n (Finset.range n), f i) = ∑ x ∈ insert n (Finset.range n), m (f x)
Tactic: simp only [Finset.range_add_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ m (⋃ i ∈ insert n (Finset.range n), f i) = ∑ x ∈ insert n (Finset.range n), m (f x)
have succ : m (⋃ i ∈ insert n (Finset.range n), f i) = m (f n) + ∑ x ∈ Finset.range n, m (f x)
Tactic: rw [Finset.sum_insert (by simp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ m (⋃ i ∈ insert n (Finset.range n), f i) = m (f n) + ∑ x ∈ Finset.range n, m (f x)
have succ : m (f n ∪ ⋃ x ∈ Finset.range n, f x) = m (f n) + ∑ x ∈ Finset.range n, m (f x)
Tactic: simp only [Finset.mem_insert, Set.iUnion_iUnion_eq_or_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ m (f n ∪ ⋃ x ∈ Finset.range n, f x) = m (f n) + ∑ x ∈ Finset.range n, m (f x)
have succ : MeasurableSet.{u_1} (α := α) (⋃ x ∈ Finset.range n, f x)
Tactic: rw [h'm _ _ (f_meas n), ih]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ m (f n ∪ ⋃ x ∈ Finset.range n, f x) = m (f n) + ∑ x ∈ Finset.range n, m (f x)
have succ₁ : Disjoint (f n) (⋃ x ∈ Finset.range n, f x)
Tactic: rw [h'm _ _ (f_meas n), ih]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ Disjoint (f n) (⋃ x ∈ Finset.range n, f x)
have succ : ∀ (i : ℕ) (i_1 : i < n), Disjoint (f n) (f i)
Tactic: simp only [Finset.mem_range, Set.disjoint_iUnion_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
have zero : m (⋃ i ∈ Finset.range 0, f i) = ∑ i ∈ Finset.range 0, 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'
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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)
⊢ m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
have 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)
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'
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (hypothesis)
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)
⊢ Filter.Tendsto (β := ENNReal) (fun (e : ℕ) ↦ ‖m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ) Filter.atTop
    (nhds 0)
have A : ∀ (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'