awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ AEDisjoint μ s t

Tactic:
measure_mono_null inter_subset_right h

Premises used: MeasureTheory.measure_mono_null, MeasureTheory.AEDisjoint, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ AEDisjoint μ s t

Tactic:
AEDisjoint.symm (of_null_right h)

Premises used: MeasureTheory.AEDisjoint.symm, MeasureTheory.AEDisjoint.of_null_right
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set α
⊢ AEDisjoint μ sᶜ s

Tactic:
(@disjoint_compl_left _ _ s).aedisjoint

Premises used: disjoint_compl_left, Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.AEDisjoint
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set α
⊢ AEDisjoint μ s sᶜ

Tactic:
(@disjoint_compl_right _ _ s).aedisjoint

Premises used: Disjoint.aedisjoint, disjoint_compl_right
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Subsingleton α
⊢ AEMeasurable f μ

Tactic:
Subsingleton.measurable.aemeasurable

Premises used: Measurable.aemeasurable, Subsingleton.measurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Subsingleton β
⊢ AEMeasurable f μ

Tactic:
(measurable_of_subsingleton_codomain f).aemeasurable

Premises used: Measurable.aemeasurable, measurable_of_subsingleton_codomain
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
h : Nontrivial α
inhabit : ∀ (inhabited_h : Inhabited α), AEMeasurable (_m := m0) f 0
⊢ AEMeasurable (_m := m0) f 0

Tactic:
inhabit α
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
h : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable (_m := m0) f 0

Tactic:
⟨fun _ => f default, measurable_const, rfl⟩

Premises used: Inhabited.default, AEMeasurable, And.intro, Exists.intro, measurable_const, rfl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
h : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable (_m := m0) f 0

Tactic:
exact ⟨fun _ => f default, measurable_const, rfl⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
m : MeasurableSpace α
hm : m ≤ m0
⊢ AEMeasurable id μ

Tactic:
@Measurable.aemeasurable α α m0 m id μ (measurable_id'' hm)

Premises used: Measurable.aemeasurable, measurable_id''
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
h : NeZero (R := Measure β) (Measure.map f μ)
by_contra : ∀ (h' : ¬AEMeasurable f μ), False
⊢ AEMeasurable f μ

Tactic:
by_contra h'
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
h : NeZero (R := Measure β) (Measure.map f μ)
h' : ¬AEMeasurable f μ
⊢ False

Tactic:
simp [h'] at h
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : AEMeasurable f ν
hμν : μ ≪ ν
⊢ AEMeasurable f μ

Tactic:
⟨hf.mk f, hf.measurable_mk, hμν.ae_le hf.ae_eq_mk⟩

Premises used: AEMeasurable, AEMeasurable.mk, MeasureTheory.Measure.AbsolutelyContinuous.ae_le, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ ν : Measure α
h : AEMeasurable f μ
h' : ν ≤ μ
⊢ AEMeasurable f ν

Tactic:
mono_ac h h'.absolutelyContinuous

Premises used: LE.le.absolutelyContinuous, AEMeasurable.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
s t : Set α
h : s ⊆ t
ht : AEMeasurable f (μ.restrict t)
⊢ AEMeasurable f (μ.restrict s)

Tactic:
ht.mono_measure (restrict_mono h le_rfl)

Premises used: le_rfl, MeasureTheory.Measure.restrict_mono, AEMeasurable.mono_measure
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ ν : Measure α
h : AEMeasurable f μ
h' : ν ≪ μ
⊢ AEMeasurable f ν

Tactic:
⟨h.mk f, h.measurable_mk, h' h.ae_eq_mk⟩

Premises used: AEMeasurable, AEMeasurable.mk, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
s : Set α
h : AEMeasurable f (μ.restrict s)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = mk f h x

Tactic:
ae_imp_of_ae_restrict h.ae_eq_mk

Premises used: MeasureTheory.ae_imp_of_ae_restrict, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
s : Set α
h : AEMeasurable f (μ.restrict s)
⊢ f =ᶠ[ae μ ⊓ 𝓟 s] mk f h

Tactic:
le_ae_restrict h.ae_eq_mk

Premises used: Filter.Eventually, Filter.EventuallyEq, MeasureTheory.le_ae_restrict, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
⊢ Nontrivial β

Tactic:
nontriviality β
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabit : ∀ (inhabited_h : Inhabited β), AEMeasurable f (sum μ)
⊢ AEMeasurable f (sum μ)

Tactic:
inhabit β
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
i : ι
rw : Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) {x : α | f x ≠ mk f ⋯ x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
i : ι
⊢ Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) {x : α | f x ≠ mk f ⋯ x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(h i).ae_eq_mk

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
i : ι
⊢ Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) {x : α | f x ≠ mk f ⋯ x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact (h i).ae_eq_mk

Premises used: AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
⊢ ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have hsμ : ∀ i, μ i (s i) = 0 := by
    intro i
    rw [measure_toMeasurable]
    exact (h i).ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)

Tactic:
have hsm : MeasurableSet (⋂ i, s i) :=
    MeasurableSet.iInter fun i => measurableSet_toMeasurable _ _
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
i : ι
x : α
hx : x ∉ s i
contrapose! : ∀ (hx : f x ≠ mk f ⋯ x), x ∈ s i
⊢ f x = mk f ⋯ x

Tactic:
contrapose! hx
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
i : ι
x : α
hx : f x ≠ mk f ⋯ x
⊢ x ∈ s i

Tactic:
subset_toMeasurable _ _ hx

Premises used: Set.Mem, MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
i : ι
x : α
hx : f x ≠ mk f ⋯ x
⊢ x ∈ s i

Tactic:
exact subset_toMeasurable _ _ hx

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
⊢ ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x

Tactic:
have hs : ∀ i x, x ∉ s i → f x = (h i).mk f x := by
    intro i x hx
    contrapose! hx
    exact subset_toMeasurable _ _ hx
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
⊢ AEMeasurable f (sum μ)

Tactic:
⟨g, measurable_of_restrict_of_restrict_compl hsm ?_ ?_, ae_sum_iff.mpr fun i => ?_⟩

Premises used: Iff.mpr, AEMeasurable, MeasureTheory.Measure.ae_sum_iff, And.intro, Exists.intro, measurable_of_restrict_of_restrict_compl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
refine_1 : Measurable (α := (↑(⋂ (i : ι), s i) : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i) g)
refine_2 : Measurable (α := (↑(⋂ (i : ι), s i)ᶜ : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i)ᶜ g)
refine_3 : ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, f x = g x
⊢ AEMeasurable f (sum μ)

Tactic:
refine ⟨g, measurable_of_restrict_of_restrict_compl hsm ?_ ?_, ae_sum_iff.mpr fun i => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
refine_1 :
  Measurable.{u_2, u_3} (α := (↑(⋂ (i : ι), s i) : Type u_2)) (β := β)
    (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default))
