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 : IsDirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hs : Monotone s
h : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (a : ℕ), s (x a)) : ℝ≥0∞)
    (⨆ (a : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s (x a)) : ℝ≥0∞)

Tactic:
exacts [(hs.comp hxm).directed_le.measure_iUnion, fun _ _ h ↦ measure_mono (hs h)]

Premises used: Directed.measure_iUnion, Monotone.comp, MeasureTheory.measure_mono, Monotone.directed_le
-- 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 : Monotone s
⊢ IsEmpty ι ∨ Nonempty ι

Tactic:
cases isEmpty_or_nonempty ι with
  | inl _ => simp
  | inr _ =>
    rcases exists_seq_monotone_tendsto_atTop_atTop ι with ⟨x, hxm, hx⟩
    rw [← hs.iUnion_comp_tendsto_atTop hx, ← Monotone.iSup_comp_tendsto_atTop _ hx]
    exacts [(hs.comp hxm).directed_le.measure_iUnion, fun _ _ h ↦ measure_mono (hs h)]

Premises used: isEmpty_or_nonempty, MeasureTheory.measure_mono
-- 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 : Antitone s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
hs.dual_left.measure_iUnion

Premises used: Antitone.dual_left, Monotone.measure_iUnion, 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
f : ι → Set α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : ι), accumulate f x) : ℝ≥0∞)
    (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i) : ℝ≥0∞)
    (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)

Tactic:
rw [← iUnion_accumulate]

Premises used: Set.iUnion_accumulate
-- 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
f : ι → Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : ι), accumulate f x) : ℝ≥0∞)
    (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)

Tactic:
monotone_accumulate.measure_iUnion

Premises used: Set.monotone_accumulate, Monotone.measure_iUnion
-- 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
f : ι → Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : ι), accumulate f x) : ℝ≥0∞)
    (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)

Tactic:
exact monotone_accumulate.measure_iUnion

Premises used: Set.monotone_accumulate, Monotone.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
hd : DirectedOn ((fun (x1 x2 : Set α) ↦ x1 ⊆ x2) on s) t
⊢ Countable.{u_5 + 1} (↑t : Type u_5)

Tactic:
haveI := ht.to_subtype
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
hd : DirectedOn ((fun (x1 x2 : Set α) ↦ x1 ⊆ x2) on s) t
this : Countable.{u_5 + 1} (↑t : Type u_5)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : (↑t : Type u_5)), s (↑x : ι)) : ℝ≥0∞)
    (⨆ i ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (⨆ (i : { x : ι // x ∈ t }), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)))
    (⨆ i ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s i))
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) (⨆ (i : { x : ι // x ∈ t }), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)))
    (⨆ (i : (↑t : Type u_5)), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ t, s i) : ℝ≥0∞) (⨆ i ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [biUnion_eq_iUnion, hd.directed_val.measure_iUnion, ← iSup_subtype'']

Premises used: Directed.measure_iUnion, iSup_subtype'', DirectedOn.directed_val, Set.biUnion_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
hfin : ∃ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
rcases :
  ∀ (k : ι) (hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥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:
rcases hfin with ⟨k, hk⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ t ⊆ s k, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have : ∀ t ⊆ s k, μ t ≠ ∞ := fun t ht => ne_top_of_le_ne_top hk (measure_mono ht)
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : ∀ t ⊆ s k, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞)
      (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞)
      (⨆ (i : ι),
          HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) :
        ℝ≥0∞)
rw₁ : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (i : ι) ↦ s k \ s i
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [← ENNReal.sub_sub_cancel hk (iInf_le (fun i => μ (s i)) k), ENNReal.sub_iInf, ←
    ENNReal.sub_sub_cancel hk (measure_mono (iInter_subset _ k)), ←
    measure_diff (iInter_subset _ k) (.iInter h) (this _ (iInter_subset _ k)),
    diff_iInter, Directed.measure_iUnion]

Premises used: Directed.measure_iUnion, ENNReal.sub_sub_cancel, MeasureTheory.NullMeasurableSet.iInter, MeasureTheory.measure_diff, MeasureTheory.measure_mono, ENNReal.sub_iInf, Set.iInter_subset, DFunLike.coe, iInf_le, Set.diff_iInter
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : ∀ t ⊆ s k, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
e_a :
  Eq (α := ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s k \ s i))
    (⨆ (i : ι),
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞))
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞)
      (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞)
      (⨆ (i : ι),
          HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) :
        ℝ≥0∞)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : ∀ t ⊆ s k, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s k \ s i))
    (⨆ (i : ι),
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞))

