awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
this : AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : AEMeasurable (_root_.id ∘ f) μ), AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this

Premises used: Function.RightInverse.comp_eq_id, Set.rightInverse_rangeSplitting, MeasurableEmbedding.injective
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
suffices : AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ
⊢ AEMeasurable f μ

Tactic:
suffices AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ by
    rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
⊢ AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ

Tactic:
hg.measurable_rangeSplitting.comp_aemeasurable H.subtype_mk

Premises used: MeasurableEmbedding.measurable_rangeSplitting, Classical.choose, Measurable.comp_aemeasurable, Set.rangeSplitting, AEMeasurable.subtype_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
⊢ AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ

Tactic:
exact hg.measurable_rangeSplitting.comp_aemeasurable H.subtype_mk

Premises used: MeasurableEmbedding.measurable_rangeSplitting, Measurable.comp_aemeasurable, AEMeasurable.subtype_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
s : Set α
hs : MeasurableSet s
μ : Measure α
f : α → β
rw :
  AEMeasurable (_m := m0) f
      (Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)) ↔
    AEMeasurable (α := (↑s : Type u_2)) (_m := Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)
rw₁ rw₂ :
  AEMeasurable (α := { x : α // x ∈ s }) (_m := Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ) ↔
    AEMeasurable (α := (↑s : Type u_2)) (_m := Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)
⊢ AEMeasurable f (μ.restrict s) ↔
    AEMeasurable (α := (↑s : Type u_2)) (_m := Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)

Tactic:
rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).aemeasurable_map_iff]

Premises used: map_comap_subtype_coe, MeasurableEmbedding.subtype_coe, MeasurableEmbedding.aemeasurable_map_iff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : One β
⊢ AEMeasurable.{u_2, u_3} (β := β) (fun (x : α) ↦ 1) μ

Tactic:
measurable_one.aemeasurable

Premises used: Measurable.aemeasurable, measurable_one
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
c : ℝ≥0∞
hc : c ≠ 0
⊢ AEMeasurable f (c • μ) ↔ AEMeasurable f μ

Tactic:
⟨fun h => ⟨h.mk f, h.measurable_mk, (ae_ennreal_smul_measure_iff hc).1 h.ae_eq_mk⟩, fun h =>
    ⟨h.mk f, h.measurable_mk, (ae_ennreal_smul_measure_iff hc).2 h.ae_eq_mk⟩⟩

Premises used: Iff.mpr, AEMeasurable.mk, MeasureTheory.Measure.ae_ennreal_smul_measure_iff, And.intro, Iff.intro, Exists.intro, Iff.mp, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
β : Type u_3
inst : MeasurableSpace β
α : Type u_7
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → β
hf : AEMeasurable f (μ.trim hm)
⊢ AEMeasurable f μ

Tactic:
⟨hf.mk f, Measurable.mono hf.measurable_mk hm le_rfl, ae_eq_of_ae_eq_trim hf.ae_eq_mk⟩

Premises used: le_rfl, AEMeasurable, AEMeasurable.mk, MeasureTheory.ae_eq_of_ae_eq_trim, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, Measurable.mono, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
s : Set α
hs : MeasurableSet s
hf : Measurable.{u_2, u_3} (β := β) fun (x : (↑s : Type u_2)) ↦ f (↑x : α)
⊢ AEMeasurable f (μ.restrict s)

Tactic:
(aemeasurable_restrict_iff_comap_subtype hs).2 hf.aemeasurable

Premises used: Iff.mpr, Measurable.aemeasurable, aemeasurable_restrict_iff_comap_subtype
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ : Measure α
e : α ≃ᵐ β
f : β → γ
⊢ AEMeasurable (_m := inst) f (Measure.map (⇑e : (a : α) → β) μ) ↔ AEMeasurable (f ∘ (⇑e : (a : α) → β)) μ

Tactic:
e.measurableEmbedding.aemeasurable_map_iff

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.aemeasurable_map_iff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
hfm : AEMeasurable f μ
s : Set α
⊢ AEMeasurable f (μ.restrict s)

Tactic:
⟨AEMeasurable.mk f hfm, hfm.measurable_mk, ae_restrict_of_ae hfm.ae_eq_mk⟩

Premises used: AEMeasurable, AEMeasurable.mk, MeasureTheory.ae_restrict_of_ae, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
⊢ Nonempty α

Tactic:
haveI : Nonempty α := ⟨x⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
obtain : ∀ (u : ℕ → α) (hu_tendsto : Tendsto u atTop atTop), AEMeasurable g (μ.restrict (Ioi x))
⊢ AEMeasurable g (μ.restrict (Ioi x))

