awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 = ∅
i j : ι
hij : i ≠ j
⊢ (AEDisjoint μ on s) i j

Tactic:
(disjoint_iff_inter_eq_empty.mpr (H i j hij)).aedisjoint

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty, Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 = ∅
i j : ι
hij : i ≠ j
⊢ (AEDisjoint μ on s) i j

Tactic:
exact (disjoint_iff_inter_eq_empty.mpr (H i j hij)).aedisjoint

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty, Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
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∞)
⊢ ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty

Tactic:
contrapose! H
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 = ∅
apply : (↑s : Set ι).Pairwise (AEDisjoint μ on t)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
apply sum_measure_le_measure_univ h

Premises used: MeasureTheory.sum_measure_le_measure_univ
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 = ∅
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
hij : i ≠ j
⊢ (AEDisjoint μ on t) i j

Tactic:
(disjoint_iff_inter_eq_empty.mpr (H i hi j hj hij)).aedisjoint

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty, Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 = ∅
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
hij : i ≠ j
⊢ (AEDisjoint μ on t) i j

Tactic:
exact (disjoint_iff_inter_eq_empty.mpr (H i hi j hj hij)).aedisjoint

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty, Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
rw : ¬Disjoint s t
⊢ (s ∩ t).Nonempty

Tactic:
rw [← Set.not_disjoint_iff_nonempty_inter]

Premises used: Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
contrapose! :
  ∀ (h : Disjoint s t),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
      (μ : (a : Set α) → ℝ≥0∞) u
⊢ ¬Disjoint s t

Tactic:
contrapose! h
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : Disjoint s t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)

Tactic:
(measure_union h ht).symm

Premises used: MeasureTheory.measure_union, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : Disjoint s t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
measure_mono (union_subset h's h't)

Premises used: Set.union_subset, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : Disjoint s t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) u

Tactic:
calc
    μ s + μ t = μ (s ∪ t) := (measure_union h ht).symm
    _ ≤ μ u := measure_mono (union_subset h's h't)

Premises used: Set.union_subset, MeasureTheory.measure_mono, MeasureTheory.measure_union, Union.union, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) u <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [add_comm] at h

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
rw : (t ∩ s).Nonempty
⊢ (s ∩ t).Nonempty

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
⊢ (t ∩ s).Nonempty

Tactic:
nonempty_inter_of_measure_lt_add μ hs h't h's h

Premises used: MeasureTheory.nonempty_inter_of_measure_lt_add
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
⊢ (t ∩ s).Nonempty

Tactic:
exact nonempty_inter_of_measure_lt_add μ hs h't h's h

Premises used: MeasureTheory.nonempty_inter_of_measure_lt_add
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
rcases :
  ∀ (e : ι → ℕ) (he : Injective e),
    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 Countable.exists_injective_nat ι with ⟨e, he⟩

Premises used: Countable.exists_injective_nat
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
generalize ht : Function.extend e s ⊥ = t

Premises used: Bot.bot, Function.extend
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
⊢ Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t

Tactic:
replace hd : Directed (· ⊆ ·) t := ht ▸ hd.extend_bot he
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
    (⨆ (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

Premises used: Set.iSup_eq_iUnion, Pi.bot_apply, MeasureTheory.measure_empty, Function.apply_extend, Set.bot_eq_empty, Function.comp_def, DFunLike.coe, iSup_extend_bot
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞) (⨆ (i : ι), s i) : ℝ≥0∞)
    (⨆ (n : ℕ), Function.extend e (fun (x : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s x)) (fun (x : ℕ) ↦ 0) n : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
this.trans (iSup_extend_bot he _)

Premises used: Set.iUnion, iSup_extend_bot, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞) (⨆ (i : ι), s i) : ℝ≥0∞)
    (⨆ (n : ℕ), Function.extend e (fun (x : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s x)) (fun (x : ℕ) ↦ 0) n : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
exact this.trans (iSup_extend_bot he _)

Premises used: iSup_extend_bot, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
suffices :
  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∞)

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 _)
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)

Tactic:
le_antisymm ?_ (iSup_le fun i ↦ measure_mono <| subset_iUnion _ _)

Premises used: Set.subset_iUnion, le_antisymm, MeasureTheory.measure_mono, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
refine :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞)
    (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥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 _ _)

Premises used: Set.subset_iUnion, le_antisymm, MeasureTheory.measure_mono, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
⊢ ∀ (n : ℕ), MeasurableSet (Td n)

