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 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
i : ι
n : ℕ
hn : x n ≤ i
⊢ ∃ (i_1 : ℕ), s (x i_1) ⊆ s i

Tactic:
⟨n, hs hn⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
i : ι
n : ℕ
hn : x n ≤ i
⊢ ∃ (i_1 : ℕ), s (x i_1) ⊆ s i

Tactic:
exact ⟨n, hs hn⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
μ₁ :
  Eq (α := ℝ≥0∞) (⨅ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s (x n)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), s (x n)) : ℝ≥0∞)
μ₂ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), s (x n)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)

Tactic:
calc
    ⨅ i, μ (s i) ≤ ⨅ n, μ (s (x n)) := le_iInf_comp (μ ∘ s) x
    _ = μ (⋂ n, s (x n)) := by
      refine .symm <| (hs.comp_antitone hxm).directed_ge.measure_iInter (fun n ↦ hsm _) ?_
      rcases hfin with ⟨k, hk⟩
      rcases (hx.eventually_le_atBot k).exists with ⟨n, hn⟩
      exact ⟨n, ne_top_of_le_ne_top hk <| measure_mono <| hs hn⟩
    _ ≤ μ (⋂ i, s i) := by
      refine measure_mono <| iInter_mono' fun i ↦ ?_
      rcases (hx.eventually_le_atBot i).exists with ⟨n, hn⟩
      exact ⟨n, hs hn⟩

Premises used: Set.iInter, Function.comp, le_iInf_comp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
obtain :
  ∀ (i : ι) (hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
obtain ⟨i, hi⟩ := hfin
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Nonempty ι

Tactic:
have : Nonempty ι := ⟨i⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i_1 : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i_1) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
i : ι
h : ∀ (ω : α) (hω : Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x), s i ω = t i ω
⊢ s i =ᶠ[ae μ] t i

Tactic:
filter_upwards [hs] with ω hω
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i_1 : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i_1) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
i : ι
ω : α
hω : Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
h : ω ∈ s i ↔ ω ∈ t i
⊢ s i ω = t i ω

Tactic:
suffices ω ∈ s i ↔ ω ∈ t i from propext this
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i_1 : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i_1) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
i : ι
ω : α
hω : Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
⊢ ω ∈ s i ↔ ω ∈ t i

Tactic:
simpa [t] using fun _ ↦ hω
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
⊢ ∀ (i : ι), s i =ᶠ[ae μ] t i

Tactic:
have hst (i : ι) : s i =ᵐ[μ] t i := by
    filter_upwards [hs] with ω hω
    suffices ω ∈ s i ↔ ω ∈ t i from propext this
    simpa [t] using fun _ ↦ hω
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᶠ[ae μ] t i
⊢ Monotone t

Tactic:
have hMono : Monotone t := fun i j hij ω hω ↦ ⟨hω.2 hij hω.1, hω.2⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᶠ[ae μ] t i
hMono : Monotone t
rwa rwa₁ rwa₂ rwa₃ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [← measure_congr (hst i)]

Premises used: MeasureTheory.measure_congr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᶠ[ae μ] t i
hMono : Monotone t
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), t i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [iInf_congr <| fun i ↦ measure_congr <| hst i,
    ← hMono.measure_iInter (fun i ↦ (hsm i).congr (hst i)) ⟨i, by rwa [← measure_congr (hst i)]⟩]

Premises used: MeasureTheory.measure_congr, iInf_congr, Monotone.measure_iInter, MeasureTheory.NullMeasurableSet.congr, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᶠ[ae μ] t i
hMono : Monotone t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), t i) : ℝ≥0∞)

Tactic:
measure_congr ?_

Premises used: MeasureTheory.measure_congr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᶠ[ae μ] t i
hMono : Monotone t
refine : ⋂ (i : ι), s i =ᶠ[ae μ] ⋂ (i : ι), t i
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), t i) : ℝ≥0∞)

Tactic:
refine measure_congr ?_

Premises used: MeasureTheory.measure_congr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᶠ[ae μ] t i
hMono : Monotone t
nth_rw : (⋂ (i : ι), s i) ∩ univ =ᶠ[ae μ] (⋂ (i : ι), s i) ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
⊢ ⋂ (i : ι), s i =ᶠ[ae μ] ⋂ (i : ι), t i

Tactic:
nth_rw 1 [← iInter_inter, ← inter_univ (⋂ i, s i)]

Premises used: Set.iInter, Set.inter_univ, Set.iInter_inter
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᶠ[ae μ] t i
hMono : Monotone t
⊢ ⋂ (i : ι), s i =ᶠ[ae μ] ⋂ (i : ι), s i

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atBot
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Nonempty ι
t : ι → Set α := fun (i : ι) ↦ s i ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᶠ[ae μ] t i
hMono : Monotone t
⊢ (⋂ (i : ι), s i) ∩ univ =ᶠ[ae μ] (⋂ (i : ι), s i) ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}

