awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
refine_1 : μ.withDensity (f - g) ≤ μ.withDensity f - μ.withDensity g
refine_2 : μ.withDensity f - μ.withDensity g ≤ μ.withDensity (f - g)
⊢ μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
⊢ MeasurableSet t

Tactic:
have ht : MeasurableSet t := measurableSet_le hf hg
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
refine_1 :
  (μ.withDensity (f - g)).restrict t + (μ.withDensity (f - g)).restrict tᶜ ≤
    (μ.withDensity f - μ.withDensity g).restrict t + (μ.withDensity f - μ.withDensity g).restrict tᶜ
⊢ μ.withDensity (f - g) ≤ μ.withDensity f - μ.withDensity g

Tactic:
rw [← restrict_add_restrict_compl (μ := μ.withDensity (f - g)) ht,
      ← restrict_add_restrict_compl (μ := μ.withDensity f - μ.withDensity g) ht]

Premises used: MeasureTheory.Measure.restrict_add_restrict_compl
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
simp : Eq (α := ℝ≥0∞) ((μ.withDensity (f - g) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ.withDensity (f - g)).restrict t = 0

Tactic:
simp only [restrict_eq_zero]

Premises used: MeasureTheory.Measure.restrict_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
⊢ Measurable (f - g)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
rw : f - g =ᶠ[ae (μ.restrict t)] 0
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f - g) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ ht, lintegral_eq_zero_iff (by fun_prop)]

Premises used: MeasureTheory.lintegral_eq_zero_iff, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
⊢ f - g =ᶠ[ae (μ.restrict t)] 0

Tactic:
ae_restrict_of_forall_mem ht fun x hx ↦ ?_

Premises used: MeasureTheory.ae_restrict_of_forall_mem, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
refine : ∀ (x : α) (hx : x ∈ t), (f - g) x = 0 x
⊢ f - g =ᶠ[ae (μ.restrict t)] 0

Tactic:
refine ae_restrict_of_forall_mem ht fun x hx ↦ ?_

Premises used: MeasureTheory.ae_restrict_of_forall_mem
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
x : α
hx : x ∈ t
⊢ (f - g) x = 0 x

Tactic:
simpa [tsub_eq_zero_iff_le]

Premises used: tsub_eq_zero_iff_le
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
⊢ (μ.withDensity (f - g)).restrict t = 0

Tactic:
have h_zero : (μ.withDensity (f - g)).restrict t = 0 := by
      simp only [restrict_eq_zero]
      rw [withDensity_apply _ ht, lintegral_eq_zero_iff (by fun_prop)]
      refine ae_restrict_of_forall_mem ht fun x hx ↦ ?_
      simpa [tsub_eq_zero_iff_le]
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
refine_1 :
  (μ.withDensity (f - g)).restrict tᶜ ≤
    (μ.withDensity f - μ.withDensity g).restrict t + (μ.withDensity f - μ.withDensity g).restrict tᶜ
⊢ (μ.withDensity (f - g)).restrict t + (μ.withDensity (f - g)).restrict tᶜ ≤
    (μ.withDensity f - μ.withDensity g).restrict t + (μ.withDensity f - μ.withDensity g).restrict tᶜ

Tactic:
rw [h_zero, zero_add]

Premises used: zero_add
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
refine_1 : (μ.withDensity (f - g)).restrict tᶜ ≤ (μ.withDensity f - μ.withDensity g).restrict tᶜ
⊢ (μ.withDensity (f - g)).restrict tᶜ ≤
    (μ.withDensity f - μ.withDensity g).restrict t + (μ.withDensity f - μ.withDensity g).restrict tᶜ

Tactic:
suffices (μ.withDensity (f - g)).restrict tᶜ ≤
      (μ.withDensity f - μ.withDensity g).restrict tᶜ from this.trans (Measure.le_add_left le_rfl)
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
refine_1 : (μ.withDensity (f - g)).restrict tᶜ ≤ (μ.withDensity f).restrict tᶜ - (μ.withDensity g).restrict tᶜ
⊢ (μ.withDensity (f - g)).restrict tᶜ ≤ (μ.withDensity f - μ.withDensity g).restrict tᶜ

Tactic:
rw [restrict_sub_eq_restrict_sub_restrict ht.compl]

