awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
n : ℕ
⊢ (m : (a : Set α) → ℝ≥0∞) (s n) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (accumulate f n) : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: rw [addContent_diff_of_ne_top m hC hm_ne_top hUf (hC.accumulate_mem hf n)
      (Set.accumulate_subset_iUnion _), addContent_accumulate m hC h_disj hf n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
n : ℕ
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (accumulate f n) : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ (m : (a : Set α) → ℝ≥0∞) (s n) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have rw₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: rw [addContent_diff_of_ne_top m hC hm_ne_top hUf (hC.accumulate_mem hf n)
      (Set.accumulate_subset_iUnion _), addContent_accumulate m hC h_disj hf n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have hmsn : ∀ (n : ℕ),
  (m : (a : Set α) → ℝ≥0∞) (s n) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: have hmsn n : m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i) := by
    rw [addContent_diff_of_ne_top m hC hm_ne_top hUf (hC.accumulate_mem hf n)
      (Set.accumulate_subset_iUnion _), addContent_accumulate m hC h_disj hf n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
hmsn :
  ∀ (n : ℕ),
    (m : (a : Set α) → ℝ≥0∞) (s n) =
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have h_tendsto₁ : Tendsto (β := ℝ≥0∞)
  (fun (n : ℕ) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞))
  atTop (𝓝 0)
Tactic: simp_rw [hmsn] at h_tendsto
Cleared hypotheses: h_tendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
hmsn :
  ∀ (n : ℕ),
    (m : (a : Set α) → ℝ≥0∞) (s n) =
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
h_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞))
    atTop (𝓝 0)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have refine : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (∑ i ∈ Finset.range n, (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)) atTop
  (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
Tactic: refine tendsto_nhds_unique ?_ (ENNReal.tendsto_nat_tsum fun i ↦ m (f i))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
hmsn :
  ∀ (n : ℕ),
    (m : (a : Set α) → ℝ≥0∞) (s n) =
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
h_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞))
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (∑ i ∈ Finset.range n, (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
have refine : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)) atTop
  (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
Tactic: refine (Filter.tendsto_add_atTop_iff_nat 1).mp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
hmsn :
  ∀ (n : ℕ),
    (m : (a : Set α) → ℝ≥0∞) (s n) =
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
h_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞))
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
have rwa : ∀ (n : ℕ),
  LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
Tactic: rwa [ENNReal.tendsto_const_sub_nhds_zero_iff (hm_ne_top _ hUf) (fun n ↦ ?_)] at h_tendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
hmsn :
  ∀ (n : ℕ),
    (m : (a : Set α) → ℝ≥0∞) (s n) =
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
h_tendsto :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞))
    atTop (𝓝 0)
n : ℕ
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (accumulate f n) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
Tactic: rw [← addContent_accumulate m hC h_disj hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) (f n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (f n)) atTop
  (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)))
Tactic: rw [← iUnion_disjointed, m_iUnion _ (hC.disjointed_mem hf) (by rwa [iUnion_disjointed])
      (disjoint_disjointed f)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f n) : ℝ≥0∞)
    (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (disjointed f i) : ℝ≥0∞)
have nth_rw : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⨆ (j : ℕ), ⨆ (_ : j ≤ n), disjointed f j) : ℝ≥0∞)
  ((m : (a : Set α) → ℝ≥0∞) (⋃ (y : ℕ), ⋃ (_ : y ≤ n), disjointed f y) : ℝ≥0∞)
Tactic: nth_rw 1 [← addContent_accumulate _ hC (disjoint_disjointed f) (hC.disjointed_mem hf),
    ← hf_mono.partialSups_eq, ← partialSups_disjointed, partialSups_eq_biSup, accumulate]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (f n)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)))
have h : ∀ (n : ℕ),
  Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f n) : ℝ≥0∞)
    (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (disjointed f i) : ℝ≥0∞)
Tactic: have h n : m (f n) = ∑ i ∈ range (n + 1), m (disjointed f i) := by
    nth_rw 1 [← addContent_accumulate _ hC (disjoint_disjointed f) (hC.disjointed_mem hf),
    ← hf_mono.partialSups_eq, ← partialSups_disjointed, partialSups_eq_biSup, accumulate]
    rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h :
  ∀ (n : ℕ),
    Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f n) : ℝ≥0∞)
      (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (disjointed f i) : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (f n)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)))
have simp_rw : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)) atTop
  (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)))
Tactic: simp_rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h :
  ∀ (n : ℕ),
    Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f n) : ℝ≥0∞)
      (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (disjointed f i) : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)))
have refine : Tendsto (β := ℝ≥0∞) (fun (k : ℕ) ↦ ∑ i ∈ Finset.range k, (m : (a : Set α) → ℝ≥0∞) (disjointed f i)) atTop
  (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)))
Tactic: refine (tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (disjointed f i))) 1).2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
  (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⨆ (i : ℕ), (partialSups f : (a : ℕ) → Set α) i)) : Filter ℝ≥0∞)
Tactic: rw [← iSup_eq_iUnion, ← iSup_partialSups_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⨆ (i : ℕ), (partialSups f : (a : ℕ) → Set α) i)) : Filter ℝ≥0∞)
have refine : ⋃ (i : ℕ), (partialSups f : (a : ℕ) → Set α) i ∈ C
Tactic: refine tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum hC m_iUnion
      (partialSups_monotone f) (hC.partialSups_mem hf) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
⊢ ⋃ (i : ℕ), (partialSups f : (a : ℕ) → Set α) i ∈ C
have rwa : ⨆ (i : ℕ), (partialSups f : (a : ℕ) → Set α) i ∈ C
Tactic: rwa [← iSup_eq_iUnion, iSup_partialSups_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
rwa : ⨆ (i : ℕ), (partialSups f : (a : ℕ) → Set α) i ∈ C
⊢ ⋃ (i : ℕ), (partialSups f : (a : ℕ) → Set α) i ∈ C
have rwa₁ : ⨆ (i : ℕ), f i ∈ C
Tactic: rwa [← iSup_eq_iUnion, iSup_partialSups_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
  (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
Tactic: have h_tendsto : Tendsto (fun n ↦ m (partialSups f n)) atTop (𝓝 (m (⋃ i, f i))) := by
    rw [← iSup_eq_iUnion, ← iSup_partialSups_eq]
    refine tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum hC m_iUnion
      (partialSups_monotone f) (hC.partialSups_mem hf) ?_
    rwa [← iSup_eq_iUnion, iSup_partialSups_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))
have rw : Tendsto (β := ℝ≥0∞) (fun (k : ℕ) ↦ ∑ i ∈ Finset.range k, (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
  (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))
Tactic: rw [tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (f i))) 1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have h_tendsto' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
  (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))
Tactic: have h_tendsto' : Tendsto (fun n ↦ ∑ i ∈ range (n + 1), m (f i)) atTop (𝓝 (∑' i, m (f i))) := by
    rw [tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (f i))) 1]
    exact ENNReal.tendsto_nat_tsum _