awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ae μ ⊓ 𝓟 s ≤ ae (μ.restrict s)

Tactic:
fun _s hs =>
  eventually_inf_principal.2 (ae_imp_of_ae_restrict hs)

Premises used: Filter.eventually_inf_principal, Iff.mpr, Set.Mem, Filter.Eventually, setOf, MeasureTheory.ae_imp_of_ae_restrict
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
h : ∀ (t : Set α), t ∈ ae (μ.restrict s) ↔ t ∈ ae μ ⊓ 𝓟 s
⊢ ae (μ.restrict s) = ae μ ⊓ 𝓟 s

Tactic:
ext t
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | a ∉ t ∧ a ∈ s} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t ∈ ae (μ.restrict s) ↔ t ∈ ae μ ⊓ 𝓟 s

Tactic:
simp only [mem_inf_principal, mem_ae_iff, restrict_apply_eq_zero' hs, compl_setOf,
    Classical.not_imp, fun a => and_comm (a := a ∈ s) (b := a ∉ t)]

Premises used: and_comm, Classical.not_imp, MeasureTheory.Measure.restrict_apply_eq_zero', Filter.mem_inf_principal, MeasureTheory.mem_ae_iff, Set.compl_setOf
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | a ∉ t ∧ a ∈ s} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ae (μ.restrict s) ≤ ae μ

Tactic:
ae_mono restrict_le_self

Premises used: MeasureTheory.ae_mono, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ae (μ.restrict s) = ⊥ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
ae_eq_bot.trans restrict_eq_zero

Premises used: MeasureTheory.Measure.restrict_eq_zero, MeasureTheory.ae_eq_bot, Iff.trans
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ (ae (μ.restrict s)).NeBot ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
neBot_iff.trans ae_restrict_eq_bot.not

Premises used: MeasureTheory.ae_restrict_eq_bot, Filter.neBot_iff, Iff.not, Iff.trans
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
simp : ∃ t₁ ∈ ae μ, ∃ (t₂ : Set α), s ⊆ t₂ ∧ s = t₁ ∩ t₂
⊢ s ∈ ae (μ.restrict s)

Tactic:
simp only [ae_restrict_eq hs, mem_principal, mem_inf_iff]

Premises used: Filter.mem_principal, MeasureTheory.ae_restrict_eq, Filter.mem_inf_iff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∃ t₁ ∈ ae μ, ∃ (t₂ : Set α), s ⊆ t₂ ∧ s = t₁ ∩ t₂

Tactic:
⟨_, univ_mem, s, Subset.rfl, (univ_inter s).symm⟩

Premises used: Set.univ_inter, Set.Subset.rfl, And.intro, Exists.intro, Filter.univ_mem, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∃ t₁ ∈ ae μ, ∃ (t₂ : Set α), s ⊆ t₂ ∧ s = t₁ ∩ t₂

Tactic:
exact ⟨_, univ_mem, s, Subset.rfl, (univ_inter s).symm⟩
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : α → Prop
hst : s =ᶠ[ae μ] t
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) → ∀ᵐ (x : α) ∂μ.restrict t, p x

Tactic:
simp [Measure.restrict_congr_set hst]

Premises used: MeasureTheory.Measure.restrict_congr_set
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : α → Prop
hst : s =ᶠ[ae μ] t
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict t, p x

Tactic:
⟨ae_restrict_of_ae_eq_of_ae_restrict hst, ae_restrict_of_ae_eq_of_ae_restrict hst.symm⟩

Premises used: Iff.intro, MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᶠ[ae (μ.restrict sᶜ)] fun (x : α) ↦ b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply₀ (f_mble t_mble)]

Premises used: MeasureTheory.Measure.restrict_apply₀
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᶠ[ae (μ.restrict sᶜ)] fun (x : α) ↦ b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
rw :
  ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)) {t : Set β}
    (t_mble : MeasurableSet t) (ht : b ∉ t),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
rw₁ :
  ∀ (hs : Eq (α := ℝ≥0∞) ((μ.restrict sᶜ : (a : Set α) → ℝ≥0∞) {a : α | ¬f a = b} : ℝ≥0∞) (0 : ℝ≥0∞)) {t : Set β}
    (t_mble : MeasurableSet t) (ht : b ∉ t), NullMeasurableSet {a : α | ¬f a = b} (μ.restrict sᶜ)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)

Tactic:
rw [EventuallyEq, ae_iff, Measure.restrict_apply₀] at hs

Premises used: Filter.EventuallyEq, MeasureTheory.ae_iff, MeasureTheory.Measure.restrict_apply₀
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)

Tactic:
apply le_antisymm _ (measure_mono inter_subset_left)

Premises used: Set.inter_subset_left, le_antisymm, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
apply :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s ∪ f ⁻¹' t ∩ sᶜ) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)