Tactic:
obtain ⟨u, hu_tendsto⟩ := exists_seq_tendsto (atTop : Filter α)

Premises used: Filter.atTop, Filter.exists_seq_tendsto
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
rw : ∀ (x_1 : α), x < x_1 → ∃ (i : ℕ), x_1 ≤ u i
⊢ Ioi x = ⋃ (n : ℕ), Ioc x (u n)

Tactic:
rw [iUnion_Ioc_eq_Ioi_self_iff.mpr _]

Premises used: Iff.mpr, Set.iUnion_Ioc_eq_Ioi_self_iff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ ∀ (x_1 : α), x < x_1 → ∃ (i : ℕ), x_1 ≤ u i

Tactic:
fun y _ => (hu_tendsto.eventually (eventually_ge_atTop y)).exists

Premises used: Filter.Eventually.exists, Filter.Tendsto.eventually, Filter.eventually_ge_atTop
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ ∀ (x_1 : α), x < x_1 → ∃ (i : ℕ), x_1 ≤ u i

Tactic:
exact fun y _ => (hu_tendsto.eventually (eventually_ge_atTop y)).exists

Premises used: Filter.Eventually.exists, Filter.Tendsto.eventually, Filter.eventually_ge_atTop
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ Ioi x = ⋃ (n : ℕ), Ioc x (u n)

Tactic:
have Ioi_eq_iUnion : Ioi x = ⋃ n : ℕ, Ioc x (u n) := by
    rw [iUnion_Ioc_eq_Ioi_self_iff.mpr _]
    exact fun y _ => (hu_tendsto.eventually (eventually_ge_atTop y)).exists
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
rw : ∀ (i : ℕ), AEMeasurable g (μ.restrict (Ioc x (u i)))
⊢ AEMeasurable g (μ.restrict (Ioi x))

Tactic:
rw [Ioi_eq_iUnion, aemeasurable_iUnion_iff]

Premises used: aemeasurable_iUnion_iff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
inl : ∀ (h : x < u n), AEMeasurable g (μ.restrict (Ioc x (u n)))
inr : ∀ (h : u n ≤ x), AEMeasurable g (μ.restrict (Ioc x (u n)))
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))

Tactic:
rcases lt_or_ge x (u n) with h | h

Premises used: lt_or_ge
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : x < u n
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))

Tactic:
g_meas (u n) h
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : x < u n
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))

Tactic:
exact g_meas (u n) h
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : u n ≤ x
inr : AEMeasurable (_m := m0) g 0
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))

Tactic:
rw [Ioc_eq_empty (not_lt.mpr h), Measure.restrict_empty]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_empty, Set.Ioc_eq_empty, not_lt
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable (_m := m0) g 0

Tactic:
aemeasurable_zero_measure

Premises used: aemeasurable_zero_measure
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable (_m := m0) g 0

Tactic:
exact aemeasurable_zero_measure

Premises used: aemeasurable_zero_measure
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
mp : AEMeasurable (s.indicator f) μ → AEMeasurable f (μ.restrict s)
mpr : AEMeasurable f (μ.restrict s) → AEMeasurable (s.indicator f) μ
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable (s.indicator f) μ
⊢ AEMeasurable f (μ.restrict s)

Tactic:
(h.mono_measure Measure.restrict_le_self).congr (indicator_ae_eq_restrict hs)

Premises used: AEMeasurable.congr, MeasureTheory.Measure.restrict_le_self, AEMeasurable.mono_measure, indicator_ae_eq_restrict
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable (s.indicator f) μ
⊢ AEMeasurable f (μ.restrict s)

Tactic:
exact (h.mono_measure Measure.restrict_le_self).congr (indicator_ae_eq_restrict hs)

Premises used: AEMeasurable.congr, MeasureTheory.Measure.restrict_le_self, AEMeasurable.mono_measure, indicator_ae_eq_restrict
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
⊢ AEMeasurable (s.indicator f) μ

Tactic:
⟨indicator s (h.mk f), h.measurable_mk.indicator hs, ?_⟩

Premises used: AEMeasurable, Set.indicator, Measurable.indicator, AEMeasurable.mk, And.intro, Exists.intro, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
mpr : s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)
⊢ AEMeasurable (s.indicator f) μ

Tactic:
refine ⟨indicator s (h.mk f), h.measurable_mk.indicator hs, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
⊢ s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEMeasurable.mk f h)