Premises used: MeasurableSet.compl, MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrict
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
refine_1 : (μ.restrict tᶜ).withDensity (f - g) ≤ (μ.restrict tᶜ).withDensity f - (μ.restrict tᶜ).withDensity g
⊢ (μ.withDensity (f - g)).restrict tᶜ ≤ (μ.withDensity f).restrict tᶜ - (μ.withDensity g).restrict tᶜ

Tactic:
simp_rw [restrict_withDensity ht.compl]

Premises used: MeasureTheory.restrict_withDensity, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
rw : IsFiniteMeasure ((μ.withDensity g).restrict tᶜ)
⊢ IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)

Tactic:
rw [← restrict_withDensity ht.compl]

Premises used: MeasureTheory.restrict_withDensity, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ IsFiniteMeasure ((μ.withDensity g).restrict tᶜ)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)

Tactic:
have : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g) := by
      rw [← restrict_withDensity ht.compl]
      infer_instance
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
refine_1 : g ≤ᶠ[ae (μ.restrict tᶜ)] f
⊢ (μ.restrict tᶜ).withDensity (f - g) ≤ (μ.restrict tᶜ).withDensity f - (μ.restrict tᶜ).withDensity g

Tactic:
rw [withDensity_sub_of_le hg]

Premises used: MeasureTheory.Measure.withDensity_sub_of_le
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
⊢ g ≤ᶠ[ae (μ.restrict tᶜ)] f

Tactic:
ae_restrict_of_forall_mem ht.compl fun x hx ↦ ?_

Premises used: MeasureTheory.ae_restrict_of_forall_mem, MeasurableSet.compl, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
refine_1 : ∀ (x : α) (hx : x ∈ tᶜ), g x ≤ f x
⊢ g ≤ᶠ[ae (μ.restrict tᶜ)] f

Tactic:
refine ae_restrict_of_forall_mem ht.compl fun x hx ↦ ?_

Premises used: MeasureTheory.ae_restrict_of_forall_mem, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
x : α
hx : x ∈ tᶜ
⊢ g x < f x

Tactic:
simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le, t] at hx

Premises used: not_le, Set.mem_setOf_eq, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
x : α
hx : g x < f x
⊢ g x ≤ f x

Tactic:
hx.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
x : α
hx : g x < f x
⊢ g x ≤ f x

Tactic:
exact hx.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity f - μ.withDensity g ≤ μ.withDensity (f - g)

Tactic:
sub_le_of_le_add ?_

Premises used: MeasureTheory.Measure.sub_le_of_le_add
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
refine_2 : μ.withDensity f ≤ μ.withDensity (f - g) + μ.withDensity g
⊢ μ.withDensity f - μ.withDensity g ≤ μ.withDensity (f - g)

Tactic:
refine sub_le_of_le_add ?_

Premises used: MeasureTheory.Measure.sub_le_of_le_add
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
refine_2 : μ.withDensity f ≤ μ.withDensity (f - g + g)
⊢ μ.withDensity f ≤ μ.withDensity (f - g) + μ.withDensity g

Tactic:
rw [← withDensity_add_right _ hg]

Premises used: MeasureTheory.withDensity_add_right
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity f ≤ μ.withDensity (f - g + g)

Tactic:
withDensity_mono (ae_of_all _ fun x ↦ le_tsub_add)

Premises used: MeasureTheory.ae_of_all, le_tsub_add, MeasureTheory.withDensity_mono
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity f ≤ μ.withDensity (f - g + g)

Tactic:
exact withDensity_mono (ae_of_all _ fun x ↦ le_tsub_add)

Premises used: MeasureTheory.ae_of_all, le_tsub_add, MeasureTheory.withDensity_mono
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
ι : Sort u_2
p : ι → Prop
s : ι → Set X
x : X
hl : (𝓝 x).HasBasis p s
⊢ x ∈ μ.support ↔ ∀ (i : ι), p i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) (s i) : ENNReal)

Tactic:
hl.frequently_smallSets pos_mono

Premises used: Set.Mem, Filter.HasBasis.frequently_smallSets, setOf, Filter.Frequently, MeasureTheory.Measure.support, MeasureTheory.pos_mono, Not
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
x : X
⊢ x ∈ μ.support ↔
    ∃ᶠ (u : Set X) in (𝓝 x).smallSets, LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) u : ENNReal)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Filter.Frequently, MeasureTheory.Measure.support, Not
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
x : X
⊢ x ∈ μ.support ↔ ∀ U ∈ 𝓝 x, LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) U : ENNReal)

