awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
f g : α → β
h : f =ᶠ[ae μ] g
⊢ g =ᶠ[ae μ] f

Tactic:
h.symm

Premises used: Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
f g h : α → β
h₁ : f =ᶠ[ae μ] g
h₂ : g =ᶠ[ae μ] h
⊢ f =ᶠ[ae μ] h

Tactic:
h₁.trans h₂

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
f g : α → β
⊢ f =ᶠ[ae μ] g ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≠ g x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s : Set α
f g : α → β
h : EqOn f g s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f =ᶠ[ae μ] g

Tactic:
eventuallyEq_of_mem h2 h

Premises used: Filter.eventuallyEq_of_mem
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
simp :
  (∀ (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = univ) ↔
    ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ae μ = ⊤ ↔ ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [Filter.ext_iff, mem_ae_iff, mem_top, ne_eq]

Premises used: ne_eq, Filter.ext_iff, MeasureTheory.mem_ae_iff, Filter.mem_top
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
h : ∀ (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = univ
a : α
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
simpa [ha] using (h {a}ᶜ).1

Premises used: Compl.compl, Iff.mp, Singleton.singleton
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
refine_1 :
  ∀ (h : ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)) (s : Set α)
    (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)), s = univ
refine_2 :
  ∀ (h : ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)) (s : Set α),
    s = univ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∀ (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = univ) ↔
    ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine ⟨fun h a ha ↦ by simpa [ha] using (h {a}ᶜ).1, fun h s ↦ ⟨fun hs ↦ ?_, ?_⟩⟩
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : ¬sᶜ.Nonempty
⊢ s = univ

Tactic:
rw [← compl_empty_iff, ← not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty, Set.compl_empty_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
a : α
ha : a ∈ sᶜ
⊢ False

Tactic:
h _ <| measure_mono_null (singleton_subset_iff.2 ha) hs

Premises used: Iff.mpr, Set.singleton_subset_iff, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
a : α
ha : a ∈ sᶜ
⊢ False

Tactic:
exact h _ <| measure_mono_null (singleton_subset_iff.2 ha) hs

Premises used: Iff.mpr, Set.singleton_subset_iff, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
β : Type u_4
inst_2 : Preorder β
f g : α → β
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ f ≤ᶠ[ae μ] g

Tactic:
h.mono fun _ ↦ le_of_lt

Premises used: le_of_lt, Filter.Eventually.mono, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s : Set α
⊢ (∀ᵐ (x : α) ∂μ, x ∉ s) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [ae_iff, Classical.not_not, setOf_mem_eq]

Premises used: Classical.not_not, Set.setOf_mem_eq, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s : Set α
⊢ s =ᶠ[ae μ] univ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
eventuallyEq_univ

Premises used: Set.Mem, setOf, Filter.eventuallyEq_univ
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
simp :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | a ∈ s ∧ a ∉ t} : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → x ∈ t) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [ae_iff]

Premises used: MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | a ∈ s ∧ a ∉ t} : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t s' t' : Set α
h : s ≤ᶠ[ae μ] t
h' : s' ≤ᶠ[ae μ] t'
⊢ s ∩ s' ≤ᶠ[ae μ] t ∩ t'

Tactic:
h.inter h'

Premises used: Filter.EventuallyLE.inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t s' t' : Set α
h : s ≤ᶠ[ae μ] t
h' : s' ≤ᶠ[ae μ] t'
⊢ s ∪ s' ≤ᶠ[ae μ] t ∪ t'

Tactic:
h.union h'

Premises used: Filter.EventuallyLE.union
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
⊢ s ∪ t =ᶠ[ae μ] t ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [eventuallyLE_antisymm_iff, ae_le_set, union_diff_right,
    diff_eq_empty.2 Set.subset_union_right]

Premises used: Iff.mpr, Set.subset_union_right, Filter.eventuallyLE_antisymm_iff, Set.union_diff_right, Set.diff_eq_empty, MeasureTheory.ae_le_set
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
⊢ s \ t =ᶠ[ae μ] s ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [eventuallyLE_antisymm_iff, ae_le_set]

Premises used: Filter.eventuallyLE_antisymm_iff, MeasureTheory.ae_le_set
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s \ t =ᶠ[ae μ] s

Tactic:
diff_ae_eq_self.mpr (measure_mono_null inter_subset_right ht)

Premises used: Iff.mpr, MeasureTheory.measure_mono_null, MeasureTheory.diff_ae_eq_self, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
⊢ s =ᶠ[ae μ] t ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [eventuallyLE_antisymm_iff, ae_le_set]

Premises used: Filter.eventuallyLE_antisymm_iff, MeasureTheory.ae_le_set
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s =ᶠ[ae μ] t

Tactic:
simp [ae_eq_set, symmDiff_def]

Premises used: symmDiff_def, MeasureTheory.ae_eq_set
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
⊢ sᶜ =ᶠ[ae μ] tᶜ ↔ s =ᶠ[ae μ] t