Tactic:
have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (AEMeasurable.mk f h) :=
      (indicator_ae_eq_restrict hs).trans (h.ae_eq_mk.trans <| (indicator_ae_eq_restrict hs).symm)
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae (μ.restrict sᶜ)] s.indicator (AEMeasurable.mk f h)

Tactic:
have B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (AEMeasurable.mk f h) :=
      (indicator_ae_eq_restrict_compl hs).trans (indicator_ae_eq_restrict_compl hs).symm
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEMeasurable.mk f h)
B : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] s.indicator (AEMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)

Tactic:
ae_of_ae_restrict_of_ae_restrict_compl _ A B

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEMeasurable.mk f h)
B : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] s.indicator (AEMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)

Tactic:
exact ae_of_ae_restrict_of_ae_restrict_compl _ A B

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : NullMeasurableSet s μ
rcases :
  ∀ (t : Set α) (ht : MeasurableSet t) (hst : s =ᶠ[ae μ] t),
    AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)

Tactic:
rcases hs with ⟨t, ht, hst⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s t : Set α
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
rw : AEMeasurable (t.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
rw₁ : AEMeasurable f (μ.restrict t) ↔ AEMeasurable f (μ.restrict s)
rw₂ rw₃ : AEMeasurable f (μ.restrict t) ↔ AEMeasurable f (μ.restrict t)
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)

Tactic:
rw [← aemeasurable_congr (indicator_ae_eq_of_ae_eq_set hst.symm), aemeasurable_indicator_iff ht,
      restrict_congr_set hst]

Premises used: MeasureTheory.Measure.restrict_congr_set, indicator_ae_eq_of_ae_eq_set, aemeasurable_congr, aemeasurable_indicator_iff, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : Zero β
s : Set α
inst_2 : MeasurableSingletonClass β
b : β
inst_3 : NeZero b
mp : AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ → NullMeasurableSet s μ
mpr : NullMeasurableSet s μ → AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ
⊢ AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ ↔ NullMeasurableSet s μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : Zero β
s : Set α
inst_2 : MeasurableSingletonClass β
b : β
inst_3 : NeZero b
h : AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ
⊢ NullMeasurableSet (preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ) μ

Tactic:
h.nullMeasurable (MeasurableSet.singleton (0 : β)).compl

Premises used: AEMeasurable.nullMeasurable, MeasurableSet.singleton, MeasurableSet.compl, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : Zero β
s : Set α
inst_2 : MeasurableSingletonClass β
b : β
inst_3 : NeZero b
h : AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ
h₁ : s = preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ
⊢ NullMeasurableSet s μ

Tactic:
convert! h.nullMeasurable (MeasurableSet.singleton (0 : β)).compl

Premises used: AEMeasurable.nullMeasurable, MeasurableSet.singleton, MeasurableSet.compl, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : Zero β
s : Set α
inst_2 : MeasurableSingletonClass β
b : β
inst_3 : NeZero b
h : AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ
h₁ : s = (if Membership.mem (γ := Set β) {0}ᶜ b then s else ∅) ∪ if Membership.mem (γ := Set β) {0}ᶜ 0 then sᶜ else ∅
⊢ s = preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ

Tactic:
rw [indicator_const_preimage_eq_union s {0}ᶜ b]

Premises used: Compl.compl, Set.indicator_const_preimage_eq_union, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : Zero β
s : Set α
inst_2 : MeasurableSingletonClass β
b : β
inst_3 : NeZero b
h : AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ
⊢ s = (if Membership.mem (γ := Set β) {0}ᶜ b then s else ∅) ∪ if Membership.mem (γ := Set β) {0}ᶜ 0 then sᶜ else ∅

Tactic:
simp [NeZero.ne b]

Premises used: NeZero.ne
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : Zero β
s : Set α
inst_2 : MeasurableSingletonClass β
b : β
inst_3 : NeZero b
h : NullMeasurableSet s μ
⊢ AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ

Tactic:
(aemeasurable_indicator_iff₀ h).mpr aemeasurable_const

Premises used: Iff.mpr, aemeasurable_indicator_iff₀, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : Zero β
s : Set α
inst_2 : MeasurableSingletonClass β
b : β
inst_3 : NeZero b
h : NullMeasurableSet s μ
⊢ AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ

Tactic:
exact (aemeasurable_indicator_iff₀ h).mpr aemeasurable_const

Premises used: Iff.mpr, aemeasurable_indicator_iff₀, aemeasurable_const