⊢ Measurable (α := (↑(⋂ (i : ι), s i) : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i) g)

Tactic:
rw [restrict_piecewise]

Premises used: Set.restrict_piecewise
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
refine_1 :
  Measurable.{u_2, u_3} (α := (↑(⋂ (i : ι), toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}) : Type u_2)) (β := β)
    (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}) (const α default))
⊢ Measurable.{u_2, u_3} (α := (↑(⋂ (i : ι), s i) : Type u_2)) (β := β)
    (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default))

Tactic:
simp only [s]
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
⊢ Measurable.{u_2, u_3} (α := (↑(⋂ (i : ι), toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}) : Type u_2)) (β := β)
    (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}) (const α default))

Tactic:
measurable_const

Premises used: measurable_const, Set.restrict
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
⊢ Measurable.{u_2, u_3} (α := (↑(⋂ (i : ι), toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}) : Type u_2)) (β := β)
    (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}) (const α default))

Tactic:
exact measurable_const

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
refine_2 :
  Measurable (α := (↑(⋃ (i : ι), (s i)ᶜ) : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f)
⊢ Measurable (α := (↑(⋂ (i : ι), s i)ᶜ : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i)ᶜ g)

Tactic:
rw [restrict_piecewise_compl, compl_iInter]

Premises used: Set.compl_iInter, Set.restrict_piecewise_compl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (α := (↑(⋃ (i : ι), (s i)ᶜ) : Type u_2))
    (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)

Tactic:
⟨⋃ i, (h i).mk f ⁻¹' t ∩ (s i)ᶜ, MeasurableSet.iUnion fun i ↦
      (measurable_mk _ ht).inter (measurableSet_toMeasurable _ _).compl, ?_⟩

Premises used: MeasurableSet, Compl.compl, setOf, AEMeasurable.mk, Ne, MeasurableSet.compl, Inter.inter, MeasureTheory.measurableSet_toMeasurable, Set.preimage, And.intro, Exists.intro, MeasurableSet.iUnion, Set.iUnion, AEMeasurable.measurable_mk, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
refine_2 :
  Eq (α := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
    (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) ⁻¹'
      ⋃ (i : ι), mk f ⋯ ⁻¹' t ∩ (s i)ᶜ)
    (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)
⊢ MeasurableSet (α := (↑(⋃ (i : ι), (s i)ᶜ) : Type u_2))
    (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)

Tactic:
refine ⟨⋃ i, (h i).mk f ⁻¹' t ∩ (s i)ᶜ, MeasurableSet.iUnion fun i ↦
      (measurable_mk _ ht).inter (measurableSet_toMeasurable _ _).compl, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
refine_2 :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x),
    Membership.mem (γ := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
        (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) ⁻¹'
          ⋃ (i : ι), mk f ⋯ ⁻¹' t ∩ (s i)ᶜ)
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) x hx) ↔
      Membership.mem (γ := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
        (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) x hx)
⊢ Eq (α := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
    (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) ⁻¹'
      ⋃ (i : ι), mk f ⋯ ⁻¹' t ∩ (s i)ᶜ)
    (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
h_1 : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x
refine_2 : ∀ (hx : ∃ (i : ι), x ∉ s i), (∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i) ↔ f x ∈ t
⊢ Membership.mem (γ := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
      (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) ⁻¹'
        ⋃ (i : ι), mk f ⋯ ⁻¹' t ∩ (s i)ᶜ)
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) x hx) ↔
    Membership.mem (γ := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
      (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) x hx)

Tactic:
simp only [mem_preimage, mem_iUnion, Set.restrict, mem_inter_iff,
      mem_compl_iff] at hx ⊢

Premises used: Set.mem_inter_iff, Set.mem_iUnion, Set.restrict, Set.mem_compl_iff, Set.mem_preimage