awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
b : ι
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (M (t b)) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_3 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
have H : ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)
Tactic: have H : ∀ b, (M (t b) ∩ M (⋃ b, s b) : Set α) =ᵐ[μ] M (t b) := by
    refine fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_
    · calc
        μ (M (t b)) = μ (t b) := measure_toMeasurable _
        _ ≤ μ (s b) := h_le b
        _ ≤ μ (M (t b) ∩ M (⋃ b, s b)) :=
          measure_mono <|
            subset_inter ((hsub b).trans <| subset_toMeasurable _ _)
              ((subset_iUnion _ _).trans <| subset_toMeasurable _ _)
    · measurability
    · rw [measure_toMeasurable]
      exact htop b
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞)
ht : t₁ ⊆ t₂
htμ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₁ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ t₁) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₂ ∪ t₂) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : Bool), bif b then s₁ else t₁) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : Bool), bif b then s₂ else t₂) : ℝ≥0∞)
Tactic: rw [union_eq_iUnion, union_eq_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
I : Set β
hc : I.Countable
s : β → Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ I, toMeasurable μ (s b)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ I, s b) : ℝ≥0∞)
have haveI : ∀ (this : Encodable (↑I : Type u_2)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ I, toMeasurable μ (s b)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ I, s b) : ℝ≥0∞)
Tactic: haveI := hc.toEncodable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : (↑s : Set ι).Pairwise (AEDisjoint μ on t)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, t b) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [← measure_biUnion_finset₀ H h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : Pairwise (AEDisjoint μ on s)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) (⨆ (s_1 : Finset ι), ∑ a ∈ s_1, (μ : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [ENNReal.tsum_eq_iSup_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ ∃ (i : ι) (j : ι), i ≠ j ∧ (s i ∩ s j).Nonempty
have contrapose! : ∀ (H : ∀ (i j : ι) (_ : i ≠ j), s i ∩ s j = ∅),
  LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι) (_ : i ≠ j), s i ∩ s j = ∅
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have apply : Pairwise (AEDisjoint μ on s)
Tactic: apply tsum_measure_le_measure_univ hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞)
⊢ ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty
have contrapose! : ∀ (H : ∀ (i : ι) (_ : i ∈ s) (j : ι) (_ : j ∈ s) (_h : i ≠ j), t i ∩ t j = ∅),
  LE.le (α := ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : ∀ (i : ι) (_ : i ∈ s) (j : ι) (_ : j ∈ s) (_h : i ≠ j), t i ∩ t j = ∅
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have apply : (↑s : Set ι).Pairwise (AEDisjoint μ on t)
Tactic: apply sum_measure_le_measure_univ h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h :
  (μ : (a : Set α) → ℝ≥0∞) u <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (s ∩ t).Nonempty
have rw : ¬Disjoint s t
Tactic: rw [← Set.not_disjoint_iff_nonempty_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h :
  (μ : (a : Set α) → ℝ≥0∞) u <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ¬Disjoint s t
have contrapose! : ∀ (h : Disjoint s t),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) u
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h :
  (μ : (a : Set α) → ℝ≥0∞) u <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (s ∩ t).Nonempty
have h₁ : (μ : (a : Set α) → ℝ≥0∞) u <
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [add_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h :
  (μ : (a : Set α) → ℝ≥0∞) u <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (s ∩ t).Nonempty
have rw : (t ∩ s).Nonempty
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rcases : ∀ (e : ι → ℕ) (he : Injective e),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rcases Countable.exists_injective_nat ι with ⟨e, he⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
e : ι → ℕ
he : Injective e
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have generalize : ∀ (t : ℕ → Set α) (ht : Function.extend e s ⊥ = t),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: generalize ht : Function.extend e s ⊥ = t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have hd₁ : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
Tactic: replace hd : Directed (· ⊆ ·) t := ht ▸ hd.extend_bot he
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
this :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have this₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⨆ (i : ι), s i) : ℝ≥0∞)
  (⨆ (n : ℕ), Function.extend e (fun (x : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s x)) (fun (x : ℕ) ↦ 0) n : ℝ≥0∞)
Tactic: simp only [← ht, Function.apply_extend μ, ← iSup_eq_iUnion, iSup_extend_bot he,
      Function.comp_def, Pi.bot_apply, bot_eq_empty, measure_empty] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have suffices : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)
Tactic: suffices μ (⋃ n, t n) = ⨆ n, μ (t n) by
    simp only [← ht, Function.apply_extend μ, ← iSup_eq_iUnion, iSup_extend_bot he,
      Function.comp_def, Pi.bot_apply, bot_eq_empty, measure_empty] at this
    exact this.trans (iSup_extend_bot he _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)
Tactic: refine le_antisymm ?_ (iSup_le fun i ↦ measure_mono <| subset_iUnion _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
T : ℕ → Set α := fun (n : ℕ) ↦ toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞)
    (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)