Tactic:
apply (measure_mono (Eq.symm (inter_union_compl (f ⁻¹' t) s)).le).trans

Premises used: Eq.le, Set.preimage, Set.inter_union_compl, MeasureTheory.measure_mono, LE.le.trans, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
apply :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s ∪ f ⁻¹' t ∩ sᶜ) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)

Tactic:
apply (measure_union_le _ _).trans

Premises used: LE.le.trans, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s)

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
suffices : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s)

Tactic:
suffices μ ((f ⁻¹' t) ∩ sᶜ) = 0 by simp [this]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
rw :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero, ← hs]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
h : f ⁻¹' t ⊆ {a : α | ¬f a = b}
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ f ⁻¹' t ⊆ {a : α | ¬f a = b}

Tactic:
fun x hx hfx ↦ ht (hfx ▸ hx)

Premises used: Set.Mem, setOf, Eq.rec, Set.Subset, Not
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ f ⁻¹' t ⊆ {a : α | ¬f a = b}

Tactic:
exact fun x hx hfx ↦ ht (hfx ▸ hx)
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ.restrict sᶜ : (a : Set α) → ℝ≥0∞) {a : α | ¬f a = b} : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ NullMeasurableSet {a : α | ¬f a = b} (μ.restrict sᶜ)

Tactic:
NullMeasurableSet.of_null hs

Premises used: MeasureTheory.NullMeasurableSet.of_null
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ.restrict sᶜ : (a : Set α) → ℝ≥0∞) {a : α | ¬f a = b} : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ NullMeasurableSet {a : α | ¬f a = b} (μ.restrict sᶜ)

Tactic:
exact NullMeasurableSet.of_null hs

Premises used: MeasureTheory.NullMeasurableSet.of_null
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
⊢ NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet (t ∩ s) μ

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
refine_1 : ∀ (h : NullMeasurableSet t (μ.restrict s)), NullMeasurableSet (t ∩ s) μ
refine_2 : ∀ (h : NullMeasurableSet (t ∩ s) μ), NullMeasurableSet t (μ.restrict s)
⊢ NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet (t ∩ s) μ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
⊢ ∃ t' ⊇ t, MeasurableSet t' ∧ t' =ᶠ[ae (μ.restrict s)] t

Tactic:
h.exists_measurable_superset_ae_eq

Premises used: MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
refine_1 : ∀ (t' : Set α) (ht' : MeasurableSet t') (t't : t' =ᶠ[ae (μ.restrict s)] t), NullMeasurableSet (t ∩ s) μ
⊢ NullMeasurableSet (t ∩ s) μ

Tactic:
obtain ⟨t', -, ht', t't⟩ : ∃ t' ⊇ t, MeasurableSet t' ∧ t' =ᵐ[μ.restrict s] t :=
      h.exists_measurable_superset_ae_eq

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t') = (x ∈ t)

Tactic:
have : ∀ᵐ x ∂μ, x ∈ s → (x ∈ t') = (x ∈ t) :=
        (ae_restrict_iff'₀ hs).1 t't
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t') = (x ∈ t)
h₁ : ∀ (y : α) (hy : y ∈ s → (y ∈ t') = (y ∈ t)), (t' ∩ s) y = (t ∩ s) y
⊢ t' ∩ s =ᶠ[ae μ] t ∩ s

Tactic:
filter_upwards [this] with y hy
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t') = (x ∈ t)
y : α
hy : y ∈ s → (y ∈ t') = (y ∈ t)
⊢ (y ∈ t' ∩ s) = (y ∈ t ∩ s)

Tactic:
simpa only [eq_iff_iff, mem_inter_iff, and_congr_left_iff] using hy

Premises used: Set.mem_inter_iff, and_congr_left_iff, eq_iff_iff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
⊢ t' ∩ s =ᶠ[ae μ] t ∩ s

Tactic:
have A : (t' ∩ s : Set α) =ᵐ[μ] (t ∩ s : Set α) := by
      have : ∀ᵐ x ∂μ, x ∈ s → (x ∈ t') = (x ∈ t) :=
        (ae_restrict_iff'₀ hs).1 t't
      filter_upwards [this] with y hy
      change (y ∈ t' ∩ s) = (y ∈ t ∩ s)
      simpa only [eq_iff_iff, mem_inter_iff, and_congr_left_iff] using hy
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
A : t' ∩ s =ᶠ[ae μ] t ∩ s
⊢ ∃ s' ⊇ s, MeasurableSet s' ∧ s' =ᶠ[ae μ] s

Tactic:
hs.exists_measurable_superset_ae_eq

Premises used: MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
A : t' ∩ s =ᶠ[ae μ] t ∩ s
refine_1 : ∀ (s' : Set α) (hs' : MeasurableSet s') (s's : s' =ᶠ[ae μ] s), NullMeasurableSet (t ∩ s) μ
⊢ NullMeasurableSet (t ∩ s) μ

Tactic:
obtain ⟨s', -, hs', s's⟩ : ∃ s' ⊇ s, MeasurableSet s' ∧ s' =ᵐ[μ] s :=
      hs.exists_measurable_superset_ae_eq

Premises used: MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
A : t' ∩ s =ᶠ[ae μ] t ∩ s
s' : Set α
hs' : MeasurableSet s'
s's : s' =ᶠ[ae μ] s
⊢ t' ∩ s' =ᶠ[ae μ] t' ∩ s

Tactic:
have B : (t' ∩ s' : Set α) =ᵐ[μ] (t' ∩ s : Set α) :=
      ae_eq_set_inter (EventuallyEq.refl _ _) s's
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
A : t' ∩ s =ᶠ[ae μ] t ∩ s
s' : Set α
hs' : MeasurableSet s'
s's : s' =ᶠ[ae μ] s
B : t' ∩ s' =ᶠ[ae μ] t' ∩ s
⊢ NullMeasurableSet (t ∩ s) μ

Tactic:
(ht'.inter hs').nullMeasurableSet.congr (B.trans A)

Premises used: Filter.EventuallyEq.trans, MeasurableSet.nullMeasurableSet, MeasureTheory.NullMeasurableSet.congr, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
A : t' ∩ s =ᶠ[ae μ] t ∩ s
s' : Set α
hs' : MeasurableSet s'
s's : s' =ᶠ[ae μ] s
B : t' ∩ s' =ᶠ[ae μ] t' ∩ s
⊢ NullMeasurableSet (t ∩ s) μ

Tactic:
exact (ht'.inter hs').nullMeasurableSet.congr (B.trans A)

Premises used: Filter.EventuallyEq.trans, MeasurableSet.nullMeasurableSet, MeasureTheory.NullMeasurableSet.congr, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
h₁ : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (t \ s) (μ.restrict s)

Tactic:
apply NullMeasurableSet.of_null

Premises used: MeasureTheory.NullMeasurableSet.of_null
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply₀' hs]

Premises used: MeasureTheory.Measure.restrict_apply₀'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ NullMeasurableSet (t \ s) (μ.restrict s)

Tactic:
have A : NullMeasurableSet (t \ s) (μ.restrict s) := by
      apply NullMeasurableSet.of_null
      rw [Measure.restrict_apply₀' hs]
      simp
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
A : NullMeasurableSet (t \ s) (μ.restrict s)
⊢ NullMeasurableSet (t ∩ s) (μ.restrict s)

Tactic:
have B : NullMeasurableSet (t ∩ s) (μ.restrict s) :=
      h.mono_ac absolutelyContinuous_restrict
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
A : NullMeasurableSet (t \ s) (μ.restrict s)
B : NullMeasurableSet (t ∩ s) (μ.restrict s)
⊢ NullMeasurableSet t (μ.restrict s)

Tactic:
simpa using A.union B

Premises used: MeasureTheory.NullMeasurableSet.union
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
⊢ NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet t μ

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.mono_ac absolutelyContinuous_restrict⟩

Premises used: MeasureTheory.Measure.absolutelyContinuous_restrict, Iff.intro, MeasureTheory.NullMeasurableSet.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
refine : ∀ (h : NullMeasurableSet t (μ.restrict s)), NullMeasurableSet t μ
⊢ NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet t μ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.mono_ac absolutelyContinuous_restrict⟩
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
⊢ ∃ t' ⊆ t, MeasurableSet t' ∧ t' =ᶠ[ae (μ.restrict s)] t

Tactic:
h.exists_measurable_subset_ae_eq

Premises used: MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
obtain :
  ∀ (t' : Set α) (t'_subs : t' ⊆ t) (ht' : MeasurableSet t') (t't : t' =ᶠ[ae (μ.restrict s)] t), NullMeasurableSet t μ
⊢ NullMeasurableSet t μ

Tactic:
obtain ⟨t', t'_subs, ht', t't⟩ : ∃ t' ⊆ t, MeasurableSet t' ∧ t' =ᵐ[μ.restrict s] t :=
    h.exists_measurable_subset_ae_eq

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
h₁ : ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t' ↔ x ∈ t
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)

Tactic:
apply ae_imp_of_ae_restrict

Premises used: MeasureTheory.ae_imp_of_ae_restrict
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
x : α
hx : t' x = t x
⊢ x ∈ t' ↔ x ∈ t

Tactic:
simpa using hx
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ t' x = t x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t' ↔ x ∈ t) x} x}
      a
h₂ h₃ : ∀ (x : α) (hx : t' x = t x), x ∈ t' ↔ x ∈ t
⊢ ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t' ↔ x ∈ t

Tactic:
filter_upwards [t't] with x hx using by simpa using hx