awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∃ (i : ι), x ∉ s i
refine_2 : (∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i) → f x ∈ t
refine_2₁ : f x ∈ t → ∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i
⊢ (∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i) ↔ f x ∈ t

Tactic:
constructor
-- 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 : ∃ (i : ι), x ∉ s i
i : ι
hxt : mk f ⋯ x ∈ t
hxs : x ∉ s i
refine_2 refine_2₁ refine_2₂ refine_2₃ : mk f ⋯ x ∈ t
⊢ f x ∈ t

Tactic:
rwa [hs _ _ hxs]
-- 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 : ∃ (i : ι), x ∉ s i
refine_2 : ∀ (i : ι) (hi : x ∉ s i), f x ∈ t → ∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i
⊢ f x ∈ t → ∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i

Tactic:
rcases hx with ⟨i, hi⟩
-- 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 : α
i : ι
hi : x ∉ s i
refine_2 : mk f ⋯ x ∈ t → ∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i
⊢ f x ∈ t → ∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i

Tactic:
rw [hs _ _ hi]
-- 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 : α
i : ι
hi : x ∉ s i
⊢ mk f ⋯ x ∈ t → ∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i

Tactic:
fun h => ⟨i, h, hi⟩

Premises used: And.intro, Exists.intro
-- 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 : α
i : ι
hi : x ∉ s i
⊢ mk f ⋯ x ∈ t → ∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i

Tactic:
exact fun h => ⟨i, h, hi⟩
-- 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
i : ι
⊢ ∀ᵐ (x : α) ∂μ i, f x = g x

Tactic:
measure_mono_null (fun x (hx : f x ≠ g x) => ?_) (hsμ i)

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.measure_mono_null
-- 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
i : ι
refine_3 : ∀ (x : α) (hx : f x ≠ g x), x ∈ s i
⊢ ∀ᵐ (x : α) ∂μ i, f x = g x

Tactic:
refine measure_mono_null (fun x (hx : f x ≠ g x) => ?_) (hsμ i)

Premises used: MeasureTheory.measure_mono_null
-- 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
i : ι
x : α
hx : f x ≠ g x
refine_3 : ∀ (hx : x ∉ s i), f x = g x
⊢ x ∈ s i

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)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : x ∉ s i
⊢ f x = g x

Tactic:
(piecewise_eq_of_notMem _ _ _ ?_).symm

Premises used: Set.piecewise_eq_of_notMem, Eq.symm
-- 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
i : ι
x : α
hx : x ∉ s i
refine_3 : x ∉ ⋂ (i : ι), s i
⊢ f x = g x

Tactic:
refine (piecewise_eq_of_notMem _ _ _ ?_).symm

Premises used: Set.piecewise_eq_of_notMem, Eq.symm
-- 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
i : ι
x : α
hx : x ∉ s i
⊢ x ∉ ⋂ (i : ι), s i

Tactic:
fun h => hx (mem_iInter.1 h i)

Premises used: Set.mem_iInter, Iff.mp, Not
-- 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
i : ι
x : α
hx : x ∉ s i
⊢ x ∉ ⋂ (i : ι), s i

Tactic:
exact fun h => hx (mem_iInter.1 h i)

Premises used: Set.mem_iInter, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
⊢ AEMeasurable f (sum μ) ↔ ∀ (i : ι), AEMeasurable f (μ i)

Tactic:
⟨fun h _ => h.mono_measure (le_sum _ _), sum_measure⟩

Premises used: AEMeasurable.sum_measure, AEMeasurable.mono_measure, MeasureTheory.Measure.le_sum, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ ν : Measure α
rw :
  AEMeasurable f (bif true then μ else ν) ∧ AEMeasurable f (bif false then μ else ν) ↔
    AEMeasurable f μ ∧ AEMeasurable f ν