Tactic:
simp only [← measure_symmDiff_eq_zero_iff, compl_symmDiff_compl]

Premises used: compl_symmDiff_compl, MeasureTheory.measure_symmDiff_eq_zero_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
rw : sᶜᶜ =ᶠ[ae μ] tᶜ ↔ s =ᶠ[ae μ] tᶜ
rw₁ rw₂ : s =ᶠ[ae μ] tᶜ ↔ s =ᶠ[ae μ] tᶜ
⊢ sᶜ =ᶠ[ae μ] t ↔ s =ᶠ[ae μ] tᶜ

Tactic:
rw [← ae_eq_set_compl_compl, compl_compl]

Premises used: compl_compl, MeasureTheory.ae_eq_set_compl_compl
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t s' t' : Set α
h : s =ᶠ[ae μ] t
h' : s' =ᶠ[ae μ] t'
⊢ s ∩ s' =ᶠ[ae μ] t ∩ t'

Tactic:
h.inter h'

Premises used: Filter.EventuallyEq.inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t s' t' : Set α
h : s =ᶠ[ae μ] t
h' : s' =ᶠ[ae μ] t'
⊢ s ∪ s' =ᶠ[ae μ] t ∪ t'

Tactic:
h.union h'

Premises used: Filter.EventuallyEq.union
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t s' t' : Set α
h : s =ᶠ[ae μ] t
h' : s' =ᶠ[ae μ] t'
⊢ s \ s' =ᶠ[ae μ] t \ t'

Tactic:
h.diff h'

Premises used: Set.Mem, Set.diff, setOf, Filter.EventuallyEq.diff
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t s' t' : Set α
h : s =ᶠ[ae μ] t
h' : s' =ᶠ[ae μ] t'
⊢ s ∆ s' =ᶠ[ae μ] t ∆ t'

Tactic:
h.symmDiff h'

Premises used: Set.union, Set.Mem, Set.diff, setOf, Filter.EventuallyEq.symmDiff, Set
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] univ
rw rw₁ : univ =ᶠ[ae μ] univ
⊢ univ ∪ t =ᶠ[ae μ] univ

Tactic:
rw [univ_union]

Premises used: Set.univ_union
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ s ∪ t =ᶠ[ae μ] s ∪ univ

Tactic:
ae_eq_set_union (ae_eq_refl s) h

Premises used: MeasureTheory.ae_eq_set_union, MeasureTheory.ae_eq_refl
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
h₁ : univ = s ∪ univ
⊢ s ∪ t =ᶠ[ae μ] univ

Tactic:
convert! ae_eq_set_union (ae_eq_refl s) h

Premises used: MeasureTheory.ae_eq_set_union, MeasureTheory.ae_eq_refl
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
h₁ h₂ : Eq.{u_1 + 1} (α := α → Prop) univ univ
⊢ univ = s ∪ univ

Tactic:
rw [union_univ]

Premises used: Set.union_univ
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ s ∪ t =ᶠ[ae μ] ∅ ∪ t

Tactic:
ae_eq_set_union h (ae_eq_refl t)

Premises used: MeasureTheory.ae_eq_set_union, MeasureTheory.ae_eq_refl
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
h₁ : t = ∅ ∪ t
⊢ s ∪ t =ᶠ[ae μ] t

Tactic:
convert! ae_eq_set_union h (ae_eq_refl t)

Premises used: MeasureTheory.ae_eq_set_union, MeasureTheory.ae_eq_refl
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
h₁ h₂ : t = t
⊢ t = ∅ ∪ t

Tactic:
rw [empty_union]

Premises used: Set.empty_union
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
⊢ s ∪ t =ᶠ[ae μ] s ∪ ∅

Tactic:
ae_eq_set_union (ae_eq_refl s) h

Premises used: MeasureTheory.ae_eq_set_union, MeasureTheory.ae_eq_refl
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
h₁ : s = s ∪ ∅
⊢ s ∪ t =ᶠ[ae μ] s

Tactic:
convert! ae_eq_set_union (ae_eq_refl s) h

Premises used: MeasureTheory.ae_eq_set_union, MeasureTheory.ae_eq_refl
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
h₁ h₂ : s = s
⊢ s = s ∪ ∅

Tactic:
rw [union_empty]

Premises used: Set.union_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] univ
⊢ s ∩ t =ᶠ[ae μ] univ ∩ t

Tactic:
ae_eq_set_inter h (ae_eq_refl t)

Premises used: MeasureTheory.ae_eq_refl, MeasureTheory.ae_eq_set_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] univ
h₁ : t = univ ∩ t
⊢ s ∩ t =ᶠ[ae μ] t

Tactic:
convert! ae_eq_set_inter h (ae_eq_refl t)

Premises used: MeasureTheory.ae_eq_refl, MeasureTheory.ae_eq_set_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] univ
h₁ h₂ : t = t
⊢ t = univ ∩ t

