awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hm : Monotone s
h : NeBot.{u_5} (α := ι) atTop
⊢ IsDirectedOrder ι

Tactic:
have := (atTop_neBot_iff.1 h).2
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hm : Monotone s
h : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
rw : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) atTop (𝓝 (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)))
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n)) : Filter ℝ≥0∞)

Tactic:
rw [hm.measure_iUnion]

Premises used: Monotone.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hm : Monotone s
h : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) atTop (𝓝 (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)))

Tactic:
tendsto_atTop_iSup fun n m hnm => measure_mono <| hm hnm

Premises used: tendsto_atTop_iSup, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hm : Monotone s
h : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) atTop (𝓝 (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)))

Tactic:
exact tendsto_atTop_iSup fun n m hnm => measure_mono <| hm hnm

Premises used: tendsto_atTop_iSup, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hm : Antitone s
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) atBot
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n)) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_iUnion_atTop (ι := ιᵒᵈ) hm.dual_left

Premises used: MeasureTheory.tendsto_measure_iUnion_atTop, setOf, Antitone.dual_left, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_9} (α := ι) atTop
x : MeasurableSpace α
μ : Measure α
f : ι → Set α
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i)) : Filter ℝ≥0∞)

Tactic:
.of_neBot_imp fun h ↦ ?_

Premises used: Filter.Tendsto.of_neBot_imp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_9} (α := ι) atTop
x : MeasurableSpace α
μ : Measure α
f : ι → Set α
⊢ NeBot.{u_9} (α := ι) atTop

Tactic:
refine .of_neBot_imp fun h ↦ ?_
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_9} (α := ι) atTop
x : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : NeBot.{u_9} (α := ι) atTop
⊢ IsDirectedOrder ι

Tactic:
have := (atTop_neBot_iff.1 h).2
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_9} (α := ι) atTop
x : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : NeBot.{u_9} (α := ι) atTop
this : IsDirectedOrder ι
rw :
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (accumulate f i)) atTop
    (𝓝 (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (accumulate f i)))
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i)) : Filter ℝ≥0∞)

Tactic:
rw [measure_iUnion_eq_iSup_accumulate]

Premises used: MeasureTheory.measure_iUnion_eq_iSup_accumulate
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_9} (α := ι) atTop
x : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : NeBot.{u_9} (α := ι) atTop
this : IsDirectedOrder ι
i j : ι
hij : i ≤ j
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (accumulate f j) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_9} (α := ι) atTop
x : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : NeBot.{u_9} (α := ι) atTop
this : IsDirectedOrder ι
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (accumulate f i)) atTop
    (𝓝 (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (accumulate f i)))

Tactic:
exact tendsto_atTop_iSup fun i j hij ↦ by gcongr

Premises used: tendsto_atTop_iSup
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), s n)) : Filter ℝ≥0∞)

Tactic:
.of_neBot_imp fun h ↦ ?_

Premises used: Filter.Tendsto.of_neBot_imp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ NeBot.{u_5} (α := ι) atTop

Tactic:
refine .of_neBot_imp fun h ↦ ?_
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h : NeBot.{u_5} (α := ι) atTop
⊢ IsDirectedOrder ι

Tactic:
have := (atTop_neBot_iff.1 h).2
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
rw : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) atTop (𝓝 (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)))
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), s n)) : Filter ℝ≥0∞)

Tactic:
rw [hm.measure_iInter hs hf]

Premises used: Antitone.measure_iInter
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) atTop (𝓝 (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)))

Tactic:
tendsto_atTop_iInf fun n m hnm => measure_mono <| hm hnm

Premises used: MeasureTheory.measure_mono, tendsto_atTop_iInf
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) atTop (𝓝 (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)))

Tactic:
exact tendsto_atTop_iInf fun n m hnm => measure_mono <| hm hnm

Premises used: MeasureTheory.measure_mono, tendsto_atTop_iInf
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Monotone s
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) atBot
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), s n)) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_iInter_atTop (ι := ιᵒᵈ) hs hm.dual_left hf