have hm : ∀ (n : ℕ), MeasurableSet (Td n)
Tactic: have hm : ∀ n, MeasurableSet (Td n) := .disjointed fun n ↦ measurableSet_toMeasurable _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
T : ℕ → Set α := fun (n : ℕ) ↦ toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), Td n) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), T i) : ℝ≥0∞)
Tactic: rw [iUnion_disjointed, measure_iUnion_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
T : ℕ → Set α := fun (n : ℕ) ↦ toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), T i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), Td n) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), t i) : ℝ≥0∞)
Tactic: rw [iUnion_disjointed, measure_iUnion_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
T : ℕ → Set α := fun (n : ℕ) ↦ toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
I : Finset ℕ
⊢ LE.le (α := ℝ≥0∞) (∑ n ∈ I, (μ : (a : Set α) → ℝ≥0∞) (Td n)) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t n))
have rcases : ∀ (N : ℕ) (hN : ∀ i ∈ I, t i ⊆ t N),
  LE.le (α := ℝ≥0∞) (∑ n ∈ I, (μ : (a : Set α) → ℝ≥0∞) (Td n)) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t n))
Tactic: rcases hd.finset_le I with ⟨N, hN⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
T : ℕ → Set α := fun (n : ℕ) ↦ toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞)
    (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)
have μ₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), Td n) : ℝ≥0∞)
Tactic: calc
    μ (⋃ n, t n) = μ (⋃ n, Td n) := by rw [iUnion_disjointed, measure_iUnion_toMeasurable]
    _ ≤ ∑' n, μ (Td n) := measure_iUnion_le _
    _ = ⨆ I : Finset ℕ, ∑ n ∈ I, μ (Td n) := ENNReal.tsum_eq_iSup_sum
    _ ≤ ⨆ n, μ (t n) := iSup_le fun I => by
      rcases hd.finset_le I with ⟨N, hN⟩
      calc
        (∑ n ∈ I, μ (Td n)) = μ (⋃ n ∈ I, Td n) :=
          (measure_biUnion_finset ((disjoint_disjointed T).set_pairwise I) fun n _ => hm n).symm
        _ ≤ μ (⋃ n ∈ I, T n) := measure_mono (iUnion₂_mono fun n _hn => disjointed_subset _ _)
        _ = μ (⋃ n ∈ I, t n) := measure_biUnion_toMeasurable I.countable_toSet _
        _ ≤ μ (t N) := measure_mono (iUnion₂_subset hN)
        _ ≤ ⨆ n, μ (t n) := le_iSup (μ ∘ t) N
-- 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 : Monotone s
h : Nonempty ι
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have inr : ∀ (x : ℕ → ι) (hxm : Monotone x) (hx : Tendsto x atTop atTop),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rcases exists_seq_monotone_tendsto_atTop_atTop ι 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 : 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∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have inr : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (a : ℕ), s (x a)) : ℝ≥0∞)
  (⨆ (a : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s (x a)) : ℝ≥0∞)
Tactic: rw [← hs.iUnion_comp_tendsto_atTop hx, ← Monotone.iSup_comp_tendsto_atTop _ 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 : IsDirectedOrder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hs : Monotone s
h : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
inr :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (a : ℕ), s (x a)) : ℝ≥0∞)
    (⨆ (a : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s (x a)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : Monotone (β := ℝ≥0∞) fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s i)
Tactic: rw [← hs.iUnion_comp_tendsto_atTop hx, ← Monotone.iSup_comp_tendsto_atTop _ hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have x : 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)]
-- 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
f : ι → Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i) : ℝ≥0∞)
    (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : ι), accumulate f x) : ℝ≥0∞)
  (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)
Tactic: rw [← iUnion_accumulate]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ t, s i) : ℝ≥0∞) (⨆ i ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have this : Countable.{u_5 + 1} (↑t : Type u_5)
Tactic: haveI := ht.to_subtype
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ t, s i) : ℝ≥0∞) (⨆ i ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : (↑t : Type u_5)), s (↑x : ι)) : ℝ≥0∞)
  (⨆ i ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rw [biUnion_eq_iUnion, hd.directed_val.measure_iUnion, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ t, s i) : ℝ≥0∞) (⨆ i ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (⨆ (i : { x : ι // x ∈ t }), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)))
  (⨆ i ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s i))
Tactic: rw [biUnion_eq_iUnion, hd.directed_val.measure_iUnion, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ t, s i) : ℝ≥0∞) (⨆ i ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) (⨆ (i : { x : ι // x ∈ t }), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)))
  (⨆ (i : (↑t : Type u_5)), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)))
Tactic: rw [biUnion_eq_iUnion, hd.directed_val.measure_iUnion, ← iSup_subtype'']
-- 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
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 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∞)
Tactic: rcases hfin with ⟨k, hk⟩
Cleared hypotheses: hfin
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (⨅ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have this : ∀ 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)