awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : s.Nonempty
h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h_disj : Disjoint s sᶜ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞)

Tactic:
rw [← union_compl_self s, measure_union h_disj hs.compl, measure_union h_disj hs.compl] at h_univ

Premises used: Set.union_compl_self, MeasurableSet.compl, MeasureTheory.measure_union
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : s.Nonempty
h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h_disj : Disjoint s sᶜ
h_univ₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞)
⊢ MeasurableSet s

Tactic:
rw [← union_compl_self s, measure_union h_disj hs.compl, measure_union h_disj hs.compl] at h_univ

Premises used: Set.union_compl_self, MeasurableSet.compl, MeasureTheory.measure_union
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : s.Nonempty
h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h_disj : Disjoint s sᶜ
h_univ₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞)
hs₁ : MeasurableSet s
⊢ s.Nonempty

Tactic:
rw [← union_compl_self s, measure_union h_disj hs.compl, measure_union h_disj hs.compl] at h_univ

Premises used: Set.union_compl_self, MeasurableSet.compl, MeasureTheory.measure_union
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : s.Nonempty
h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h_disj : Disjoint s sᶜ
h_univ₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞)
hs₁ : MeasurableSet s
x : s.Nonempty
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← union_compl_self s, measure_union h_disj hs.compl, measure_union h_disj hs.compl] at h_univ

Premises used: Set.union_compl_self, MeasurableSet.compl, MeasureTheory.measure_union
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : s.Nonempty
h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h_disj : Disjoint s sᶜ
h_univ₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞)
hs₁ : MeasurableSet s
x : s.Nonempty
h_lt₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Disjoint s sᶜ

Tactic:
rw [← union_compl_self s, measure_union h_disj hs.compl, measure_union h_disj hs.compl] at h_univ

Premises used: Set.union_compl_self, MeasurableSet.compl, MeasureTheory.measure_union
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
s : Set α
h_univ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞)
hs : MeasurableSet s
h : s.Nonempty
h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h_disj : Disjoint s sᶜ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
s : Set α
h_univ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞)
hs : MeasurableSet s
h : s.Nonempty
h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h_disj : Disjoint s sᶜ
⊢ False

Tactic:
exact ENNReal.add_lt_add_of_lt_of_le (by finiteness) h_lt (hμν sᶜ) |>.not_ge h_univ.symm.le