Premises used: setOf, Monotone.dual_left, MeasureTheory.tendsto_measure_iInter_atTop, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i)) : Filter ℝ≥0∞)

Tactic:
.of_neBot_imp fun hne ↦ ?_

Premises used: Filter.Tendsto.of_neBot_imp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ NeBot.{u_9} (α := ι) atTop

Tactic:
refine .of_neBot_imp fun hne ↦ ?_
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hne : NeBot.{u_9} (α := ι) atTop
⊢ Nonempty ι

Tactic:
cases atTop_neBot_iff.mp hne

Premises used: Iff.mp, Filter.atTop_neBot_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hne : NeBot.{u_9} (α := ι) atTop
left : Nonempty ι
⊢ IsDirectedOrder ι

Tactic:
cases atTop_neBot_iff.mp hne

Premises used: Iff.mp, Filter.atTop_neBot_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hne : NeBot.{u_9} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
intro :
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j)) atTop
    (𝓝 (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j)))
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i)) : Filter ℝ≥0∞)

Tactic:
rw [measure_iInter_eq_iInf_measure_iInter_le hm hf]

Premises used: MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hne : NeBot.{u_9} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j)) atTop
    (𝓝 (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j)))

Tactic:
tendsto_atTop_iInf
    fun i j hij ↦ measure_mono <| biInter_subset_biInter_left fun k hki ↦ le_trans hki hij

Premises used: Set.biInter_subset_biInter_left, MeasureTheory.measure_mono, tendsto_atTop_iInf, le_trans
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hne : NeBot.{u_9} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j)) atTop
    (𝓝 (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j)))

Tactic:
exact tendsto_atTop_iInf
    fun i j hij ↦ measure_mono <| biInter_subset_biInter_left fun k hki ↦ le_trans hki hij

Premises used: MeasureTheory.measure_mono, tendsto_atTop_iInf
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : SemilatticeSup ι
inst_1 : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hfem : Eq.{u_8 + 1} (α := Set α) (⋂ (n : ι), f n) ∅
F : (m : ι) → ℝ≥0∞ := fun (m : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n)
⊢ Antitone F

Tactic:
have hFAnti : Antitone F :=
      fun i j hij => measure_mono (biInter_subset_biInter_left fun k hki => le_trans hki hij)
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : SemilatticeSup ι
inst_1 : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hfem : Eq.{u_8 + 1} (α := Set α) (⋂ (n : ι), f n) ∅
F : (m : ι) → ℝ≥0∞ := fun (m : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
this : Tendsto F atTop (𝓝 0)
h : Nonempty ι := ⋯
⊢ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : ι), F n < ε

Tactic:
rw [ENNReal.tendsto_atTop_zero_iff_lt_of_antitone hFAnti] at this

Premises used: ENNReal.tendsto_atTop_zero_iff_lt_of_antitone
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : SemilatticeSup ι
inst_1 : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hfem : Eq.{u_8 + 1} (α := Set α) (⋂ (n : ι), f n) ∅
F : (m : ι) → ℝ≥0∞ := fun (m : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
this : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : ι), F n < ε
h : Nonempty ι := ⋯
⊢ ∃ (m : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n) < ε

Tactic:
this ε hε
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : SemilatticeSup ι
inst_1 : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hfem : Eq.{u_8 + 1} (α := Set α) (⋂ (n : ι), f n) ∅
F : (m : ι) → ℝ≥0∞ := fun (m : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
this : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : ι), F n < ε
h : Nonempty ι := ⋯
⊢ ∃ (m : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n) < ε