Tactic:
have hm : ∀ n, MeasurableSet (Td n) := .disjointed fun n ↦ measurableSet_toMeasurable _ _
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
rw₁ 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∞)

Tactic:
rw [iUnion_disjointed, measure_iUnion_toMeasurable]

Premises used: iUnion_disjointed, MeasureTheory.measure_iUnion_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 : ℕ), Td n) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (Td n) : ℝ≥0∞)

Tactic:
measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (Td n))
    (⨆ (I : Finset ℕ), ∑ n ∈ I, (μ : (a : Set α) → ℝ≥0∞) (Td n))

Tactic:
ENNReal.tsum_eq_iSup_sum

Premises used: ENNReal.tsum_eq_iSup_sum
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 ℕ
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))
⊢ 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⟩

Premises used: Directed.finset_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 ℕ
N : ℕ
hN : ∀ i ∈ I, t i ⊆ t N
⊢ Eq (α := ℝ≥0∞) (∑ n ∈ I, (μ : (a : Set α) → ℝ≥0∞) (Td n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ n ∈ I, Td n) : ℝ≥0∞)

Tactic:
(measure_biUnion_finset ((disjoint_disjointed T).set_pairwise I) fun n _ => hm n).symm

Premises used: SetLike.coe, MeasureTheory.measure_biUnion_finset, disjoint_disjointed, Eq.symm, Pairwise.set_pairwise
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 ℕ
N : ℕ
hN : ∀ i ∈ I, t i ⊆ t N
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ n ∈ I, Td n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ n ∈ I, T n) : ℝ≥0∞)

Tactic:
measure_mono (iUnion₂_mono fun n _hn => disjointed_subset _ _)

Premises used: Set.iUnion₂_mono, MeasureTheory.measure_mono, disjointed_subset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 ℕ
N : ℕ
hN : ∀ i ∈ I, t i ⊆ t N
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ n ∈ I, T n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ n ∈ I, t n) : ℝ≥0∞)

Tactic:
measure_biUnion_toMeasurable I.countable_toSet _

Premises used: MeasureTheory.measure_biUnion_toMeasurable, Finset.countable_toSet
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 ℕ
N : ℕ
hN : ∀ i ∈ I, t i ⊆ t N
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ n ∈ I, t n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t N) : ℝ≥0∞)

Tactic:
measure_mono (iUnion₂_subset hN)

Premises used: Set.iUnion₂_subset, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 ℕ
N : ℕ
hN : ∀ i ∈ I, t i ⊆ t N
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t N) : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)

Tactic:
le_iSup (μ ∘ t) N

Premises used: Function.comp, le_iSup, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 ℕ
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:
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

Premises used: Set.iUnion₂_subset, MeasureTheory.measure_biUnion_toMeasurable, Function.comp, le_iSup, Set.iUnion₂_mono, SetLike.coe, MeasureTheory.measure_biUnion_finset, MeasureTheory.measure_mono, Finset.countable_toSet, disjointed_subset, disjoint_disjointed, Eq.symm, DFunLike.coe, Set.iUnion, Finset.sum, Pairwise.set_pairwise
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), t n) : ℝ≥0∞)
    (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t 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

Premises used: Finset, ENNReal.tsum_eq_iSup_sum, MeasureTheory.measure_iUnion_le, Nat, iSup_le, DFunLike.coe, Set.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
s : ι → Set α
hs : Monotone s
h : IsEmpty ι
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp
-- 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 ι
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∞)
⊢ 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⟩

Premises used: Filter.exists_seq_monotone_tendsto_atTop_atTop
-- 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
inr :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (a : ℕ), s (x a)) : ℝ≥0∞)
    (⨆ (a : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s (x a)) : ℝ≥0∞)
rw : Monotone (β := ℝ≥0∞) fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s i)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [← hs.iUnion_comp_tendsto_atTop hx, ← Monotone.iSup_comp_tendsto_atTop _ hx]

Premises used: Monotone.iSup_comp_tendsto_atTop, Monotone.iUnion_comp_tendsto_atTop
-- 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:
(hs.comp hxm).directed_le.measure_iUnion

Premises used: Directed.measure_iUnion, Monotone.comp, 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
h : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ Monotone (β := ℝ≥0∞) fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s i)

Tactic:
fun _ _ h ↦ measure_mono (hs h)

Premises used: Monotone, MeasureTheory.measure_mono