Tactic:
(𝓝 x).basis_sets.mem_measureSupport

Premises used: nhds, Filter.basis_sets, Filter.HasBasis.mem_measureSupport
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
⊢ μ.support = Set.univ

Tactic:
simpa [Set.eq_univ_iff_forall, mem_support_iff_forall] using fun _ _ ↦ μ.measure_pos_of_mem_nhds

Premises used: Set.eq_univ_iff_forall, MeasureTheory.Measure.mem_support_iff_forall, MeasureTheory.Measure.measure_pos_of_mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ ν : Measure X
hμν : μ ≪ ν
⊢ μ.support ⊆ ν.support

Tactic:
fun _ hx ↦ hx.mp <| .of_forall hμν.pos_mono

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.pos_mono, Set.Mem, setOf, Filter.Eventually.of_forall, Set.Subset, Filter.Frequently, MeasureTheory.Measure.support, Filter.Frequently.mp, Not
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ ν : Measure X
h : μ ≤ ν
⊢ μ.support ⊆ ν.support

Tactic:
h.absolutelyContinuous.support_mono

Premises used: LE.le.absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.support_mono
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
x : X
⊢ x ∉ μ.support ↔
    ∀ᶠ (u : Set X) in (𝓝 x).smallSets, Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) u : ENNReal) (0 : ENNReal)

Tactic:
simp [mem_support_iff]

Premises used: MeasureTheory.Measure.mem_support_iff
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
ι : Sort u_2
p : ι → Prop
s : ι → Set X
x : X
hl : (𝓝 x).HasBasis p s
⊢ x ∉ μ.support ↔ ∃ (i : ι), p i ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s i) : ENNReal) (0 : ENNReal)

Tactic:
simp [hl.mem_measureSupport]

Premises used: Filter.HasBasis.mem_measureSupport
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
⊢ Eq.{u_1 + 1} (α := Set X) (Measure.support 0) ∅

Tactic:
simp [Measure.support]

Premises used: MeasureTheory.Measure.support
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ ν : Measure X
h : ∀ (x : X), x ∈ (μ + ν).support ↔ x ∈ μ.support ∪ ν.support
⊢ (μ + ν).support = μ.support ∪ ν.support

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ ν : Measure X
x : X
⊢ x ∈ (μ + ν).support ↔ x ∈ μ.support ∪ ν.support

Tactic:
simp [mem_support_iff]

Premises used: MeasureTheory.Measure.mem_support_iff
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
x : X
⊢ x ∉ μ.support ↔ ∃ U ∈ 𝓝 x, Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) U : ENNReal) (0 : ENNReal)

Tactic:
simp [mem_support_iff_forall]

Premises used: MeasureTheory.Measure.mem_support_iff_forall
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
⊢ μ.support =
    {x : X |
      ∀ (u : Set X),
        x ∈ u → IsOpen[inst] u → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) u : ENNReal)}

Tactic:
simp [Set.ext_iff, nhds_basis_opens _ |>.mem_measureSupport]

Premises used: Set.ext_iff, nhds_basis_opens, Filter.HasBasis.mem_measureSupport
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
simp_rw :
  ∀ (x : X),
    (∀ (i : Set X),
        x ∈ i ∧ IsOpen[inst] i →
          ∃ x ∈ i,
            ∀ (i : Set X),
              x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) i : ENNReal)) →
      ∀ (i : Set X),
        x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) i : ENNReal)
⊢ IsClosed[inst] μ.support

Tactic:
simp_rw [isClosed_iff_frequently, nhds_basis_opens _ |>.mem_measureSupport,
    nhds_basis_opens _ |>.frequently_iff]

Premises used: isClosed_iff_frequently, Filter.HasBasis.frequently_iff, nhds_basis_opens, Filter.HasBasis.mem_measureSupport
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
⊢ ∀ (x : X),
    (∀ (i : Set X),
        x ∈ i ∧ IsOpen[inst] i →
          ∃ x ∈ i,
            ∀ (i : Set X),
              x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) i : ENNReal)) →
      ∀ (i : Set X),
        x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) i : ENNReal)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
⊢ IsOpen[inst] μ.supportᶜ

Tactic:
isOpen_compl_iff.mpr μ.isClosed_support

Premises used: Iff.mpr, MeasureTheory.Measure.isClosed_support, isOpen_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
t : Set X
ht : IsOpen[inst] t
h : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ t ⊆ μ.supportᶜ

Tactic:
fun _ hx ↦ notMem_support_iff_exists.mpr ⟨t, ht.mem_nhds hx, h⟩

Premises used: Iff.mpr, Set.Mem, setOf, Set.Subset, MeasureTheory.Measure.notMem_support_iff_exists, And.intro, IsOpen.mem_nhds, Exists.intro, Not
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
t : Set X
ht : IsClosed[inst] t
h : t ∈ ae μ
⊢ μ.support ⊆ t

Tactic:
Set.compl_subset_compl.mp <| subset_compl_support_of_isOpen ht.isOpen_compl h

Premises used: IsClosed.isOpen_compl, Set.compl_subset_compl, MeasureTheory.Measure.subset_compl_support_of_isOpen, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
h :
  ∀ (x : X),
    x ∈ μ.supportᶜ ↔
      Membership.mem (γ := Set X)
        (⋃₀ {t : Set X | IsOpen[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) t : ENNReal) (0 : ENNReal)}) x
⊢ μ.supportᶜ =
    ⋃₀ {t : Set X | IsOpen[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) t : ENNReal) (0 : ENNReal)}

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
x : X
⊢ x ∈ μ.supportᶜ ↔
    Membership.mem (γ := Set X)
      (⋃₀ {t : Set X | IsOpen[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) t : ENNReal) (0 : ENNReal)}) x

Tactic:
simp only [Set.mem_compl_iff, Set.mem_sUnion, Set.mem_setOf_eq, and_right_comm,
    nhds_basis_opens x |>.notMem_measureSupport, fun t ↦ and_comm (b := x ∈ t)]

Premises used: Filter.HasBasis.notMem_measureSupport, Set.mem_setOf_eq, and_comm, and_right_comm, nhds_basis_opens, Set.mem_sUnion, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
⊢ μ.supportᶜᶜ =
    (⋃₀ {t : Set X | IsOpen[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) t : ENNReal) (0 : ENNReal)})ᶜ

Tactic:
congr($(compl_support_eq_sUnion (μ := μ))ᶜ)

Premises used: congrArg, Compl.compl, id, MeasureTheory.Measure.compl_support_eq_sUnion
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
h : μ.support = μ.supportᶜᶜ
h₁ :
  Eq.{u_1 + 1} (α := Set X)
    (⋂₀ {t : Set X | IsClosed[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) tᶜ : ENNReal) (0 : ENNReal)})
    (⋃₀ {t : Set X | IsOpen[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) t : ENNReal) (0 : ENNReal)})ᶜ
⊢ μ.support =
    ⋂₀ {t : Set X | IsClosed[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) tᶜ : ENNReal) (0 : ENNReal)}

Tactic:
convert! congr($(compl_support_eq_sUnion (μ := μ))ᶜ)

Premises used: MeasureTheory.Measure.compl_support_eq_sUnion
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
⊢ μ.support = μ.supportᶜᶜ

Tactic:
simp [Set.compl_sUnion, compl_involutive.image_eq_preimage_symm]

Premises used: compl_involutive, Set.compl_sUnion, Function.Involutive.image_eq_preimage_symm
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
⊢ Eq.{u_1 + 1} (α := Set X)
    (⋂₀ {t : Set X | IsClosed[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) tᶜ : ENNReal) (0 : ENNReal)})
    (⋃₀ {t : Set X | IsOpen[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) t : ENNReal) (0 : ENNReal)})ᶜ

Tactic:
simp [Set.compl_sUnion, compl_involutive.image_eq_preimage_symm]

Premises used: compl_involutive, Set.compl_sUnion, Function.Involutive.image_eq_preimage_symm
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
h : IsLindelof μ.supportᶜ
⊢ μ.support ∈ ae μ

Tactic:
compl_compl μ.support ▸ h.compl_mem_sets_of_nhdsWithin fun s hs ↦ ?_

Premises used: compl_compl, Eq.rec, IsLindelof.compl_mem_sets_of_nhdsWithin, MeasureTheory.Measure.support