Tactic:
exact this ε hε
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : SemilatticeSup ι
inst_1 : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hfem : Eq.{u_8 + 1} (α := Set α) (⋂ (n : ι), f n) ∅
F : (m : ι) → ℝ≥0∞ := fun (m : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
suffices : Tendsto F atTop (𝓝 0)
⊢ ∃ (m : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n) < ε

Tactic:
suffices Filter.Tendsto F Filter.atTop (𝓝 0) by
    let _ := hfin.nonempty
    rw [ENNReal.tendsto_atTop_zero_iff_lt_of_antitone hFAnti] at this
    exact this ε hε
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : SemilatticeSup ι
inst_1 : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hfem : Eq.{u_8 + 1} (α := Set α) (⋂ (n : ι), f n) ∅
F : (m : ι) → ℝ≥0∞ := fun (m : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), f n) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [hfem, measure_empty]

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : SemilatticeSup ι
inst_1 : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hfem : Eq.{u_8 + 1} (α := Set α) (⋂ (n : ι), f n) ∅
F : (m : ι) → ℝ≥0∞ := fun (m : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), f n) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have hzero : μ (⋂ n, f n) = 0 := by
    simp only [hfem, measure_empty]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : SemilatticeSup ι
inst_1 : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hfem : Eq.{u_8 + 1} (α := Set α) (⋂ (n : ι), f n) ∅
F : (m : ι) → ℝ≥0∞ := fun (m : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
hzero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), f n) : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Tendsto F atTop (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), f n)))
⊢ Tendsto F atTop (𝓝 0)

Tactic:
rw [← hzero]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : SemilatticeSup ι
inst_1 : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hfem : Eq.{u_8 + 1} (α := Set α) (⋂ (n : ι), f n) ∅
F : (m : ι) → ℝ≥0∞ := fun (m : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
hzero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), f n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Tendsto F atTop (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), f n)))

Tactic:
tendsto_measure_iInter_le hm hfin

Premises used: MeasureTheory.tendsto_measure_iInter_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : SemilatticeSup ι
inst_1 : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hfem : Eq.{u_8 + 1} (α := Set α) (⋂ (n : ι), f n) ∅
F : (m : ι) → ℝ≥0∞ := fun (m : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
hzero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), f n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Tendsto F atTop (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), f n)))

Tactic:
exact tendsto_measure_iInter_le hm hfin

Premises used: MeasureTheory.tendsto_measure_iInter_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s r) : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  ∀ (ha : Order.IsPredPrelimit a),
    Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
      (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)
neg :
  ∀ (ha : ¬Order.IsPredPrelimit a),
    Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
      (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)

Tactic:
by_cases ha : Order.IsPredPrelimit a

Premises used: Order.IsPredPrelimit
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s r) : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : Order.IsPredPrelimit a
rw : IsCountablyGenerated (α := (↑(Ioi a) : Type u_8)) (comap (Subtype.val (p := fun (x : ι) ↦ x ∈ Ioi a)) (𝓝[>] a))
⊢ IsCountablyGenerated.{u_8} (α := (↑(Ioi a) : Type u_8)) atBot

Tactic:
rw [← comap_coe_Ioi_nhdsGT a ha]

Premises used: comap_coe_Ioi_nhdsGT
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s r) : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : Order.IsPredPrelimit a
⊢ IsCountablyGenerated (α := (↑(Ioi a) : Type u_8)) (comap (Subtype.val (p := fun (x : ι) ↦ x ∈ Ioi a)) (𝓝[>] a))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s r) : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : Order.IsPredPrelimit a
⊢ IsCountablyGenerated.{u_8} (α := (↑(Ioi a) : Type u_8)) atBot

Tactic:
have : (atBot : Filter (Ioi a)).IsCountablyGenerated := by
      rw [← comap_coe_Ioi_nhdsGT a ha]
      infer_instance
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s r) : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : Order.IsPredPrelimit a
this : IsCountablyGenerated.{u_8} (α := (↑(Ioi a) : Type u_8)) atBot
pos :
  Tendsto (α := { x : ι // x ∈ Ioi a }) (β := ℝ≥0∞)
    (((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ Ioi a) : { x : ι // x ∈ Ioi a } → ℝ≥0∞) atBot
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (x : (↑(Ioi a) : Type u_8)), s (↑x : ι))) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)

Tactic:
simp_rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, ← mem_Ioi, biInter_eq_iInter]

Premises used: Filter.tendsto_map'_iff, Set.biInter_eq_iInter, Set.mem_Ioi, map_coe_Ioi_atBot