awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Antitone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ Antitone (β := Prop) fun (x : ι) ↦ ω ∈ s x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ Monotone (β := Prop) fun (x : ιᵒᵈ) ↦ ω ∈ s x) x} x}
      a
⊢ ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ιᵒᵈ) ↦ ω ∈ s x
have h₁ : ∀ (a : α), (Antitone (β := Prop) fun (x : ι) ↦ a ∈ s x) → Monotone (β := Prop) fun (x : ιᵒᵈ) ↦ a ∈ s x
Tactic: filter_upwards [hs] with ω hω using hω.dual_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
    (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), ⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)
Tactic: rw [← Antitone.measure_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), ⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
    (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)
have hs : Antitone.{u_9, u_8} (β := Set α) fun (i : ι) ↦ ⋂ (j : ι), ⋂ (_ : j ≤ i), f j
Tactic: rw [← Antitone.measure_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), ⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)
hs : Antitone.{u_9, u_8} (β := Set α) fun (i : ι) ↦ ⋂ (j : ι), ⋂ (_ : j ≤ i), f j
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
    (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)
have hsm : ∀ (i : ι), NullMeasurableSet (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) μ
Tactic: rw [← Antitone.measure_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), ⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)
hs : Antitone.{u_9, u_8} (β := Set α) fun (i : ι) ↦ ⋂ (j : ι), ⋂ (_ : j ≤ i), f j
hsm : ∀ (i : ι), NullMeasurableSet (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
    (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)
have hfin₁ : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← Antitone.measure_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), ⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i' : ι), ⋂ (i : ι), ⋂ (_ : i' ≤ i), f i') : ℝ≥0∞)
Tactic: rw [iInter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_8
ι : Type u_9
x : MeasurableSpace α
μ : Measure α
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞) (∞ : ℝ≥0∞)
have hfin₁ : ∀ (k : ι) (hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f k) : ℝ≥0∞) (∞ : ℝ≥0∞)), k ≤ k
Tactic: refine hfin.imp fun k hk ↦ ne_top_of_le_ne_top hk <| measure_mono <| iInter₂_subset k ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hm : Monotone s
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n)) : Filter ℝ≥0∞)
have h : NeBot.{u_5} (α := ι) atTop
Tactic: refine .of_neBot_imp fun h ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n)) : Filter ℝ≥0∞)
have this : IsDirectedOrder ι
Tactic: have := (atTop_neBot_iff.1 h).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 : ι → ℝ≥0∞) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n)) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) atTop (𝓝 (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)))
Tactic: rw [hm.measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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∞)
have h : NeBot.{u_9} (α := ι) atTop
Tactic: refine .of_neBot_imp fun h ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i)) : Filter ℝ≥0∞)
have this : IsDirectedOrder ι
Tactic: have := (atTop_neBot_iff.1 h).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i)) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (accumulate f i)) atTop
  (𝓝 (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (accumulate f i)))
Tactic: rw [measure_iUnion_eq_iSup_accumulate]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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∞)
have h : NeBot.{u_5} (α := ι) atTop
Tactic: refine .of_neBot_imp fun h ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), s n)) : Filter ℝ≥0∞)
have this : IsDirectedOrder ι
Tactic: have := (atTop_neBot_iff.1 h).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 : ι → ℝ≥0∞) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), s n)) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) atTop (𝓝 (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)))
Tactic: rw [hm.measure_iInter hs hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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∞)
have hne : NeBot.{u_9} (α := ι) atTop
Tactic: refine .of_neBot_imp fun hne ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i)) : Filter ℝ≥0∞)
have left : Nonempty ι
Tactic: cases atTop_neBot_iff.mp hne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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 ι
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i)) : Filter ℝ≥0∞)
have right : IsDirectedOrder ι
Tactic: cases atTop_neBot_iff.mp hne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i)) : Filter ℝ≥0∞)
have intro : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j)) atTop
  (𝓝 (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j)))
Tactic: rw [measure_iInter_eq_iInf_measure_iInter_le hm hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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)
⊢ ∃ (m : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n) < ε
have hFAnti : Antitone F
Tactic: have hFAnti : Antitone F :=
      fun i j hij => measure_mono (biInter_subset_biInter_left fun k hki => le_trans hki hij)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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 ι := ⋯
⊢ ∃ (m : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n) < ε
have this₁ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : ι), F n < ε
Tactic: rw [ENNReal.tendsto_atTop_zero_iff_lt_of_antitone hFAnti] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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
⊢ ∃ (m : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), ⋂ (_ : n ≤ m), f n) < ε
have suffices : Tendsto F atTop (𝓝 0)
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ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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
⊢ Tendsto F atTop (𝓝 0)
have hzero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), f n) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hzero : μ (⋂ n, f n) = 0 := by
    simp only [hfem, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 (𝓝 0)
have rw : Tendsto F atTop (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ι), f n)))
Tactic: rw [← hzero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)
have pos : ∀ (ha : Order.IsPredPrelimit a),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)
have neg : ∀ (ha : ¬Order.IsPredPrelimit a),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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
have rw : IsCountablyGenerated (α := (↑(Ioi a) : Type u_8)) (comap (Subtype.val (p := fun (x : ι) ↦ x ∈ Ioi a)) (𝓝[>] a))
Tactic: rw [← comap_coe_Ioi_nhdsGT a ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)
have 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∞)
Tactic: simp_rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, ← mem_Ioi, biInter_eq_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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
⊢ 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∞)
have pos : ∀ (i : { x : ι // x ∈ Ioi a }), NullMeasurableSet (s (↑i : ι)) μ
Tactic: apply tendsto_measure_iInter_atBot
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 : ∀ (i : { x : ι // x ∈ Ioi a }), NullMeasurableSet (s (↑i : ι)) μ
⊢ 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∞)
have pos₁ : Monotone.{u_8, u_1} (β := Set α) fun (x : { x : ι // x ∈ Ioi a }) ↦ s (↑x : ι)
Tactic: apply tendsto_measure_iInter_atBot