Tactic:
rw [univ_inter]

Premises used: Set.univ_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ s ∩ t =ᶠ[ae μ] s ∩ univ

Tactic:
ae_eq_set_inter (ae_eq_refl s) h

Premises used: MeasureTheory.ae_eq_refl, MeasureTheory.ae_eq_set_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
h₁ : s = s ∩ univ
⊢ s ∩ t =ᶠ[ae μ] s

Tactic:
convert! ae_eq_set_inter (ae_eq_refl s) h

Premises used: MeasureTheory.ae_eq_refl, MeasureTheory.ae_eq_set_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
h₁ h₂ : s = s
⊢ s = s ∩ univ

Tactic:
rw [inter_univ]

Premises used: Set.inter_univ
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ s ∩ t =ᶠ[ae μ] ∅ ∩ t

Tactic:
ae_eq_set_inter h (ae_eq_refl t)

Premises used: MeasureTheory.ae_eq_refl, MeasureTheory.ae_eq_set_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
h₁ : ∅ = ∅ ∩ t
⊢ s ∩ t =ᶠ[ae μ] ∅

Tactic:
convert! ae_eq_set_inter h (ae_eq_refl t)

Premises used: MeasureTheory.ae_eq_refl, MeasureTheory.ae_eq_set_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
h₁ h₂ : Eq.{u_1 + 1} (α := α → Prop) ∅ ∅
⊢ ∅ = ∅ ∩ t

Tactic:
rw [empty_inter]

Premises used: Set.empty_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
⊢ s ∩ t =ᶠ[ae μ] s ∩ ∅

Tactic:
ae_eq_set_inter (ae_eq_refl s) h

Premises used: MeasureTheory.ae_eq_refl, MeasureTheory.ae_eq_set_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
h₁ : ∅ = s ∩ ∅
⊢ s ∩ t =ᶠ[ae μ] ∅

Tactic:
convert! ae_eq_set_inter (ae_eq_refl s) h

Premises used: MeasureTheory.ae_eq_refl, MeasureTheory.ae_eq_set_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
h₁ h₂ : Eq.{u_1 + 1} (α := α → Prop) ∅ ∅
⊢ ∅ = s ∩ ∅

Tactic:
rw [inter_empty]

Premises used: Set.inter_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s : Set β
hs : s.Countable
t t' : β → Set α
h : ∀ b ∈ s, t b =ᶠ[ae μ] t' b
⊢ ⋂ b ∈ s, t b =ᶠ[ae μ] ⋂ b ∈ s, t' b

Tactic:
.countable_bInter hs h

Premises used: Filter.EventuallyEq.countable_bInter
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s : Set β
hs : s.Countable
t t' : β → Set α
h : ∀ b ∈ s, t b =ᶠ[ae μ] t' b
⊢ ⋃ b ∈ s, t b =ᶠ[ae μ] ⋃ b ∈ s, t' b

Tactic:
.countable_bUnion hs h

Premises used: Filter.EventuallyEq.countable_bUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
M : Type u_4
inst_2 : One M
f : α → M
s : Set α
simp :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | a ∈ s ∧ ¬f a = 1} : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ Function.mulSupport f) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.mulIndicator f =ᶠ[ae μ] 1 ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ Function.mulSupport f) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [EventuallyEq, eventually_iff, ae, compl_setOf]

Premises used: MeasureTheory.ae, Filter.eventually_iff, Filter.EventuallyEq, Set.compl_setOf
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
M : Type u_4
inst_2 : One M
f : α → M
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | a ∈ s ∧ ¬f a = 1} : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ Function.mulSupport f) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
H : s ≤ᶠ[ae μ] t
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s \ t) : ℝ≥0∞)

Tactic:
rw [union_diff_self, Set.union_comm]

Premises used: Set.union_comm, Set.union_diff_self
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
H : s ≤ᶠ[ae μ] t
rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) t
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) t

Tactic:
rw [ae_le_set.1 H, add_zero]

Premises used: Iff.mp, add_zero, MeasureTheory.ae_le_set
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
H : s =ᶠ[ae μ] t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
le_antisymm H.le.measure_le H.symm.le.measure_le

Premises used: Filter.EventuallyEq.le, le_antisymm, Filter.EventuallyLE.measure_le, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.OuterMeasure.AE
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
H : s ≤ᶠ[ae μ] t
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
nonpos_iff_eq_zero.1 <| ht ▸ H.measure_le

Premises used: Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅) 0

Tactic:
OuterMeasureClass.measure_empty μ

Premises used: MeasureTheory.OuterMeasureClass.measure_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
OuterMeasureClass.measure_mono μ h

Premises used: MeasureTheory.OuterMeasureClass.measure_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s ⊆ t
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
eq_bot_mono (measure_mono h) ht

Premises used: MeasureTheory.measure_mono, eq_bot_mono