awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p_1 : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p_1 x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
x : ℝ
hx : x ∈ s
h'x : Membership.mem (γ := Set ℝ) (⋃ i ∈ A, T i) x
p : (↑s : Type) × (↑s : Type)
pA : p ∈ A
xp : x ∈ T p
⊢ Membership.mem (γ := Set ℝ) (⋃ p ∈ A, s ∩ T p) x

Tactic:
exact mem_biUnion pA ⟨hx, xp⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
x : ℝ
hx : x ∈ s
h'x : x ∉ ⋃ (i : (↑s : Type) × (↑s : Type)), T i
⊢ x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p

Tactic:
Or.inl ⟨hx, h'x⟩

Premises used: Set.union, Set.Mem, setOf, And.intro, Or.inl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
x : ℝ
hx : x ∈ s
h'x : x ∉ ⋃ (i : (↑s : Type) × (↑s : Type)), T i
⊢ x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p

Tactic:
exact Or.inl ⟨hx, h'x⟩

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
⊢ s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p

Tactic:
have : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p := by
    intro x hx
    by_cases h'x : x ∈ ⋃ i : ↥s × ↥s, T i
    · rw [← hA] at h'x
      obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
        simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using h'x
      right
      exact mem_biUnion pA ⟨hx, xp⟩
    · exact Or.inl ⟨hx, h'x⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
apply : ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u ∪ ⋃ p ∈ A, s ∩ T p), p x
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict s, p x

Tactic:
apply ae_restrict_of_ae_restrict_of_subset this

Premises used: MeasureTheory.ae_restrict_of_ae_restrict_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
rw : (∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x) ∧ ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u ∪ ⋃ p ∈ A, s ∩ T p), p x

Tactic:
rw [ae_restrict_union_iff, ae_restrict_biUnion_iff _ A_count]

Premises used: MeasureTheory.ae_restrict_biUnion_iff, MeasureTheory.ae_restrict_union_iff
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
left : ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x
right : ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x
⊢ (∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x) ∧ ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ μ.restrict (s \ u) = 0

Tactic:
simp only [restrict_eq_zero, hfinite.measure_zero]

Premises used: MeasureTheory.Measure.restrict_eq_zero, Set.Finite.measure_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ μ.restrict (s \ u) = 0

Tactic:
have : μ.restrict (s \ u) = 0 := by simp only [restrict_eq_zero, hfinite.measure_zero]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this_1 : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
this : μ.restrict (s \ u) = 0
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x

Tactic:
simp only [this, ae_zero, eventually_bot]

Premises used: MeasureTheory.ae_zero, Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
right : ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
⊢ ∀ᵐ (x :
    ℝ) ∂μ.restrict (s ∩ T (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ s) a as, Subtype.mk (p := fun (x : ℝ) ↦ x ∈ s) b bs)), p x

Tactic:
dsimp [T]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
right : ∀ (hba : b ≤ a), ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
right₁ : ∀ (hab : a < b), ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x

Tactic:
rcases le_or_gt b a with (hba | hab)

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hba : b ≤ a
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x

Tactic:
simp only [Ioo_eq_empty_of_le hba, inter_empty, restrict_empty, ae_zero, eventually_bot]

Premises used: MeasureTheory.Measure.restrict_empty, Set.Ioo_eq_empty_of_le, MeasureTheory.ae_zero, Set.inter_empty, Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hab : a < b
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x

Tactic:
h a b as bs hab
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hab : a < b
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x

Tactic:
exact h a b as bs hab
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
⊢ (s \ u).Finite

Tactic:
have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
⊢ ∃ (A : Set ((↑s : Type) × (↑s : Type))),
    A.Countable ∧ Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)

Tactic:
isOpen_iUnion_countable _ fun p => isOpen_Ioo

Premises used: TopologicalSpace.isOpen_iUnion_countable, isOpen_Ioo
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
obtain :
  ∀ (A : Set ((↑s : Type) × (↑s : Type))) (A_count : A.Countable)
    (hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)), ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x

Tactic:
obtain ⟨A, A_count, hA⟩ :
    ∃ A : Set (↥s × ↥s), A.Countable ∧ ⋃ i ∈ A, T i = ⋃ i : ↥s × ↥s, T i :=
    isOpen_iUnion_countable _ fun p => isOpen_Ioo