Premises used: Compl.compl, Eq.le, ENNReal.add_lt_add_of_lt_of_le, LT.lt.not_ge, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hsum : Ne (α := ℝ≥0∞) (∑' (x : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f x)) ∞
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ μ.real (f x)

Tactic:
apply ENNReal.summable_toReal

Premises used: ENNReal.summable_toReal
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hsum : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (∑' (x : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f x)) ∞

Tactic:
rw [← MeasureTheory.measure_iUnion hf₂ hf₁]

Premises used: MeasureTheory.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ne_of_lt (measure_lt_top _ _)

Premises used: MeasureTheory.measure_lt_top, ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ne_of_lt (measure_lt_top _ _)

Premises used: MeasureTheory.measure_lt_top, ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
p : α → Prop
hp : NullMeasurableSet {a : α | p a} μ
rw : (∀ᵐ (a : α) ∂μ, p a) ↔ {a : α | p a} =ᶠ[ae μ] univ
rw₁ : (∀ᵐ (a : α) ∂μ, p a) ↔ {a : α | p a} ∈ ae μ
rw₂ rw₃ : {x : α | p x} ∈ ae μ ↔ {a : α | p a} ∈ ae μ
⊢ (∀ᵐ (a : α) ∂μ, p a) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | p a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [← ae_eq_univ_iff_measure_eq hp, eventuallyEq_univ, eventually_iff]

Premises used: Filter.eventually_iff, MeasureTheory.ae_eq_univ_iff_measure_eq, Filter.eventuallyEq_univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Set α
hs : NullMeasurableSet s μ
⊢ (∀ᵐ (a : α) ∂μ, a ∈ s) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
ae_iff_measure_eq hs

Premises used: Set.Mem, setOf, MeasureTheory.ae_iff_measure_eq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
⊢ Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i

Tactic:
have decr : Antitone fun n ↦ ⋃ i ≥ n, Es i :=
    fun n m hnm ↦ biUnion_mono (fun _ hi ↦ le_trans hnm hi) (fun _ _ ↦ subset_rfl)
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
apply : Subset.{u_5} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅
⊢ Eq.{u_5 + 1} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅

Tactic:
apply subset_antisymm _ (empty_subset _)

Premises used: subset_antisymm, Set.empty_subset
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
x : X
hx : Membership.mem (γ := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) x
⊢ ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1

Tactic:
simp only [mem_iInter, mem_iUnion, exists_prop] at hx

Premises used: Set.mem_iUnion, exists_prop, Set.mem_iInter
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
obtain : ∀ j ≥ 0, ∀ (x_in_Es_j : x ∈ Es j), Membership.mem (γ := Set X) ∅ x
⊢ Membership.mem (γ := Set X) ∅ x

Tactic:
obtain ⟨j, _, x_in_Es_j⟩ := hx 0

Premises used: OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left : j ≥ 0
x_in_Es_j : x ∈ Es j
obtain : ∀ (k : ℕ) (k_gt_j : k ≥ j + 1) (x_in_Es_k : x ∈ Es k), Membership.mem (γ := Set X) ∅ x
⊢ Membership.mem (γ := Set X) ∅ x

Tactic:
obtain ⟨k, k_gt_j, x_in_Es_k⟩ := hx (j + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left : j ≥ 0
x_in_Es_j : x ∈ Es j
k : ℕ
k_gt_j : k ≥ j + 1
x_in_Es_k : x ∈ Es k
⊢ x ≠ x

Tactic:
have oops := (Es_disj (Nat.ne_of_lt k_gt_j)).ne_of_mem x_in_Es_j x_in_Es_k
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left : j ≥ 0
x_in_Es_j : x ∈ Es j
k : ℕ
k_gt_j : k ≥ j + 1
x_in_Es_k : x ∈ Es k
oops : x ≠ x
⊢ Membership.mem (γ := Set X) ∅ x

Tactic:
contradiction
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
⊢ Eq.{u_5 + 1} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅

Tactic:
have nothing : ⋂ n, ⋃ i ≥ n, Es i = ∅ := by
    apply subset_antisymm _ (empty_subset _)
    intro x hx
    simp only [mem_iInter, mem_iUnion, exists_prop] at hx
    obtain ⟨j, _, x_in_Es_j⟩ := hx 0
    obtain ⟨k, k_gt_j, x_in_Es_k⟩ := hx (j + 1)
    have oops := (Es_disj (Nat.ne_of_lt k_gt_j)).ne_of_mem x_in_Es_j x_in_Es_k
    contradiction
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
nothing : Eq.{u_5 + 1} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅
n : ℕ
⊢ NullMeasurableSet (⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) μ

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
nothing : Eq.{u_5 + 1} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅
⊢ Tendsto (α := ℕ) (β := ℝ≥0∞)
    (comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i : ℕ → ℝ≥0∞) atTop
    (𝓝 ((μ : (a : Set X) → ℝ≥0∞) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i)) : Filter ℝ≥0∞)

Tactic:
have key := tendsto_measure_iInter_atTop (μ := μ) (fun n ↦ by measurability)
    decr ⟨0, measure_ne_top _ _⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
nothing : Eq.{u_5 + 1} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅
key :
  Tendsto (α := ℕ) (β := ℝ≥0∞)
    (comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i : ℕ → ℝ≥0∞) atTop
    (𝓝 ((μ : (a : Set X) → ℝ≥0∞) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i)) : Filter ℝ≥0∞)
⊢ Tendsto (α := ℕ) (β := ℝ≥0∞)
    (comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)

Tactic:
simp only [nothing, measure_empty] at key

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
nothing : Eq.{u_5 + 1} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅
key :
  Tendsto (α := ℕ) (β := ℝ≥0∞)
    (comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
⊢ Tendsto (α := ℕ) (β := ℝ≥0∞)
    (comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)

Tactic:
key
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
nothing : Eq.{u_5 + 1} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅
key :
  Tendsto (α := ℕ) (β := ℝ≥0∞)
    (comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
⊢ Tendsto (α := ℕ) (β := ℝ≥0∞)
    (comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)

Tactic:
convert! key
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hst : μ (s \ t) ≠ ∞ := (measure_lt_top_of_subset diff_subset hs').ne
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hts : μ (t \ s) ≠ ∞ := (measure_lt_top_of_subset diff_subset ht').ne
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hts : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
rw :
  |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))| ≤
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
⊢ |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)| ≤
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t))

Tactic:
rw [this, measure_symmDiff_eq hs ht, ENNReal.toReal_add hst hts]

Premises used: ENNReal.toReal_add, MeasureTheory.measure_symmDiff_eq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hts : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
⊢ |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))| ≤
    |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))| + |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))|

Tactic:
abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal

Premises used: abs_sub, SDiff.sdiff, ENNReal.toReal, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hts : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
h : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) = |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))|
h₁ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s)) = |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))|
⊢ |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))| ≤
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))

Tactic:
convert! abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal

Premises used: abs_sub, SDiff.sdiff, ENNReal.toReal, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hts : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) = |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))|

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hts : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s)) = |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))|

Tactic:
simp