Tactic:
exact ae_eq_set_inter (by rfl) (ae_eq_univ.2 hs).symm

Premises used: Iff.mpr, MeasureTheory.ae_eq_set_inter, MeasureTheory.ae_eq_univ, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
hs.dual_left.measure_iInter hsm hfin

Premises used: Monotone.measure_iInter, Antitone.dual_left, OrderDual
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
measure_iInter_of_ae_monotone (ι := ιᵒᵈ) ?_ hsm hfin

Premises used: OrderDual, MeasureTheory.measure_iInter_of_ae_monotone
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
refine : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ιᵒᵈ) ↦ ω ∈ s x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
refine measure_iInter_of_ae_monotone (ι := ιᵒᵈ) ?_ hsm hfin

Premises used: MeasureTheory.measure_iInter_of_ae_monotone
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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ω : Antitone (β := Prop) fun (x : ι) ↦ ω ∈ s x
⊢ Monotone (β := Prop) fun (x : ιᵒᵈ) ↦ ω ∈ s x

Tactic:
hω.dual_left

Premises used: Set.Mem, Antitone.dual_left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
h₁ h₂ : ∀ (ω : α) (hω : Antitone (β := Prop) fun (x : ι) ↦ ω ∈ s x), Monotone (β := Prop) fun (x : ιᵒᵈ) ↦ ω ∈ s x
⊢ ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ιᵒᵈ) ↦ ω ∈ s x

Tactic:
filter_upwards [hs] with ω hω using hω.dual_left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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) μ
hfin₁ : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
    (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)

Tactic:
rw [← Antitone.measure_iInter]

Premises used: Antitone.measure_iInter
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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' : ι), ⋂ (i : ι), ⋂ (_ : i' ≤ i), f i') : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), f i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), ⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞)

Tactic:
rw [iInter_comm]

Premises used: Set.iInter_comm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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' : ι), ⋂ (i : ι), ⋂ (_ : i' ≤ i), f i') : ℝ≥0∞)

Tactic:
congrArg μ <| iInter_congr fun i ↦ (biInf_const nonempty_Ici).symm

Premises used: congrArg, Set.iInter_congr, biInf_const, Set.nonempty_Ici, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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' : ι), ⋂ (i : ι), ⋂ (_ : i' ≤ i), f i') : ℝ≥0∞)

Tactic:
exact congrArg μ <| iInter_congr fun i ↦ (biInf_const nonempty_Ici).symm

Premises used: congrArg, Set.iInter_congr, biInf_const, Set.nonempty_Ici, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
⊢ Antitone.{u_9, u_8} (β := Set α) fun (i : ι) ↦ ⋂ (j : ι), ⋂ (_ : j ≤ i), f j

Tactic:
fun i j h ↦ biInter_mono (Iic_subset_Iic.2 h) fun _ _ ↦ Set.Subset.rfl

Premises used: Iff.mpr, Set.biInter_mono, Set.Mem, Set.Iic_subset_Iic, Antitone, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
⊢ Antitone.{u_9, u_8} (β := Set α) fun (i : ι) ↦ ⋂ (j : ι), ⋂ (_ : j ≤ i), f j

Tactic:
exact fun i j h ↦ biInter_mono (Iic_subset_Iic.2 h) fun _ _ ↦ Set.Subset.rfl

Premises used: Iff.mpr, Set.biInter_mono, Set.Iic_subset_Iic, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 : ι), NullMeasurableSet (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) μ

Tactic:
fun i ↦ .biInter (to_countable _) fun _ _ ↦ h _

Premises used: Set.Mem, Preorder.toLE, LE.le, Set.to_countable, MeasureTheory.NullMeasurableSet.biInter
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 : ι), NullMeasurableSet (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) μ

Tactic:
exact fun i ↦ .biInter (to_countable _) fun _ _ ↦ h _
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)

Tactic:
hfin.imp fun k hk ↦ ne_top_of_le_ne_top hk <| measure_mono <| iInter₂_subset k ?_

Premises used: Set.iInter₂_subset, Exists.imp, ne_top_of_le_ne_top, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
hfin₁ : ∀ (k : ι) (hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f k) : ℝ≥0∞) (∞ : ℝ≥0∞)), k ≤ k
⊢ ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (j : ι), ⋂ (_ : j ≤ i), f j) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine hfin.imp fun k hk ↦ ne_top_of_le_ne_top hk <| measure_mono <| iInter₂_subset k ?_

Premises used: Exists.imp, ne_top_of_le_ne_top, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f k) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ k ≤ k

Tactic:
rfl
-- 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
⊢ 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 α
hm : Monotone s
⊢ NeBot.{u_5} (α := ι) atTop

Tactic:
refine .of_neBot_imp fun h ↦ ?_