Premises used: TopologicalSpace.isOpen_iUnion_countable, isOpen_Ioo, Set.Elem, Prod, Set
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u

Tactic:
have M : ∀ᵐ x ∂μ, x ∉ s \ u := hfinite.countable.ae_notMem _
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
rw : ∀ (i : (↑s : Type) × (↑s : Type)) (hi : i ∈ A), ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ T i → p x
⊢ ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x

Tactic:
rw [ae_ball_iff A_count]

Premises used: MeasureTheory.ae_ball_iff
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
change : ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
⊢ ∀ᵐ (x : ℝ) ∂μ,
    x ∈ s ∩ T (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ s) a as, Subtype.mk (p := fun (x : ℝ) ↦ x ∈ s) b bs) → p x

Tactic:
change ∀ᵐ x : ℝ ∂μ, x ∈ s ∩ Ioo a b → p x
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
inl : ∀ (hba : b ≤ a), ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
inr : ∀ (hab : a < b), ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x

Tactic:
rcases le_or_gt b a with (hba | hab)

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hba : b ≤ a
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x

Tactic:
simp only [Ioo_eq_empty_of_le hba, inter_empty, IsEmpty.forall_iff, eventually_true,
        mem_empty_iff_false]

Premises used: Set.Ioo_eq_empty_of_le, Filter.eventually_true, Set.mem_empty_iff_false, Set.inter_empty, IsEmpty.forall_iff
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hab : a < b
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x

Tactic:
h a b as bs hab
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hab : a < b
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x

Tactic:
exact h a b as bs hab
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
⊢ ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x

Tactic:
have M' : ∀ᵐ x ∂μ, ∀ (i : ↥s × ↥s), i ∈ A → x ∈ s ∩ T i → p x := by
    rw [ae_ball_iff A_count]
    rintro ⟨⟨a, as⟩, ⟨b, bs⟩⟩ -
    change ∀ᵐ x : ℝ ∂μ, x ∈ s ∩ Ioo a b → p x
    rcases le_or_gt b a with (hba | hab)
    · simp only [Ioo_eq_empty_of_le hba, inter_empty, IsEmpty.forall_iff, eventually_true,
        mem_empty_iff_false]
    · exact h a b as bs hab
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
h₁ : ∀ (x : ℝ) (hx : x ∉ s \ u) (h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x), x ∈ s → p x
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x

Tactic:
filter_upwards [M, M'] with x hx h'x
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
pos : ∀ (Hx : Membership.mem (γ := Set ℝ) (⋃ (i : (↑s : Type) × (↑s : Type)), T i) x), p x
neg : ∀ (Hx : x ∉ ⋃ (i : (↑s : Type) × (↑s : Type)), T i), p x
⊢ p x

Tactic:
by_cases Hx : x ∈ ⋃ i : ↥s × ↥s, T i
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
Hx : Membership.mem (γ := Set ℝ) (⋃ (i : (↑s : Type) × (↑s : Type)), T i) x
⊢ Membership.mem (γ := Set ℝ) (⋃ i ∈ A, T i) x

Tactic:
rw [← hA] at Hx
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
Hx : Membership.mem (γ := Set ℝ) (⋃ i ∈ A, T i) x
⊢ ∃ p ∈ A, x ∈ T p

Tactic:
simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using Hx

Premises used: Set.mem_iUnion, SetCoe.exists, exists_and_right, exists_prop
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
Hx : Membership.mem (γ := Set ℝ) (⋃ i ∈ A, T i) x
pos : ∀ (p_1 : (↑s : Type) × (↑s : Type)) (pA : p_1 ∈ A) (xp : x ∈ T p_1), p x
⊢ p x

Tactic:
obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
      simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using Hx
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p_1 : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p_1 x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p_1 x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p_1 x
xs : x ∈ s
Hx : Membership.mem (γ := Set ℝ) (⋃ i ∈ A, T i) x
p : (↑s : Type) × (↑s : Type)
pA : p ∈ A
xp : x ∈ T p
⊢ p_1 x

Tactic:
apply h'x p pA ⟨xs, xp⟩

Premises used: And.intro