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 : 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∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw₁ : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (i : ι) ↦ s k \ s i
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
⊢ 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∞)
have 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∞))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞))
have 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∞)
Tactic: refine le_antisymm (iSup_mono' fun i => ?_) (iSup_mono fun i => le_measure_diff)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 : ι
⊢ ∃ (i' : ι),
    (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) ≤
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i') : ℝ≥0∞)
have 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∞)
Tactic: rcases hd i k with ⟨j, hji, hjk⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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
⊢ ∃ (i' : ι),
    (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) ≤
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i') : ℝ≥0∞)
have h₁ : (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) ≤
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s j) : ℝ≥0∞)
Tactic: use j
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) (s k \ s i) ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s j) : ℝ≥0∞)
have h₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k \ s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k \ s j) : ℝ≥0∞)
Tactic: rw [← measure_diff hjk (h _) (this _ hjk)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
have refine : LE.le (α := ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
Tactic: refine le_antisymm (le_iInf fun i ↦ measure_mono <| iInter_subset _ _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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∞)
⊢ LE.le (α := ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
have this : Nonempty ι
Tactic: have := hfin.nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 ι
⊢ LE.le (α := ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
have 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∞)
Tactic: rcases exists_seq_antitone_tendsto_atTop_atBot ι with ⟨x, hxm, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
have refine : ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine .symm <| (hs.comp_antitone hxm).directed_ge.measure_iInter (fun n ↦ hsm _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rcases : ∀ (k : ι) (hk : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rcases hfin with ⟨k, hk⟩
Cleared hypotheses: hfin
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
⊢ ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rcases : ∀ (n : ℕ) (hn : x n ≤ k), ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (x i)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rcases (hx.eventually_le_atBot k).exists with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
have refine : ∀ (i : ι), ∃ (i_1 : ℕ), s (x i_1) ⊆ s i
Tactic: refine measure_mono <| iInter_mono' fun i ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 : ι
⊢ ∃ (i_1 : ℕ), s (x i_1) ⊆ s i
have rcases : ∀ (n : ℕ) (hn : x n ≤ i), ∃ (i_1 : ℕ), s (x i_1) ⊆ s i
Tactic: rcases (hx.eventually_le_atBot i).exists with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
have μ₁ : Eq (α := ℝ≥0∞) (⨅ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s (x n)) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), s (x n)) : ℝ≥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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
have μ₂ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), s (x n)) : ℝ≥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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have 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∞)
Tactic: obtain ⟨i, hi⟩ := hfin
Cleared hypotheses: hfin
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have this : Nonempty ι
Tactic: have : Nonempty ι := ⟨i⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 : ι
⊢ s i =ᶠ[ae μ] t i
have h : ∀ (ω : α) (hω : Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x), s i ω = t i ω
Tactic: filter_upwards [hs] with ω hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 ω
have h : ω ∈ s i ↔ ω ∈ t i
Tactic: suffices ω ∈ s i ↔ ω ∈ t i from propext this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have hst : ∀ (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ω
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have hMono : Monotone t
Tactic: have hMono : Monotone t := fun i j hij ω hω ↦ ⟨hω.2 hij hω.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 : 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∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), t 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)]⟩]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
have refine : ⋂ (i : ι), s i =ᶠ[ae μ] ⋂ (i : ι), t i
Tactic: refine measure_congr ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 : ι), t i
have nth_rw : (⋂ (i : ι), s i) ∩ univ =ᶠ[ae μ] (⋂ (i : ι), s i) ∩ {ω : α | Monotone (β := Prop) fun (x : ι) ↦ ω ∈ s x}
Tactic: nth_rw 1 [← iInter_inter, ← inter_univ (⋂ i, s i)]
-- 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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have refine : ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ιᵒᵈ) ↦ ω ∈ s x
Tactic: refine measure_iInter_of_ae_monotone (ι := ιᵒᵈ) ?_ hsm hfin
-- 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∞)
⊢ ∀ᵐ (ω : α) ∂μ, Monotone (β := Prop) fun (x : ιᵒᵈ) ↦ ω ∈ s x
have 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
Tactic: filter_upwards [hs] with ω hω using hω.dual_left