awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ hs.toFinset (s := s), f i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_biUnion_finset_le (μ := μ) hs.toFinset f).trans_lt _

Premises used: MeasureTheory.measure_biUnion_finset_le, Set.Finite.toFinset, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h : Eq (α := β → Set α) (fun (i : β) ↦ ⋃ (_ : i ∈ s), f i) fun (i : β) ↦ ⋃ (_ : i ∈ hs.toFinset (s := s)), f i
convert_2 : LT.lt (α := ℝ≥0∞) (∑ i ∈ hs.toFinset (s := s), (μ : (a : Set α) → ℝ≥0∞) (f i)) ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, f i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
convert! (measure_biUnion_finset_le (μ := μ) hs.toFinset f).trans_lt _ using 3

Premises used: MeasureTheory.measure_biUnion_finset_le, Set.Finite.toFinset, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (x : β) (x_1 : α),
    Membership.mem (γ := Set α) (⋃ (_ : x ∈ s), f x) x_1 ↔
      Membership.mem (γ := Set α) (⋃ (_ : x ∈ hs.toFinset (s := s)), f x) x_1
⊢ Eq (α := β → Set α) (fun (i : β) ↦ ⋃ (_ : i ∈ s), f i) fun (i : β) ↦ ⋃ (_ : i ∈ hs.toFinset (s := s)), f i

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : β
x_1 : α
h h₁ : Membership.mem (γ := Set α) (⋃ (_ : x ∈ s), f x) x_1 ↔ Membership.mem (γ := Set α) (⋃ (_ : x ∈ s), f x) x_1
⊢ Membership.mem (γ := Set α) (⋃ (_ : x ∈ s), f x) x_1 ↔
    Membership.mem (γ := Set α) (⋃ (_ : x ∈ hs.toFinset (s := s)), f x) x_1

Tactic:
rw [Finite.mem_toFinset]

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (∑ i ∈ hs.toFinset (s := s), (μ : (a : Set α) → ℝ≥0∞) (f i)) ∞

Tactic:
simpa only [ENNReal.sum_lt_top, Finite.mem_toFinset]

Premises used: Set.Finite.mem_toFinset, ENNReal.sum_lt_top
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, f i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_biUnion_lt_top hs (fun i hi ↦ Ne.lt_top (hfin i hi ·))).ne

Premises used: MeasureTheory.measure_biUnion_lt_top, Ne.lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_union_le s t).trans_lt (ENNReal.add_lt_top.mpr ⟨hs, ht⟩)

Premises used: Iff.mpr, And.intro, ENNReal.add_lt_top, LE.le.trans_lt, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨fun h => ⟨?_, ?_⟩, fun h => measure_union_lt_top h.1 h.2⟩

Premises used: MeasureTheory.measure_union_lt_top, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
refine_1 :
  ∀ (h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  ∀ (h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => measure_union_lt_top h.1 h.2⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono Set.subset_union_left).trans_lt h

Premises used: Set.subset_union_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact (measure_mono Set.subset_union_left).trans_lt h

Premises used: Set.subset_union_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono Set.subset_union_right).trans_lt h

Premises used: Set.subset_union_right, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact (measure_mono Set.subset_union_right).trans_lt h

Premises used: Set.subset_union_right, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
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:
(measure_union_lt_top hs.lt_top ht.lt_top).ne

Premises used: MeasureTheory.measure_union_lt_top, Ne.lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
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:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    ¬(Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
simp only [← lt_top_iff_ne_top, ← Ne.eq_def, not_or, measure_union_lt_top_iff]

Premises used: MeasureTheory.measure_union_lt_top_iff, Ne.eq_def, lt_top_iff_ne_top, not_or
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
ι : Sort u_5
inst : MeasurableSpace α
μ : Measure α
inst_1 : Countable ι
s : ι → Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞) (0 : ℝ≥0∞)
contrapose! :
  ∀ (hs : ∀ (n : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (n : ι), LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)

Tactic:
contrapose! hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
ι : Sort u_5
inst : MeasurableSpace α
μ : Measure α
inst_1 : Countable ι
s : ι → Set α
hs : ∀ (n : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_iUnion_null fun n => nonpos_iff_eq_zero.1 (hs n)

Premises used: MeasureTheory.measure_iUnion_null, Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
ι : Sort u_5
inst : MeasurableSpace α
μ : Measure α
inst_1 : Countable ι
s : ι → Set α
hs : ∀ (n : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_iUnion_null fun n => nonpos_iff_eq_zero.1 (hs n)

Premises used: MeasureTheory.measure_iUnion_null, Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
hst : t ⊆ s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
lt_of_le_of_lt (μ.mono hst) hs.lt_top

Premises used: lt_of_le_of_lt, MeasureTheory.OuterMeasure.mono, MeasureTheory.Measure.toOuterMeasure, Ne.lt_top
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
h : t ⊆ s
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_lt_top_of_subset h ht).ne

Premises used: MeasureTheory.measure_lt_top_of_subset, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
hs_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top_of_subset inter_subset_left hs_finite

Premises used: Set.inter_subset_left, MeasureTheory.measure_ne_top_of_subset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
hs_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
ht_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top_of_subset inter_subset_right ht_finite

Premises used: MeasureTheory.measure_ne_top_of_subset, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
ht_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
S T : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S ∩ T) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null inter_subset_right h

Premises used: MeasureTheory.measure_mono_null, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
S T : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S ∩ T) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null inter_subset_left h

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ (i : ℕ), f i)
x : β
hx_empty : C x ∅
hx_basic : ∀ t ∈ s, C x t
hx_compl : ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
hx_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ (i : ℕ), f i)
⊢ ∀ ⦃t : Set α⦄, MeasurableSet t → C x t

