awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable β
μ : Measure (α × β)
x : α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    ((μ : (a : Set (α × β)) → ℝ≥0∞) (⋃ (i : β), {(x, i)}) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    ((μ : (a : Set (α × β)) → ℝ≥0∞) (range (Prod.mk x)) : ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (range fun (x_1 : β) ↦ (x, x_1)) : ℝ≥0∞)
    ((μ : (a : Set (α × β)) → ℝ≥0∞) (range (Prod.mk x)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    (∑' (y : β), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)

Tactic:
rw [← measure_iUnion (by simp [Pairwise]) fun _ ↦ .singleton _, iUnion_singleton_eq_range,
    preimage_fst_singleton_eq_range]

Premises used: Set.preimage_fst_singleton_eq_range, MeasurableSet.singleton, Set.iUnion_singleton_eq_range, MeasureTheory.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable α
μ : Measure (α × β)
y : β
h :
  ∀ (y_1 : α × β),
    Membership.mem (γ := Set (α × β)) (Prod.snd ⁻¹' {y}) y_1 ↔
      Membership.mem (γ := Set (α × β)) (⋃ (x : α), {(x, y)}) y_1
⊢ Eq (α := Set (α × β)) (Prod.snd ⁻¹' {y}) (⋃ (x : α), {(x, y)})

Tactic:
ext y
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable α
μ : Measure (α × β)
y_1 : β
y : α × β
⊢ Membership.mem (γ := Set (α × β)) (Prod.snd ⁻¹' {y_1}) y ↔ Membership.mem (γ := Set (α × β)) (⋃ (x : α), {(x, y_1)}) y

Tactic:
simp [Prod.ext_iff, eq_comm]

Premises used: Prod.ext_iff, eq_comm
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable α
μ : Measure (α × β)
y : β
⊢ Eq (α := Set (α × β)) (Prod.snd ⁻¹' {y}) (⋃ (x : α), {(x, y)})

Tactic:
have : Prod.snd ⁻¹' {y} = ⋃ x : α, {(x, y)} := by ext y; simp [Prod.ext_iff, eq_comm]
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable α
μ : Measure (α × β)
y : β
this : Eq (α := Set (α × β)) (Prod.snd ⁻¹' {y}) (⋃ (x : α), {(x, y)})
hn : Pairwise.{u_2} (α := α) (Function.onFun (β := Set (α × β)) Disjoint fun (x : α) ↦ {(x, y)})
h : ∀ (i : α), MeasurableSet (α := α × β) {(i, y)}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' {y}) : ℝ≥0∞)
    (∑' (x : α), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)

Tactic:
rw [this, measure_iUnion]

Premises used: MeasureTheory.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable α
μ : Measure (α × β)
y : β
this : Eq (α := Set (α × β)) (Prod.snd ⁻¹' {y}) (⋃ (x : α), {(x, y)})
⊢ Pairwise.{u_2} (α := α) (Function.onFun (β := Set (α × β)) Disjoint fun (x : α) ↦ {(x, y)})

Tactic:
simp [Pairwise]

Premises used: Pairwise
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable α
μ : Measure (α × β)
y : β
this : Eq (α := Set (α × β)) (Prod.snd ⁻¹' {y}) (⋃ (x : α), {(x, y)})
⊢ ∀ (i : α), MeasurableSet (α := α × β) {(i, y)}

Tactic:
simp [Pairwise]

Premises used: Pairwise
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Fintype β
μ : Measure (α × β)
x : α
rw :
  Eq (α := ℝ≥0∞) (∑' (y : β), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
    (∑ y : β, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∑ b : β, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, b)}) (∑ y : β, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    (∑ y : β, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)

Tactic:
rw [measure_preimage_fst_singleton_eq_tsum μ x, tsum_fintype]

Premises used: MeasureTheory.measure_preimage_fst_singleton_eq_tsum, tsum_fintype
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Fintype α
μ : Measure (α × β)
y : β
rw :
  Eq (α := ℝ≥0∞) (∑' (x : α), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
    (∑ x : α, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∑ b : α, (μ : (a : Set (α × β)) → ℝ≥0∞) {(b, y)}) (∑ x : α, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' {y}) : ℝ≥0∞)
    (∑ x : α, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)

Tactic:
rw [measure_preimage_snd_singleton_eq_tsum μ y, tsum_fintype]

Premises used: tsum_fintype, MeasureTheory.measure_preimage_snd_singleton_eq_tsum
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
μ : Measure α
h : Measurable f
⊢ NullMeasurable f μ

Tactic:
h.eventuallyMeasurable

Premises used: Measurable, MeasureTheory.NullMeasurableSet, EventuallyMeasurable, MeasureTheory.NullMeasurableSpace, MeasureTheory.NullMeasurable, Measurable.eventuallyMeasurable
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
μ : Measure α
h : NullMeasurable f μ
⊢ Measurable f

Tactic:
h

Premises used: Measurable, MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace, MeasureTheory.NullMeasurable
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hg : Measurable g
hf : NullMeasurable f μ
⊢ NullMeasurable (g ∘ f) μ

Tactic:
hg.comp_eventuallyMeasurable hf

Premises used: Measurable, MeasureTheory.NullMeasurableSet, Measurable.comp_eventuallyMeasurable, EventuallyMeasurable, MeasureTheory.NullMeasurableSpace, MeasureTheory.NullMeasurable
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
μ : Measure α
g : α → β
hf : NullMeasurable f μ
hg : f =ᶠ[ae μ] g
⊢ NullMeasurable g μ

Tactic:
EventuallyMeasurable.congr hf hg.symm

Premises used: Measurable, MeasureTheory.NullMeasurableSet, EventuallyMeasurable.congr, EventuallyMeasurable, MeasureTheory.NullMeasurableSpace, MeasureTheory.NullMeasurable, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.IsComplete ↔ ∀ (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → MeasurableSet s

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: MeasureTheory.Measure.IsComplete.mk, Iff.intro, MeasureTheory.Measure.IsComplete.out'
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
h : μ.IsComplete
⊢ ∀ (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → MeasurableSet s

Tactic:
h.1

Premises used: MeasureTheory.Measure.IsComplete.out'
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : μ.IsComplete
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ MeasurableSet s

Tactic:
MeasureTheory.Measure.IsComplete.out' s hs

Premises used: MeasureTheory.Measure.IsComplete.out'
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
inst : μ.IsComplete
⊢ MeasurableSet s

Tactic:
diff_diff_cancel_left (subset_toMeasurable μ s) ▸
    (measurableSet_toMeasurable _ _).diff
      (measurableSet_of_null (ae_le_set.1 <|
        EventuallyEq.le (NullMeasurableSet.toMeasurable_ae_eq hs)))

Premises used: MeasurableSet.diff, Eq.rec, Filter.EventuallyEq.le, MeasureTheory.subset_toMeasurable, MeasureTheory.measurableSet_toMeasurable, Set.diff_diff_cancel_left, Iff.mp, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, MeasureTheory.measurableSet_of_null, MeasureTheory.ae_le_set
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst : μ.IsComplete
_m1 : MeasurableSpace β
f : α → β
hf : NullMeasurable f μ
⊢ Measurable f

Tactic:
fun _s hs => (hf hs).measurable_of_complete

Premises used: Measurable, MeasureTheory.NullMeasurableSet.measurable_of_complete
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
_hμ : μ.IsComplete
f g : α → β
hf : Measurable f
hfg : f =ᶠ[ae μ] g
⊢ Measurable g

Tactic:
NullMeasurable.measurable_of_complete (NullMeasurable.congr hf.nullMeasurable hfg)

Premises used: MeasureTheory.NullMeasurable.congr, Measurable.nullMeasurable, MeasureTheory.NullMeasurable.measurable_of_complete
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ_1 : Measure α
s t : Set α
x : MeasurableSpace α
μ : Measure α
nth_rewrite : μ.trim ≤ μ.trim
⊢ μ.trim ≤ μ.toOuterMeasure

Tactic:
nth_rewrite 2 [← μ.trimmed]

Premises used: MeasureTheory.Measure.trimmed
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ_1 : Measure α
s t : Set α
x : MeasurableSpace α
μ : Measure α
⊢ μ.trim ≤ μ.trim

Tactic:
OuterMeasure.trim_anti_measurableSpace _ fun _ ↦ MeasurableSet.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.OuterMeasure.trim_anti_measurableSpace, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ_1 : Measure α
s t : Set α
x : MeasurableSpace α
μ : Measure α
⊢ μ.trim ≤ μ.trim

Tactic:
exact OuterMeasure.trim_anti_measurableSpace _ fun _ ↦ MeasurableSet.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.OuterMeasure.trim_anti_measurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ_1 : Measure α
s t : Set α
_m : MeasurableSpace α
μ : Measure α
⊢ μ.completion.IsComplete

Tactic:
⟨fun _z hz => NullMeasurableSet.of_null hz⟩

Premises used: MeasureTheory.NullMeasurableSet.of_null, MeasureTheory.Measure.IsComplete.mk
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
x : MeasurableSpace α
μ : Measure α
⊢ Eq (α := (a : Set (NullMeasurableSpace α μ)) → ℝ≥0∞) (⇑μ.completion : (a : Set (NullMeasurableSpace α μ)) → ℝ≥0∞)
    (⇑μ : (a : Set α) → ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
x : MeasurableSpace α
μ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace α μ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
x : MeasurableSpace α
μ : Measure α
⊢ ae μ.completion = ae μ

Tactic:
rfl

Premises used: MeasureTheory.ae, MeasureTheory.Measure.completion, MeasureTheory.NullMeasurableSpace, rfl
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen[inst] U
hne : U.Nonempty
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
IsOpenPosMeasure.open_pos U hU hne

Premises used: MeasureTheory.Measure.IsOpenPosMeasure.open_pos
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen[inst] U
hne : U.Nonempty
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
(hU.measure_ne_zero μ hne).bot_lt

Premises used: IsOpen.measure_ne_zero, Ne.bot_lt
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ ν : Measure X
inst_3 : μ.IsOpenPosMeasure
s U F : Set X
x : X
inst_4 : Nonempty X
⊢ NeZero μ

Tactic:
⟨measure_univ_pos.mp <| isOpen_univ.measure_pos μ univ_nonempty⟩

Premises used: NeZero.mk, MeasureTheory.Measure.measure_univ_pos, Set.univ_nonempty, IsOpen.measure_pos, isOpen_univ, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen[inst] U
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) ↔ U.Nonempty

Tactic:
⟨fun h => nonempty_iff_ne_empty.2 fun he => h.ne' <| he.symm ▸ measure_empty, hU.measure_pos μ⟩

Premises used: Iff.mpr, IsOpen.measure_pos, Eq.rec, MeasureTheory.measure_empty, LT.lt.ne', Iff.intro, Set.nonempty_iff_ne_empty, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen[inst] U
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ U = ∅

Tactic:
simpa only [not_lt, nonpos_iff_eq_zero, not_nonempty_iff_eq_empty] using
    not_congr (hU.measure_pos_iff μ)

Premises used: Set.not_nonempty_iff_eq_empty, not_lt, not_congr, nonpos_iff_eq_zero, IsOpen.measure_pos_iff
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
s : Set X
h : (interior s).Nonempty
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(isOpen_interior.measure_pos μ h).trans_le (measure_mono interior_subset)

Premises used: interior_subset, isOpen_interior, IsOpen.measure_pos, LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
s : Set X
x : X
h : s ∈ 𝓝 x
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_pos_of_nonempty_interior _ ⟨x, mem_interior_iff_mem_nhds.2 h⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, MeasureTheory.Measure.measure_pos_of_nonempty_interior, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
c : ℝ≥0∞
h : c ≠ 0
⊢ (c • μ).IsOpenPosMeasure

Tactic:
⟨fun _U Uo Une => mul_ne_zero h (Uo.measure_ne_zero μ Une)⟩

Premises used: MeasureTheory.Measure.IsOpenPosMeasure.mk, mul_ne_zero, IsOpen.measure_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ ν : Measure X
inst_1 : μ.IsOpenPosMeasure
h : μ ≪ ν
⊢ ν.IsOpenPosMeasure

Tactic:
⟨fun _U ho hne h₀ => ho.measure_ne_zero μ hne (h h₀)⟩

Premises used: MeasureTheory.Measure.IsOpenPosMeasure.mk, IsOpen.measure_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ ν : Measure X
inst_1 : μ.IsOpenPosMeasure
h : μ ≤ ν
⊢ ν.IsOpenPosMeasure

Tactic:
h.absolutelyContinuous.isOpenPosMeasure

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.isOpenPosMeasure, LE.le.absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen[inst] U
h : U = ∅
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen[inst] U
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ U = ∅
rw₁ rw₂ : U = ∅ ↔ U = ∅
⊢ U =ᶠ[ae μ] ∅ ↔ U = ∅

Tactic:
rw [ae_eq_empty, hU.measure_zero_iff_eq_empty]

Premises used: IsOpen.measure_zero_iff_eq_empty, MeasureTheory.ae_eq_empty
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen[inst] U
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ U = ∅

Tactic:
(hU.measure_eq_zero_iff μ).mp h₀

Premises used: Iff.mp, IsOpen.measure_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst] F
h : F = univ
rw rw₁ : univ =ᶠ[ae μ] univ
⊢ F =ᶠ[ae μ] univ

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst] F
refine : ∀ (h : F =ᶠ[ae μ] univ), F = univ
⊢ F =ᶠ[ae μ] univ ↔ F = univ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst] F
h : F =ᶠ[ae μ] univ
rwa : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Fᶜ : ℝ≥0∞) (0 : ℝ≥0∞)), F = univ
rwa₁ : ∀ (h : Fᶜ = ∅), F = univ
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : F = univ), F = univ
⊢ F = univ

Tactic:
rwa [ae_eq_univ, hF.isOpen_compl.measure_eq_zero_iff μ, compl_empty_iff] at h

Premises used: IsClosed.isOpen_compl, Set.compl_empty_iff, MeasureTheory.ae_eq_univ, IsOpen.measure_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
inst_2 : OpensMeasurableSpace X
inst_3 : IsFiniteMeasure μ
hF : IsClosed[inst] F
rw : F =ᶠ[ae μ] univ ↔ F = univ
rw₁ rw₂ : F = univ ↔ F = univ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ↔ F = univ

Tactic:
rw [← ae_eq_univ_iff_measure_eq hF.measurableSet.nullMeasurableSet, hF.ae_eq_univ_iff_eq]

Premises used: MeasurableSet.nullMeasurableSet, IsClosed.measurableSet, MeasureTheory.ae_eq_univ_iff_measure_eq, IsClosed.ae_eq_univ_iff_eq
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
inst_2 : OpensMeasurableSpace X
inst_3 : IsProbabilityMeasure μ
hF : IsClosed[inst] F
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ↔ F = univ
rw₁ rw₂ : F = univ ↔ F = univ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) (1 : ℝ≥0∞) ↔ F = univ

Tactic:
rw [← measure_univ (μ := μ), hF.measure_eq_univ_iff_eq]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, IsClosed.measure_eq_univ_iff_eq
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
s : Set X
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ interior s = ∅

Tactic:
isOpen_interior.eq_empty_of_measure_zero <| measure_mono_null interior_subset hs

Premises used: interior_subset, isOpen_interior, IsOpen.eq_empty_of_measure_zero, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
p : X → Prop
hp : ∀ᵐ (x : X) ∂μ, p x
rw : Eq.{u_1 + 1} (α := Set X) (interior {x : X | p x}ᶜ) ∅
⊢ Dense.{u_1} (X := X) {x : X | p x}

Tactic:
rw [dense_iff_closure_eq, closure_eq_compl_interior_compl, compl_univ_iff]

Premises used: dense_iff_closure_eq, closure_eq_compl_interior_compl, Set.compl_univ_iff
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
p : X → Prop
hp : ∀ᵐ (x : X) ∂μ, p x
⊢ Eq.{u_1 + 1} (α := Set X) (interior {x : X | p x}ᶜ) ∅

Tactic:
μ.interior_eq_empty_of_null hp

Premises used: MeasureTheory.Measure.interior_eq_empty_of_null
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
p : X → Prop
hp : ∀ᵐ (x : X) ∂μ, p x
⊢ Eq.{u_1 + 1} (α := Set X) (interior {x : X | p x}ᶜ) ∅

Tactic:
exact μ.interior_eq_empty_of_null hp

Premises used: MeasureTheory.Measure.interior_eq_empty_of_null
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
h : f =ᶠ[ae (μ.restrict U)] g
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
⊢ ∀ᵐ (x : X) ∂μ, x ∈ U → f x = g x

Tactic:
replace h := ae_imp_of_ae_restrict h
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ∀ᵐ (x : X) ∂μ, x ∈ U → f x = g x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [ae_iff, Classical.not_imp] at h

Premises used: MeasureTheory.ae_iff, Classical.not_imp
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsOpen[inst] (U ∩ {a : X | f a ≠ g a})

Tactic:
isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) ?_

Premises used: Iff.mpr, Filter.inter_mem, And.left, IsOpen.mem_nhds, isOpen_iff_mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
refine : ∀ (a : X) (ha : a ∈ U ∩ {a : X | f a ≠ g a}), {a : X | f a ≠ g a} ∈ 𝓝 a
⊢ IsOpen[inst] (U ∩ {a : X | f a ≠ g a})

Tactic:
refine isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) ?_

Premises used: Iff.mpr, Filter.inter_mem, And.left, IsOpen.mem_nhds, isOpen_iff_mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
a : X
ha : a ∈ U ∩ {a : X | f a ≠ g a}
⊢ a ∈ U

Tactic:
rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩

Premises used: Prod.mk, Set.diagonal