awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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∞)
⊢ 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
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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∞)

Tactic:
tendsto_nhds_unique ?_ (ENNReal.tendsto_nat_tsum fun i ↦ m (f i))

Premises used: ENNReal.tendsto_nat_tsum, DFunLike.coe, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
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∞)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
refine tendsto_nhds_unique ?_ (ENNReal.tendsto_nat_tsum fun i ↦ m (f i))

Premises used: ENNReal.tendsto_nat_tsum, DFunLike.coe, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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∞)

Tactic:
(Filter.tendsto_add_atTop_iff_nat 1).mp ?_

Premises used: Iff.mp, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
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∞)
⊢ 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 (Filter.tendsto_add_atTop_iff_nat 1).mp ?_

Premises used: Iff.mp, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
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∞)
⊢ 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:
rwa [ENNReal.tendsto_const_sub_nhds_zero_iff (hm_ne_top _ hUf) (fun n ↦ ?_)] at h_tendsto

Premises used: ENNReal.tendsto_const_sub_nhds_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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 : ℕ
rw :
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (accumulate f n) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
rw [← addContent_accumulate m hC h_disj hf]

Premises used: MeasureTheory.addContent_accumulate
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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∞) ((m : (a : Set α) → ℝ≥0∞) (accumulate f n) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
addContent_mono hC.isSetSemiring (hC.accumulate_mem hf n) hUf
    (Set.accumulate_subset_iUnion _)

Premises used: MeasureTheory.addContent_mono, MeasureTheory.IsSetRing.isSetSemiring, Set.accumulate_subset_iUnion, MeasureTheory.IsSetRing.accumulate_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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∞) ((m : (a : Set α) → ℝ≥0∞) (accumulate f n) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
exact addContent_mono hC.isSetSemiring (hC.accumulate_mem hf n) hUf
    (Set.accumulate_subset_iUnion _)

Premises used: MeasureTheory.addContent_mono, MeasureTheory.IsSetRing.isSetSemiring, Set.accumulate_subset_iUnion, MeasureTheory.IsSetRing.accumulate_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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 rwa rwa₁ rwa₂ rwa₃ : ⋃ (i : ℕ), f i ∈ C
⊢ ⋃ (i : ℕ), disjointed f i ∈ C

Tactic:
rwa [iUnion_disjointed]

Premises used: iUnion_disjointed
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
rw :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (f n)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) (f n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)

Tactic:
rw [← iUnion_disjointed, m_iUnion _ (hC.disjointed_mem hf) (by rwa [iUnion_disjointed])
      (disjoint_disjointed f)]

Premises used: iUnion_disjointed, disjoint_disjointed, MeasureTheory.IsSetRing.disjointed_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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 : ℕ
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∞)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f n) : ℝ≥0∞)
    (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (disjointed f i) : ℝ≥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]

Premises used: partialSups_disjointed, partialSups_eq_biSup, Set.accumulate, Monotone.partialSups_eq, MeasureTheory.addContent_accumulate, disjoint_disjointed, MeasureTheory.IsSetRing.disjointed_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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∞) (⨆ (j : ℕ), ⨆ (_ : j ≤ n), disjointed f j) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (y : ℕ), ⋃ (_ : y ≤ n), disjointed f y) : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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∞)

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
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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∞)
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)))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (f n)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)))

Tactic:
simp_rw [h]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)))

Tactic:
(tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (disjointed f i))) 1).2 ?_

Premises used: Iff.mpr, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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∞)
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)))
⊢ 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:
refine (tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (disjointed f i))) 1).2 ?_

Premises used: Iff.mpr, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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 (k : ℕ) ↦ ∑ i ∈ Finset.range k, (m : (a : Set α) → ℝ≥0∞) (disjointed f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)))

Tactic:
ENNReal.tendsto_nat_tsum _

Premises used: ENNReal.tendsto_nat_tsum
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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 (k : ℕ) ↦ ∑ i ∈ Finset.range k, (m : (a : Set α) → ℝ≥0∞) (disjointed f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (disjointed f i)))

Tactic:
exact ENNReal.tendsto_nat_tsum _

Premises used: ENNReal.tendsto_nat_tsum
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
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∞)
⊢ 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:
rw [← iSup_eq_iUnion, ← iSup_partialSups_eq]

Premises used: iSup_partialSups_eq, Set.iSup_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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∞)

Tactic:
tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum hC m_iUnion
      (partialSups_monotone f) (hC.partialSups_mem hf) ?_

Premises used: partialSups_monotone, MeasureTheory.IsSetRing.partialSups_mem, MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum, Set.iUnion