Tactic:
le_antisymm (iSup_mono' fun i => ?_) (iSup_mono fun i => le_measure_diff)

Premises used: iSup_mono', le_antisymm, MeasureTheory.le_measure_diff, iSup_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : ∀ t ⊆ s k, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
e_a :
  ∀ (i : ι),
    ∃ (i' : ι),
      (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) ≤
        HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (s i') : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s k \ s i))
    (⨆ (i : ι),
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞))

Tactic:
refine le_antisymm (iSup_mono' fun i => ?_) (iSup_mono fun i => le_measure_diff)

Premises used: iSup_mono', le_antisymm, MeasureTheory.le_measure_diff, iSup_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : ∀ t ⊆ s k, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
i : ι
e_a :
  ∀ (j : ι) (hji : s i ⊇ s j) (hjk : s k ⊇ s j),
    ∃ (i' : ι),
      (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) ≤
        HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (s i') : ℝ≥0∞)
⊢ ∃ (i' : ι),
    (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) ≤
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i') : ℝ≥0∞)

Tactic:
rcases hd i k with ⟨j, hji, hjk⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : ∀ t ⊆ s k, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
h₁ :
  (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s j) : ℝ≥0∞)
⊢ ∃ (i' : ι),
    (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) ≤
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i') : ℝ≥0∞)

Tactic:
use j
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : ∀ t ⊆ s k, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
h₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k \ s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k \ s j) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s j) : ℝ≥0∞)

Tactic:
rw [← measure_diff hjk (h _) (this _ hjk)]

Premises used: MeasureTheory.measure_diff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : ∀ t ⊆ s k, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k \ s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k \ s j) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : ∀ t ⊆ s k, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (i : ι) ↦ s k \ s i

Tactic:
hd.mono_comp _ fun _ _ => diff_subset_diff_right

Premises used: Directed.mono_comp, Set.diff_subset_diff_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : ∀ t ⊆ s k, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (i : ι) ↦ s k \ s i

Tactic:
exact hd.mono_comp _ fun _ _ => diff_subset_diff_right

Premises used: Directed.mono_comp, Set.diff_subset_diff_right
-- 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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
le_antisymm (le_iInf fun i ↦ measure_mono <| iInter_subset _ _) ?_

Premises used: le_iInf, le_antisymm, MeasureTheory.measure_mono, Set.iInter_subset
-- 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∞)
refine :
  LE.le (α := ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
refine le_antisymm (le_iInf fun i ↦ measure_mono <| iInter_subset _ _) ?_

Premises used: le_iInf, le_antisymm, MeasureTheory.measure_mono, Set.iInter_subset
-- 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∞)
⊢ Nonempty ι

Tactic:
have := hfin.nonempty
-- 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 ι
rcases :
  ∀ (x : ℕ → ι) (hxm : Antitone x) (hx : Tendsto x atTop atBot),
    LE.le (α := ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥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:
rcases exists_seq_antitone_tendsto_atTop_atBot ι with ⟨x, hxm, hx⟩

Premises used: Filter.exists_seq_antitone_tendsto_atTop_atBot
-- 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
⊢ LE.le (α := ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) (⨅ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s (x n)))

Tactic:
le_iInf_comp (μ ∘ s) x

Premises used: 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 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∞)

Tactic:
.symm <| (hs.comp_antitone hxm).directed_ge.measure_iInter (fun n ↦ hsm _) ?_

Premises used: Antitone.directed_ge, Directed.measure_iInter, Eq.symm, Monotone.comp_antitone
-- 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
refine : ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨅ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s (x n)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), s (x n)) : ℝ≥0∞)

Tactic:
refine .symm <| (hs.comp_antitone hxm).directed_ge.measure_iInter (fun n ↦ hsm _) ?_

Premises used: Antitone.directed_ge, Directed.measure_iInter, Monotone.comp_antitone
-- 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
rcases :
  ∀ (k : ι) (hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rcases hfin with ⟨k, hk⟩
-- 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) μ
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
rcases : ∀ (n : ℕ) (hn : x n ≤ k), ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rcases (hx.eventually_le_atBot k).exists with ⟨n, hn⟩

Premises used: Filter.Tendsto.eventually_le_atBot, Filter.Eventually.exists
-- 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) μ
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
n : ℕ
hn : x n ≤ k
⊢ ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨n, ne_top_of_le_ne_top hk <| measure_mono <| hs hn⟩

Premises used: ne_top_of_le_ne_top, MeasureTheory.measure_mono, 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) μ
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
k : ι
hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)
n : ℕ
hn : x n ≤ k
⊢ ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨n, ne_top_of_le_ne_top hk <| measure_mono <| 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
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), s (x n)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)

Tactic:
measure_mono <| iInter_mono' fun i ↦ ?_

Premises used: MeasureTheory.measure_mono, Set.iInter_mono'
-- 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
refine : ∀ (i : ι), ∃ (i_1 : ℕ), s (x i_1) ⊆ s i
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), s (x n)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)

Tactic:
refine measure_mono <| iInter_mono' fun i ↦ ?_

Premises used: MeasureTheory.measure_mono, Set.iInter_mono'
-- 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 : ι
rcases : ∀ (n : ℕ) (hn : x n ≤ i), ∃ (i_1 : ℕ), s (x i_1) ⊆ s i
⊢ ∃ (i_1 : ℕ), s (x i_1) ⊆ s i

Tactic:
rcases (hx.eventually_le_atBot i).exists with ⟨n, hn⟩

Premises used: Filter.Tendsto.eventually_le_atBot, Filter.Eventually.exists