awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) μ
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) μ
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) μ
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) μ
mp₄ : ∀ (h : AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ), NullMeasurableSet s μ
mpr₄ mpr₅ : ∀ (h : 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:
classical
  constructor <;> intro h
  · convert! h.nullMeasurable (MeasurableSet.singleton (0 : β)).compl
    rw [indicator_const_preimage_eq_union s {0}ᶜ b]
    simp [NeZero.ne b]
  · exact (aemeasurable_indicator_iff₀ h).mpr aemeasurable_const

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

Tactic:
(aemeasurable_indicator_iff hs).mpr hfm.restrict

Premises used: Iff.mpr, AEMeasurable.restrict, aemeasurable_indicator_iff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
hfm : AEMeasurable f μ
s : Set α
hs : NullMeasurableSet s μ
⊢ AEMeasurable (s.indicator f) μ

Tactic:
(aemeasurable_indicator_iff₀ hs).mpr hfm.restrict

Premises used: Iff.mpr, AEMeasurable.restrict, aemeasurable_indicator_iff₀
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
e_μ : Eq (α := Measure δ) (map f μ) (map (AEMeasurable.mk f hf) μ)
⊢ Eq (α := Measure δ) (restrict (map f μ) s) (restrict (map (AEMeasurable.mk f hf) μ) s)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ Eq (α := Measure δ) (map f μ) (map (AEMeasurable.mk f hf) μ)

Tactic:
apply Measure.map_congr hf.ae_eq_mk

Premises used: MeasureTheory.Measure.map_congr, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
h : μ.restrict (AEMeasurable.mk f hf ⁻¹' s) = μ.restrict (f ⁻¹' s)
⊢ Eq (α := Measure δ) (map f (μ.restrict (AEMeasurable.mk f hf ⁻¹' s))) (map f (μ.restrict (f ⁻¹' s)))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
h :
  ∀ (t : Set α) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞) ((μ.restrict (AEMeasurable.mk f hf ⁻¹' s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      ((μ.restrict (f ⁻¹' s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ μ.restrict (AEMeasurable.mk f hf ⁻¹' s) = μ.restrict (f ⁻¹' s)

Tactic:
ext1 t ht
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ AEMeasurable.mk f hf ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (AEMeasurable.mk f hf ⁻¹' s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict (f ⁻¹' s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [ht, Measure.restrict_apply]

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : t ∩ AEMeasurable.mk f hf ⁻¹' s =ᶠ[ae μ] t ∩ f ⁻¹' s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ AEMeasurable.mk f hf ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f ⁻¹' s) : ℝ≥0∞)

Tactic:
apply measure_congr

Premises used: MeasureTheory.measure_congr
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ t ∩ AEMeasurable.mk f hf ⁻¹' s =ᶠ[ae μ] t ∩ f ⁻¹' s

Tactic:
apply (EventuallyEq.refl _ _).inter (hf.ae_eq_mk.symm.preimage s)

Premises used: Filter.EventuallyEq.inter, Filter.EventuallyEq.preimage, Filter.EventuallyEq.refl, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace δ
μ ν : Measure α
f : α → δ
h : μ ≤ ν
hf : AEMeasurable f ν
s : Set δ
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) (((map f μ : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    (((map f ν : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa [hf, hs, hf.mono_measure h] using h (f ⁻¹' s)

Premises used: Set.preimage, AEMeasurable.mono_measure
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
⊢ Nontrivial β

Tactic:
nontriviality β
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
h_1 : Nontrivial β
inhabit : ∀ (inhabited_h : Inhabited β), AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
inhabit β
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
h_1 : Nontrivial β
inhabited_h : Inhabited β
rcases :
  ∀ (S : Set (Set β)) (hSc : S.Countable) [hc : MeasurableSpace.CountablyGenerated β] (h : NullMeasurable f μ),
    AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
rcases hc.1 with ⟨S, hSc, rfl⟩

Premises used: MeasurableSpace.CountablyGenerated.isCountablyGenerated, rfl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
choose! :
  ∀ (T : (s : Set β) → Set α) (hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s)
    (hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)) (hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s),
    AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
choose! T hTf hTm hTeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_subset_ae_eq

Premises used: MeasurableSpace.GenerateMeasurable.basic, MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
choose! :
  ∀ (U : (s : Set β) → Set α) (hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s)
    (hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)) (hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s),
    AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
choose! U hUf hUm hUeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_superset_ae_eq

Premises used: MeasurableSpace.GenerateMeasurable.basic, MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
⊢ MeasurableSet v

Tactic:
have hvm : MeasurableSet v := .biUnion hSc fun s hs ↦ (hUm s hs).diff (hTm s hs)
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have hvμ : μ v = 0 := (measure_biUnion_null_iff hSc).2 fun s hs ↦ ae_le_set.1 <|
    ((hUeq s hs).trans (hTeq s hs).symm).le
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AEMeasurable f μ

Tactic:
⟨v.piecewise (fun _ ↦ default) f, ?_, measure_mono_null (fun x ↦
    not_imp_comm.2 fun hxv ↦ (piecewise_eq_of_notMem _ _ _ hxv).symm) hvμ⟩

Premises used: Iff.mpr, Inhabited.default, Set.piecewise_eq_of_notMem, AEMeasurable, not_imp_comm, MeasureTheory.measure_mono_null, And.intro, Exists.intro, Set.piecewise, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
refine : Measurable (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f)
⊢ AEMeasurable f μ

Tactic:
refine ⟨v.piecewise (fun _ ↦ default) f, ?_, measure_mono_null (fun x ↦
    not_imp_comm.2 fun hxv ↦ (piecewise_eq_of_notMem _ _ _ hxv).symm) hvμ⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Measurable (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f)

Tactic:
measurable_of_restrict_of_restrict_compl hvm ?_ ?_

Premises used: measurable_of_restrict_of_restrict_compl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : Measurable (v.restrict (π := fun (a : α) ↦ β) (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f))
refine_2 :
  Measurable (vᶜ.restrict (π := fun (a : α) ↦ β) (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f))
⊢ Measurable (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f)

Tactic:
refine measurable_of_restrict_of_restrict_compl hvm ?_ ?_

Premises used: measurable_of_restrict_of_restrict_compl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 :
  Measurable.{u_2, u_3} (α := (↑v : Type u_2)) (β := β) (v.restrict (π := fun (a : α) ↦ β) fun (x : α) ↦ default)
⊢ Measurable (v.restrict (π := fun (a : α) ↦ β) (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f))

Tactic:
rw [restrict_piecewise]

Premises used: Set.restrict_piecewise
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Measurable.{u_2, u_3} (α := (↑v : Type u_2)) (β := β) (v.restrict (π := fun (a : α) ↦ β) fun (x : α) ↦ default)

Tactic:
apply measurable_const

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2 : Measurable (α := (↑vᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ))
⊢ Measurable (vᶜ.restrict (π := fun (a : α) ↦ β) (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f))

Tactic:
rw [restrict_piecewise_compl, restrict_eq]

Premises used: Set.restrict_eq, Set.restrict_piecewise_compl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Measurable (α := (↑vᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ))

Tactic:
measurable_generateFrom fun s hs ↦ .of_subtype_image ?_

Premises used: measurable_generateFrom, MeasurableSet.of_subtype_image
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2 :
  ∀ (s : Set β) (hs : s ∈ S),
    MeasurableSet
      (image (α := { x : α // x ∈ vᶜ }) (Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ))
        (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ) ⁻¹' s))
⊢ Measurable (α := (↑vᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ))

Tactic:
refine measurable_generateFrom fun s hs ↦ .of_subtype_image ?_

Premises used: measurable_generateFrom, MeasurableSet.of_subtype_image
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
refine_2 : MeasurableSet (vᶜ ∩ f ⁻¹' s)
⊢ MeasurableSet
    (image (α := { x : α // x ∈ vᶜ }) (Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ) ⁻¹' s))

Tactic:
rw [preimage_comp, Subtype.image_preimage_coe]

Premises used: Subtype.image_preimage_coe, Set.preimage_comp
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
⊢ MeasurableSet (T s \ v)

Tactic:
(hTm s hs).diff hvm

Premises used: MeasurableSet.diff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
h₁ : vᶜ ∩ f ⁻¹' s = T s \ v
⊢ MeasurableSet (vᶜ ∩ f ⁻¹' s)

Tactic:
convert! (hTm s hs).diff hvm using 1

Premises used: MeasurableSet.diff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : (s : Set β) → Set α
hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s
hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)
hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s
U : (s : Set β) → Set α
hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s
hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)
hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
h₁ : f ⁻¹' s ∩ vᶜ = T s \ v
⊢ vᶜ ∩ f ⁻¹' s = T s \ v

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm