awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
T : Set ι
hT : Countable.{u_6 + 1} (↑T : Type u_6)
t : Set α
ht : MeasurableSet t
⊢ LE.le (α := ℝ≥0∞) ((μ.restrict (⋃ i ∈ T, s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((sum fun (i : (↑T : Type u_6)) ↦ μ.restrict (s (↑i : ι)) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simpa [ht, inter_iUnion] using measure_biUnion_le μ hT (t ∩ s ·)

Premises used: MeasureTheory.measure_biUnion_le, Inter.inter, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
⊢ ae (μ.restrict (⋃ (i : ι), s i)) = ⨆ (i : ι), ae (μ.restrict (s i))

Tactic:
le_antisymm ((ae_sum_eq fun i => μ.restrict (s i)) ▸ ae_mono restrict_iUnion_le) <|
    iSup_le fun i => ae_mono <| restrict_mono (subset_iUnion s i) le_rfl

Premises used: le_rfl, MeasureTheory.Measure.restrict_mono, MeasureTheory.ae_mono, Set.subset_iUnion, le_antisymm, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ ae (μ.restrict (s ∪ t)) = ae (μ.restrict s) ⊔ ae (μ.restrict t)

Tactic:
simp [union_eq_iUnion, iSup_bool_eq]

Premises used: iSup_bool_eq, Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
⊢ Countable.{u_6 + 1} (↑t : Type u_6)

Tactic:
haveI := ht.to_subtype
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable.{u_6 + 1} (↑t : Type u_6)
rw : ae (μ.restrict (⋃ (x : (↑t : Type u_6)), s (↑x : ι))) = ⨆ i ∈ t, ae (μ.restrict (s i))
rw₁ :
  Eq.{u_2 + 1} (α := Filter α) (⨆ (i : (↑t : Type u_6)), ae (μ.restrict (s (↑i : ι)))) (⨆ i ∈ t, ae (μ.restrict (s i)))
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Filter α) (⨆ (i : (↑t : Type u_6)), ae (μ.restrict (s (↑i : ι))))
    (⨆ (i : (↑t : Type u_6)), ae (μ.restrict (s (↑i : ι))))
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Tactic:
rw [biUnion_eq_iUnion, ae_restrict_iUnion_eq, ← iSup_subtype'']

Premises used: iSup_subtype'', MeasureTheory.ae_restrict_iUnion_eq, Set.biUnion_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Finset ι
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Tactic:
ae_restrict_biUnion_eq s t.countable_toSet

Premises used: MeasureTheory.ae_restrict_biUnion_eq, Finset.countable_toSet
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ (i : ι), s i), p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), p x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (s ∪ t), p x) ↔ (∀ᵐ (x : α) ∂μ.restrict s, p x) ∧ ∀ᵐ (x : α) ∂μ.restrict t, p x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
p : α → Prop
simp_rw : {x : α | p x} ∈ ae (μ.restrict (⋃ i ∈ t, s i)) ↔ ∀ i ∈ t, {x : α | p x} ∈ ae (μ.restrict (s i))
simp_rw₁ :
  Membership.mem (γ := Filter α) (⨆ i ∈ t, ae (μ.restrict (s i))) {x : α | p x} ↔
    ∀ i ∈ t, {x : α | p x} ∈ ae (μ.restrict (s i))
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x

Tactic:
simp_rw [Filter.Eventually, ae_restrict_biUnion_eq s ht, mem_iSup]

Premises used: MeasureTheory.ae_restrict_biUnion_eq, Filter.Eventually, Filter.mem_iSup
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Finset ι
p : α → Prop
simp_rw : {x : α | p x} ∈ ae (μ.restrict (⋃ i ∈ t, s i)) ↔ ∀ i ∈ t, {x : α | p x} ∈ ae (μ.restrict (s i))
simp_rw₁ :
  Membership.mem (γ := Filter α) (⨆ i ∈ t, ae (μ.restrict (s i))) {x : α | p x} ↔
    ∀ i ∈ t, {x : α | p x} ∈ ae (μ.restrict (s i))
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x

Tactic:
simp_rw [Filter.Eventually, ae_restrict_biUnion_finset_eq s, mem_iSup]

Premises used: Filter.Eventually, Filter.mem_iSup, MeasureTheory.ae_restrict_biUnion_finset_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
f g : α → δ
simp_rw : (∀ᵐ (x : α) ∂μ.restrict (⋃ (i : ι), s i), f x = g x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x
simp_rw₁ :
  (∀ᶠ (x : α) in ⨆ (i : ι), ae (μ.restrict (s i)), f x = g x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x
⊢ f =ᶠ[ae (μ.restrict (⋃ (i : ι), s i))] g ↔ ∀ (i : ι), f =ᶠ[ae (μ.restrict (s i))] g

Tactic:
simp_rw [EventuallyEq, ae_restrict_iUnion_eq, eventually_iSup]

Premises used: MeasureTheory.ae_restrict_iUnion_eq, Filter.EventuallyEq, Filter.eventually_iSup
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
f g : α → δ
simp_rw : f =ᶠ[⨆ i ∈ t, ae (μ.restrict (s i))] g ↔ ∀ i ∈ t, f =ᶠ[ae (μ.restrict (s i))] g
simp_rw₁ : (∀ᶠ (x : α) in ⨆ i ∈ t, ae (μ.restrict (s i)), f x = g x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x
⊢ f =ᶠ[ae (μ.restrict (⋃ i ∈ t, s i))] g ↔ ∀ i ∈ t, f =ᶠ[ae (μ.restrict (s i))] g

Tactic:
simp_rw [ae_restrict_biUnion_eq s ht, EventuallyEq, eventually_iSup]

Premises used: MeasureTheory.ae_restrict_biUnion_eq, Filter.EventuallyEq, Filter.eventually_iSup
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Finset ι
f g : α → δ
⊢ f =ᶠ[ae (μ.restrict (⋃ i ∈ t, s i))] g ↔ ∀ i ∈ t, f =ᶠ[ae (μ.restrict (s i))] g

Tactic:
ae_eq_restrict_biUnion_iff s t.countable_toSet f g

Premises used: MeasureTheory.ae_eq_restrict_biUnion_iff, Finset.countable_toSet
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : LinearOrder α
a b : α
⊢ ae (μ.restrict (Ι a b)) = ae (μ.restrict (Ioc a b)) ⊔ ae (μ.restrict (Ioc b a))

Tactic:
simp only [uIoc_eq_union, ae_restrict_union_eq]

Premises used: MeasureTheory.ae_restrict_union_eq, Set.uIoc_eq_union
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : LinearOrder α
a b : α
P : α → Prop
rw :
  (∀ᶠ (x : α) in ae (μ.restrict (Ioc a b)) ⊔ ae (μ.restrict (Ioc b a)), P x) ↔
    (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x
rw₁ rw₂ :
  ((∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x) ↔
    (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x
⊢ (∀ᵐ (x : α) ∂μ.restrict (Ι a b), P x) ↔
    (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x

Tactic:
rw [ae_restrict_uIoc_eq, eventually_sup]

Premises used: Filter.eventually_sup, MeasureTheory.ae_restrict_uIoc_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x : α | p x} (μ.restrict s)
simp :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
simp only [ae_iff, ← compl_setOf, Measure.restrict_apply₀ hp.compl]

Premises used: MeasureTheory.NullMeasurableSet.compl, MeasureTheory.ae_iff, MeasureTheory.Measure.restrict_apply₀, Set.compl_setOf
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x : α | p x} (μ.restrict s)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) =
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [iff_iff_eq]

Premises used: iff_iff_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x : α | p x} (μ.restrict s)
e_a : ∀ (x : α), x ∈ {x : α | p x}ᶜ ∩ s ↔ Membership.mem (γ := Set α) {x : α | x ∈ s → p x}ᶜ x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) =
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x : α | p x} (μ.restrict s)
x : α
⊢ x ∈ {x : α | p x}ᶜ ∩ s ↔ Membership.mem (γ := Set α) {x : α | x ∈ s → p x}ᶜ x

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : MeasurableSet.{u_2} (α := α) {x : α | p x}
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
ae_restrict_iff₀ hp.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.ae_restrict_iff₀
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
h : ∀ᵐ (x : α) ∂μ.restrict s, p x
simp :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → p a)} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
simp only [ae_iff] at h ⊢

Premises used: MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
h : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → p a)} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [setOf_and, inter_comm] using measure_inter_eq_zero_of_restrict h

Premises used: Set.setOf_and, MeasureTheory.Measure.measure_inter_eq_zero_of_restrict, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
simp :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
simp only [ae_iff, ← compl_setOf, restrict_apply₀' hs]

Premises used: MeasureTheory.ae_iff, MeasureTheory.Measure.restrict_apply₀', Set.compl_setOf
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) =
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [iff_iff_eq]

Premises used: iff_iff_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
e_a : ∀ (x : α), x ∈ {x : α | p x}ᶜ ∩ s ↔ Membership.mem (γ := Set α) {x : α | x ∈ s → p x}ᶜ x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) =
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
x : α
⊢ x ∈ {x : α | p x}ᶜ ∩ s ↔ Membership.mem (γ := Set α) {x : α | x ∈ s → p x}ᶜ x

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : MeasurableSet s
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
ae_restrict_iff'₀ hs.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.ae_restrict_iff'₀
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ f =ᶠ[ae (μ.restrict s)] g

Tactic:
hfg.filter_mono ?_

Premises used: Filter.EventuallyEq.filter_mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
refine : ae (μ.restrict s) ≤ ae μ
⊢ f =ᶠ[ae (μ.restrict s)] g

Tactic:
refine hfg.filter_mono ?_

Premises used: Filter.EventuallyEq.filter_mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
rw : μ.restrict s ≪ μ
⊢ ae (μ.restrict s) ≤ ae μ

Tactic:
rw [Measure.ae_le_iff_absolutelyContinuous]

Premises used: MeasureTheory.Measure.ae_le_iff_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ μ.restrict s ≪ μ

Tactic:
absolutelyContinuous_restrict

Premises used: MeasureTheory.Measure.absolutelyContinuous_restrict
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ μ.restrict s ≪ μ

Tactic:
exact absolutelyContinuous_restrict

Premises used: MeasureTheory.Measure.absolutelyContinuous_restrict
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
⊢ ∀ᵐ (x : α) ∂μ.restrict s, x ∈ s

Tactic:
(ae_restrict_iff'₀ hs).2 (Filter.Eventually.of_forall fun _ => id)

Premises used: Iff.mpr, id, Filter.Eventually.of_forall, MeasureTheory.ae_restrict_iff'₀
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ.restrict s, x ∈ s

Tactic:
ae_restrict_mem₀ hs.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.ae_restrict_mem₀
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
p : α → Prop
h : ∀ x ∈ s, p x
⊢ ∀ᵐ (x : α) ∂μ.restrict s, p x

Tactic:
(ae_restrict_mem hs).mono h

Premises used: MeasureTheory.ae_restrict_mem, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_7
β : Type u_8
inst : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
h : EqOn f g s
hs : MeasurableSet s
⊢ f =ᶠ[ae (μ.restrict s)] g

Tactic:
ae_restrict_of_forall_mem hs h

Premises used: MeasureTheory.ae_restrict_of_forall_mem, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
h : ∀ᵐ (x : α) ∂μ, p x
⊢ ∀ᵐ (x : α) ∂μ.restrict s, p x

Tactic:
h.filter_mono (ae_mono Measure.restrict_le_self)

Premises used: Filter.Eventually.filter_mono, MeasureTheory.ae_mono, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
p : α → Prop
hst : s ⊆ t
h : ∀ᵐ (x : α) ∂μ.restrict t, p x
⊢ ∀ᵐ (x : α) ∂μ.restrict s, p x

Tactic:
h.filter_mono (ae_mono <| Measure.restrict_mono hst (le_refl μ))

Premises used: Filter.Eventually.filter_mono, le_refl, MeasureTheory.Measure.restrict_mono, MeasureTheory.ae_mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t : Set α
p : α → Prop
ht : ∀ᵐ (x : α) ∂μ.restrict t, p x
htc : ∀ᵐ (x : α) ∂μ.restrict tᶜ, p x
rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict tᶜ : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞) = 0
rw₁ : HAdd.hAdd (α := ℝ≥0∞) 0 0 = 0
rw₂ rw₃ : Eq (α := ℝ≥0∞) 0 0
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞)
      ((μ.restrict tᶜ : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞) =
    0

Tactic:
rw [ae_iff.1 ht, ae_iff.1 htc, zero_add]

Premises used: zero_add, MeasureTheory.ae_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
rw : f ⁻¹' t ∈ ae (μ.restrict s) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t ∈ Filter.map f (ae (μ.restrict s)) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [mem_map, mem_ae_iff, Measure.restrict_apply' hs]