Tactic:
MeasurableSpace.induction_on_inter (C := fun t _ ↦ C x t)
      h_eq h_inter hx_empty hx_basic hx_compl hx_union

Premises used: MeasurableSpace.induction_on_inter
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ (i : ℕ), f i)
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ C x ∅) x} x →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ ∀ t ∈ s, C x t) x} x →
                Membership.mem (γ := Set β)
                  {x : β |
                    Membership.mem (γ := Set β)
                        {x : β | (fun (x : β) ↦ ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ) x} x →
                      Membership.mem (γ := Set β)
                        {x : β |
                          Membership.mem (γ := Set β)
                              {x : β |
                                (fun (x : β) ↦
                                    ∀ (f : ℕ → Set α),
                                      Pairwise (Disjoint on f) →
                                        (∀ (i : ℕ), MeasurableSet (f i)) →
                                          (∀ (i : ℕ), C x (f i)) → C x (⋃ (i : ℕ), f i))
                                  x}
                              x →
                            Membership.mem (γ := Set β)
                              {x : β | (fun (x : β) ↦ ∀ ⦃t : Set α⦄, MeasurableSet t → C x t) x} x}
                        x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (x : β) (hx_empty : C x ∅) (hx_basic : ∀ t ∈ s, C x t) (hx_compl : ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ)
    (hx_union :
      ∀ (f : ℕ → Set α),
        Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ (i : ℕ), f i))
    ⦃t : Set α⦄, MeasurableSet t → C x t
⊢ ∀ᵐ (x : β) ∂μ, ∀ ⦃t : Set α⦄, MeasurableSet t → C x t

Tactic:
filter_upwards [h_empty, h_basic, h_compl, h_union] with x hx_empty hx_basic hx_compl hx_union
    using MeasurableSpace.induction_on_inter (C := fun t _ ↦ C x t)
      h_eq h_inter hx_empty hx_basic hx_compl hx_union
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
rw :
  s ⊆
    if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
      h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
    else
      if h' :
          ∃ t ⊇ s,
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
        h'.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
      else
        ⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
⊢ s ⊆ toMeasurable μ s

Tactic:
rw [toMeasurable_def]

Premises used: MeasureTheory.toMeasurable_def
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
pos :
  ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
    s ⊆ hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
pos₁ :
  ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
    (h's :
      ∃ t ⊇ s,
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
    s ⊆
      h's.choose (p := fun (t : Set α) ↦
        t ⊇ s ∧
          MeasurableSet t ∧
            ∀ (u : Set α),
              MeasurableSet u →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
neg :
  ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
    (h's :
      ¬∃ t ⊇ s,
          MeasurableSet t ∧
            ∀ (u : Set α),
              MeasurableSet u →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
    s ⊆
      ⋯.choose (p := fun (t : Set α) ↦
        s ⊆ t ∧
          MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
⊢ s ⊆
    if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
      h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
    else
      if h' :
          ∃ t ⊇ s,
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
        h'.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
      else
        ⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))

Tactic:
split_ifs with hs h's
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ s ⊆ hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)

Tactic:
hs.choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's :
  ∃ t ⊇ s,
    MeasurableSet t ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)
⊢ s ⊆
    h's.choose (p := fun (t : Set α) ↦
      t ⊇ s ∧
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))

Tactic:
h's.choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's :
  ¬∃ t ⊇ s,
      MeasurableSet t ∧
        ∀ (u : Set α),
          MeasurableSet u →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)
⊢ s ⊆
    ⋯.choose (p := fun (t : Set α) ↦
      s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))

Tactic:
(exists_measurable_superset μ s).choose_spec.1

Premises used: Exists.choose_spec, And.left, MeasureTheory.exists_measurable_superset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ s ⊆ hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)

Tactic:
exacts [hs.choose_spec.1, h's.choose_spec.1, (exists_measurable_superset μ s).choose_spec.1]

Premises used: Exists.choose_spec, And.left, MeasureTheory.exists_measurable_superset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ≤ᶠ[ae μ] toMeasurable μ s

Tactic:
HasSubset.Subset.eventuallyLE (subset_toMeasurable _ _)

Premises used: HasSubset.Subset.eventuallyLE, MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
rw :
  MeasurableSet.{u_1} (α := α)
    (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
      h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
    else
      if h' :
          ∃ t ⊇ s,
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
        h'.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
      else
        ⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ MeasurableSet (toMeasurable μ s)

Tactic:
rw [toMeasurable_def]

Premises used: MeasureTheory.toMeasurable_def