⊢ AEMeasurable f (μ + ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν

Tactic:
rw [← sum_cond, aemeasurable_sum_measure_iff, Bool.forall_bool, and_comm]

Premises used: Bool.forall_bool, MeasureTheory.Measure.sum_cond, and_comm, aemeasurable_sum_measure_iff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ ν : Measure α
⊢ AEMeasurable f (bif true then μ else ν) ∧ AEMeasurable f (bif false then μ else ν) ↔
    AEMeasurable f μ ∧ AEMeasurable f ν

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
f : α → β
hμ : AEMeasurable f μ
hν : AEMeasurable f ν
⊢ AEMeasurable f (μ + ν)

Tactic:
aemeasurable_add_measure_iff.2 ⟨hμ, hν⟩

Premises used: Iff.mpr, And.intro, aemeasurable_add_measure_iff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
f : α → β
hμ : AEMeasurable f μ
hν : AEMeasurable f ν
h :
  ∀ (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((Measure.map f (μ + ν) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        ((HAdd.hAdd (α := Measure β) (Measure.map f μ) (Measure.map f ν) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Measure.map f (μ + ν) = HAdd.hAdd (α := Measure β) (Measure.map f μ) (Measure.map f ν)

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
f : α → β
hμ : AEMeasurable f μ
hν : AEMeasurable f ν
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (μ + ν) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((HAdd.hAdd (α := Measure β) (Measure.map f μ) (Measure.map f ν) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Countable ι
s : ι → Set α
h : ∀ (i : ι), AEMeasurable f (μ.restrict (s i))
⊢ AEMeasurable f (μ.restrict (⋃ (i : ι), s i))

Tactic:
(sum_measure h).mono_measure <| restrict_iUnion_le

Premises used: AEMeasurable.sum_measure, AEMeasurable.mono_measure, MeasureTheory.Measure.restrict_iUnion_le
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Countable ι
s : ι → Set α
⊢ AEMeasurable f (μ.restrict (⋃ (i : ι), s i)) ↔ ∀ (i : ι), AEMeasurable f (μ.restrict (s i))

Tactic:
⟨fun h _ => h.mono_measure <| restrict_mono (subset_iUnion _ _) le_rfl, AEMeasurable.iUnion⟩

Premises used: le_rfl, AEMeasurable.iUnion, MeasureTheory.Measure.restrict_mono, Set.subset_iUnion, AEMeasurable.mono_measure, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
s t : Set α
⊢ AEMeasurable f (μ.restrict (s ∪ t)) ↔ AEMeasurable f (μ.restrict s) ∧ AEMeasurable f (μ.restrict t)

Tactic:
simp only [union_eq_iUnion, aemeasurable_iUnion_iff, Bool.forall_bool, cond, and_comm]

Premises used: cond, Bool.forall_bool, and_comm, aemeasurable_iUnion_iff, Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
R : Type u_6
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : AEMeasurable f μ
c : R
⊢ AEMeasurable f (c • μ)

Tactic:
⟨h.mk f, h.measurable_mk, ae_smul_measure h.ae_eq_mk c⟩

Premises used: AEMeasurable, AEMeasurable.mk, MeasureTheory.Measure.ae_smul_measure, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace δ
μ : Measure α
f : α → δ
g : δ → β
hg : AEMeasurable (_m := inst_1) g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ AEMeasurable (g ∘ f) μ

Tactic:
⟨hg.mk g ∘ hf.mk f, hg.measurable_mk.comp hf.measurable_mk,
    (ae_eq_comp hf hg.ae_eq_mk).trans (hf.ae_eq_mk.fun_comp (mk g hg))⟩

Premises used: Filter.EventuallyEq.trans, AEMeasurable, Measurable.comp, Function.comp, AEMeasurable.mk, And.intro, Exists.intro, MeasureTheory.ae_eq_comp, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.fun_comp, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace δ
μ : Measure α
f : α → δ
g : δ → β
hg : AEMeasurable (_m := inst_1) g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ AEMeasurable.{u_2, u_3} (β := β) (fun (x : α) ↦ g (f x)) μ

Tactic:
comp_aemeasurable hg hf

Premises used: AEMeasurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace δ
μ : Measure α
f : α → δ
g : δ → β
hg : AEMeasurable (_m := inst_1) g (Measure.map f μ)
hf : Measurable f
⊢ AEMeasurable (g ∘ f) μ

Tactic:
hg.comp_aemeasurable hf.aemeasurable

Premises used: Measurable.aemeasurable, AEMeasurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace δ
μ : Measure α
ν : Measure δ
f : α → δ
g : δ → β
hg : AEMeasurable g ν
hf : QuasiMeasurePreserving f μ ν
⊢ AEMeasurable (g ∘ f) μ

Tactic:
(hg.mono' hf.absolutelyContinuous).comp_measurable hf.measurable

Premises used: AEMeasurable.comp_measurable, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.QuasiMeasurePreserving.measurable, AEMeasurable.mono'
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable (_m := inst) g (Measure.map f μ)
hf : AEMeasurable f μ
h :
  ∀ (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((Measure.map g (Measure.map f μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure γ) (Measure.map g (Measure.map f μ)) (Measure.map (g ∘ f) μ)

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable (_m := inst) g (Measure.map f μ)
hf : AEMeasurable f μ
s : Set γ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' g ⁻¹' s) : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' g ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (g ∘ f ⁻¹' s) : ℝ≥0∞)
h₃ h₄ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' g ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' g ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map g (Measure.map f μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply_of_aemeasurable hg hs, map_apply₀ hf (hg.nullMeasurable hs),
    map_apply_of_aemeasurable (hg.comp_aemeasurable hf) hs, preimage_comp]

Premises used: AEMeasurable.nullMeasurable, Set.preimage_comp, MeasureTheory.Measure.map_apply_of_aemeasurable, MeasureTheory.Measure.map_apply₀, AEMeasurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ : Measure α
f : α → β × γ
hf : AEMeasurable f μ
⊢ AEMeasurable.{u_2, u_3} (β := β) (fun (x : α) ↦ (f x).1) μ

Tactic:
measurable_fst.comp_aemeasurable hf

Premises used: Measurable.comp_aemeasurable, measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ : Measure α
f : α → β × γ
hf : AEMeasurable f μ
⊢ AEMeasurable.{u_2, u_4} (β := γ) (fun (x : α) ↦ (f x).2) μ

Tactic:
measurable_snd.comp_aemeasurable hf

Premises used: measurable_snd, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ : Measure α
f : α → β
g : α → γ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (β := β × γ) (fun (x : α) ↦ (f x, g x)) μ

Tactic:
⟨fun a => (hf.mk f a, hg.mk g a), hf.measurable_mk.prodMk hg.measurable_mk,
    hf.ae_eq_mk.prodMk hg.ae_eq_mk⟩

Premises used: AEMeasurable, AEMeasurable.mk, Measurable.prodMk, Prod.mk, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.prodMk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : MeasurableEq β
f g : α → β
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ NullMeasurableSet {x : α | f x = g x} μ

Tactic:
(hf.prodMk hg).nullMeasurableSet_preimage measurableSet_diagonal

Premises used: Set.Mem, setOf, AEMeasurable.nullMeasurableSet_preimage, Set.diagonal, MeasurableEq.measurableSet_diagonal, Set.preimage, AEMeasurable.prodMk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
⊢ ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g

Tactic:
⟨g, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
refine_1 : Measurable g
refine_2 : range g ⊆ t
refine_3 : f =ᶠ[ae μ] g
⊢ ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g

Tactic:
refine ⟨g, ?_, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
⊢ Measurable g

Tactic:
Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk

Premises used: Measurable.piecewise, MeasureTheory.measurableSet_toMeasurable, measurable_const, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
⊢ Measurable g

Tactic:
exact Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk

Premises used: Measurable.piecewise, MeasureTheory.measurableSet_toMeasurable, measurable_const, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
x : α
pos : ∀ (hx : x ∈ s), g x ∈ t
neg : ∀ (hx : x ∉ s), g x ∈ t
⊢ g x ∈ t

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
x : α
hx : x ∈ s
⊢ g x ∈ t

Tactic:
simpa [g, hx] using h₀.some_mem

Premises used: Set.Nonempty.some_mem