Premises used: MeasureTheory.mem_ae_iff, MeasureTheory.Measure.restrict_apply', Filter.mem_map
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
ν : Measure α
⊢ (∀ᵐ (x : α) ∂μ + ν, p x) ↔ (∀ᵐ (x : α) ∂μ, p x) ∧ ∀ᵐ (x : α) ∂ν, p x

Tactic:
add_eq_zero

Premises used: Set.Mem, Filter.Eventually, setOf, WithTop.map₂, add_eq_zero, Option.map₂
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
p : α → Prop
s : Finset ι
μ : ι → Measure α
empty : (∀ᵐ (x : α) ∂∑ i ∈ ∅, μ i, p x) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ᵐ (x : α) ∂μ i, p x
cons :
  ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    ((∀ᵐ (x : α) ∂∑ i ∈ s, μ i, p x) ↔ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ i, p x) →
      ((∀ᵐ (x : α) ∂∑ i ∈ Finset.cons a s h, μ i, p x) ↔ ∀ i ∈ Finset.cons a s h, ∀ᵐ (x : α) ∂μ i, p x)
⊢ (∀ᵐ (x : α) ∂∑ i ∈ s, μ i, p x) ↔ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ i, p x

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
p : α → Prop
μ : ι → Measure α
⊢ (∀ᵐ (x : α) ∂∑ i ∈ ∅, μ i, p x) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ᵐ (x : α) ∂μ i, p x

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
p : α → Prop
μ : ι → Measure α
a : ι
s : Finset ι
h : a ∉ s
h_1 : (∀ᵐ (x : α) ∂∑ i ∈ s, μ i, p x) ↔ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ i, p x
⊢ (∀ᵐ (x : α) ∂∑ i ∈ Finset.cons a s h, μ i, p x) ↔ ∀ i ∈ Finset.cons a s h, ∀ᵐ (x : α) ∂μ i, p x

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
δ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → β
g g' : β → δ
hf : AEMeasurable f μ
h : g =ᶠ[ae ν] g'
h2 : Measure.map f μ ≪ ν
⊢ g ∘ f =ᶠ[ae μ] g' ∘ f

Tactic:
(tendsto_ae_map hf).mono_right h2.ae_le h

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, MeasureTheory.Measure.tendsto_ae_map, MeasureTheory.Measure.AbsolutelyContinuous.ae_le, Set.preimage, Filter.Tendsto.mono_right
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
δ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → β
g g' : β → δ
hf : QuasiMeasurePreserving f μ ν
h : g =ᵐ[ν] g'
⊢ g ∘ f =ᵐ[μ] g' ∘ f

Tactic:
ae_eq_comp' hf.aemeasurable h hf.absolutelyContinuous

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.ae_eq_comp'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
δ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
g g' : β → δ
hf : AEMeasurable f μ
h : g =ᶠ[ae (F := Measure β) (Measure.map f μ)] g'
⊢ g ∘ f =ᶠ[ae μ] g' ∘ f

Tactic:
ae_eq_comp' hf h AbsolutelyContinuous.rfl

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.ae_eq_comp'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
f g : α → β
⊢ f / g =ᶠ[ae μ] 1 ↔ f =ᶠ[ae μ] g

Tactic:
⟨fun h ↦ h.mono fun x hx ↦ ?_, fun h ↦ h.mono fun x hx ↦ ?_⟩

Premises used: Filter.Eventually.mono, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
f g : α → β
refine_1 : ∀ (h : f / g =ᶠ[ae μ] 1) (x : α) (hx : (f / g) x = 1 x), f x = g x
refine_2 : ∀ (h : f =ᶠ[ae μ] g) (x : α) (hx : f x = g x), (f / g) x = 1 x
⊢ f / g =ᶠ[ae μ] 1 ↔ f =ᶠ[ae μ] g

Tactic:
refine ⟨fun h ↦ h.mono fun x hx ↦ ?_, fun h ↦ h.mono fun x hx ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
f g : α → β
h : f / g =ᶠ[ae μ] 1
x : α
hx : (f / g) x = 1 x
refine_1 : ∀ (hx : f x / g x = 1 x), f x = g x
refine_1₁ : ∀ (hx : f x / g x = 1), f x = g x
refine_1₂ refine_1₃ refine_1₄ refine_1₅ : ∀ (hx : f x = g x), f x = g x
⊢ f x = g x

Tactic:
rwa [Pi.div_apply, Pi.one_apply, div_eq_one] at hx

Premises used: Pi.one_apply, Pi.div_apply, div_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
f g : α → β
h : f =ᶠ[ae μ] g
x : α
hx : f x = g x
refine_2 : f x / g x = 1 x
refine_2₁ : f x / g x = 1
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : f x = g x
⊢ (f / g) x = 1 x

Tactic:
rwa [Pi.div_apply, Pi.one_apply, div_eq_one]

Premises used: Pi.one_apply, Pi.div_apply, div_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
inst_1 : LE β
inst_2 : MulRightMono β
f g : α → β
⊢ 1 ≤ᶠ[ae μ] g / f ↔ f ≤ᶠ[ae μ] g

Tactic:
⟨fun h ↦ h.mono fun a ha ↦ ?_, fun h ↦ h.mono fun a ha ↦ ?_⟩

Premises used: Filter.Eventually.mono, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
inst_1 : LE β
inst_2 : MulRightMono β
f g : α → β
refine_1 : ∀ (h : 1 ≤ᶠ[ae μ] g / f) (a : α) (ha : 1 a ≤ (g / f) a), f a ≤ g a
refine_2 : ∀ (h : f ≤ᶠ[ae μ] g) (a : α) (ha : f a ≤ g a), 1 a ≤ (g / f) a
⊢ 1 ≤ᶠ[ae μ] g / f ↔ f ≤ᶠ[ae μ] g

Tactic:
refine ⟨fun h ↦ h.mono fun a ha ↦ ?_, fun h ↦ h.mono fun a ha ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
inst_1 : LE β
inst_2 : MulRightMono β
f g : α → β
h : 1 ≤ᶠ[ae μ] g / f
a : α
ha : 1 a ≤ (g / f) a
refine_1 : ∀ (ha : 1 ≤ (g / f) a), f a ≤ g a
refine_1₁ : ∀ (ha : 1 ≤ g a / f a), f a ≤ g a
refine_1₂ refine_1₃ refine_1₄ refine_1₅ : ∀ (ha : f a ≤ g a), f a ≤ g a
⊢ f a ≤ g a

Tactic:
rwa [Pi.one_apply, Pi.div_apply, one_le_div'] at ha

Premises used: Pi.one_apply, one_le_div', Pi.div_apply
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
inst_1 : LE β
inst_2 : MulRightMono β
f g : α → β
h : f ≤ᶠ[ae μ] g
a : α
ha : f a ≤ g a
refine_2 : 1 ≤ (g / f) a
refine_2₁ : 1 ≤ g a / f a
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : f a ≤ g a
⊢ 1 a ≤ (g / f) a

Tactic:
rwa [Pi.one_apply, Pi.div_apply, one_le_div']

Premises used: Pi.one_apply, one_le_div', Pi.div_apply