awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg : mk f H x ∈ t
⊢ g x ∈ t

Tactic:
simp only [g, hx, piecewise_eq_of_notMem, not_false_iff]

Premises used: Set.piecewise_eq_of_notMem, not_false_iff
-- 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
neg : ∀ (hx : mk f H x ∉ t), x ∈ s
⊢ mk f H x ∈ t

Tactic:
contrapose hx
-- 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 : mk f H x ∉ t
neg : Membership.mem (γ := Set α) {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ x
⊢ x ∈ s

Tactic:
apply subset_toMeasurable

Premises used: MeasureTheory.subset_toMeasurable
-- 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 : mk f H x ∉ t
⊢ Membership.mem (γ := Set α) {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ x

Tactic:
simp +contextual only [hx, mem_compl_iff, mem_setOf_eq, not_and,
        not_false_iff, imp_true_iff]

Premises used: Set.mem_setOf_eq, imp_true_iff, not_false_iff, not_and, Set.mem_compl_iff
-- 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)
rw : {x : α | f x = mk f H x ∧ f x ∈ t} ∈ ae μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]

Premises used: compl_compl, MeasureTheory.measure_toMeasurable, MeasureTheory.compl_mem_ae_iff
-- 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 : α | f x = mk f H x ∧ f x ∈ t} ∈ ae μ

Tactic:
H.ae_eq_mk.and ht

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Eventually.and, AEMeasurable.ae_eq_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 : α | f x = mk f H x ∧ f x ∈ t} ∈ ae μ

Tactic:
exact H.ae_eq_mk.and ht

Premises used: Filter.Eventually.and, AEMeasurable.ae_eq_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)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have A : μ (toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ) = 0 := by
      rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
      exact H.ae_eq_mk.and ht
-- 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)
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
h : ∀ (x : α) (hx : x ∈ (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ)ᶜ), f x = g x
⊢ f =ᶠ[ae μ] g

Tactic:
filter_upwards [compl_mem_ae_iff.2 A] with x hx

Premises used: Iff.mpr, MeasureTheory.compl_mem_ae_iff
-- 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)
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ)ᶜ
⊢ x ∉ toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ

Tactic:
rw [mem_compl_iff] at hx

Premises used: Set.mem_compl_iff
-- 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)
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∉ toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
h : f x = mk f H x
⊢ f x = g x

Tactic:
simp only [s, g, hx, piecewise_eq_of_notMem, not_false_iff]

Premises used: Set.piecewise_eq_of_notMem, not_false_iff
-- 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)
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∉ toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
h : ∀ (hx : f x ≠ mk f H x), x ∈ toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
⊢ f x = mk f H x

Tactic:
contrapose! hx
-- 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)
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : f x ≠ mk f H x
h : Membership.mem (γ := Set α) {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ x
⊢ x ∈ toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ

Tactic:
apply subset_toMeasurable

Premises used: MeasureTheory.subset_toMeasurable
-- 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)
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : f x ≠ mk f H x
⊢ Membership.mem (γ := Set α) {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ x

Tactic:
simp only [hx, mem_compl_iff, mem_setOf_eq, false_and, not_false_iff]

Premises used: false_and, Set.mem_setOf_eq, not_false_iff, Set.mem_compl_iff
-- 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
let let₁ let₂ let₃ : ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
refine_1 :
  let s := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ;
  let g := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H);
  Measurable g
refine_2 :
  let s := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ;
  let g := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H);
  range g ⊆ t
refine_3 :
  let s := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ;
  let g := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H);
  f =ᶠ[ae μ] g
refine_2₁ :
  let s := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ;
  let g := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H);
  range g ⊆ t
refine_3₁ refine_3₂ :
  let s := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ;
  let g := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H);
  f =ᶠ[ae μ] g
⊢ ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g

Tactic:
classical
  let s : Set α := toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ
  let g : α → β := piecewise s (fun _ => h₀.some) (H.mk f)
  refine ⟨g, ?_, ?_, ?_⟩
  · exact Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk
  · rintro _ ⟨x, rfl⟩
    by_cases hx : x ∈ s
    · simpa [g, hx] using h₀.some_mem
    · simp only [g, hx, piecewise_eq_of_notMem, not_false_iff]
      contrapose hx
      apply subset_toMeasurable
      simp +contextual only [hx, mem_compl_iff, mem_setOf_eq, not_and,
        not_false_iff, imp_true_iff]
  · have A : μ (toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ) = 0 := by
      rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
      exact H.ae_eq_mk.and ht
    filter_upwards [compl_mem_ae_iff.2 A] with x hx
    rw [mem_compl_iff] at hx
    simp only [s, g, hx, piecewise_eq_of_notMem, not_false_iff]
    contrapose! hx
    apply subset_toMeasurable
    simp only [hx, mem_compl_iff, mem_setOf_eq, false_and, not_false_iff]

Premises used: Set.piecewise_eq_of_notMem, Measurable.piecewise, false_and, Set.Nonempty.some_mem, Set.mem_setOf_eq, MeasureTheory.subset_toMeasurable, imp_true_iff, MeasureTheory.measurableSet_toMeasurable, measurable_const, not_false_iff, not_and, rfl, Set.mem_compl_iff, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Preorder β
inst_1 : Zero β
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t
obtain :
  ∀ (G : α → β) (hG_meas : Measurable G) (hG_mem : range G ⊆ (Preorder.toLE : LE β).1 0) (hG_ae_eq : f =ᶠ[ae μ] G),
    ∃ (g : α → β), Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g
⊢ ∃ (g : α → β), Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g

Tactic:
obtain ⟨G, hG_meas, hG_mem, hG_ae_eq⟩ := hf.exists_ae_eq_range_subset f_nn ⟨0, le_rfl⟩

Premises used: AEMeasurable.exists_ae_eq_range_subset, le_rfl, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Preorder β
inst_1 : Zero β
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t
G : α → β
hG_meas : Measurable G
hG_mem : range G ⊆ (Preorder.toLE : LE β).1 0
hG_ae_eq : f =ᶠ[ae μ] G
⊢ ∃ (g : α → β), Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g

Tactic:
⟨G, hG_meas, fun x => hG_mem (mem_range_self x), hG_ae_eq⟩

Premises used: Set.mem_range_self, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Preorder β
inst_1 : Zero β
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t
G : α → β
hG_meas : Measurable G
hG_mem : range G ⊆ (Preorder.toLE : LE β).1 0
hG_ae_eq : f =ᶠ[ae μ] G
⊢ ∃ (g : α → β), Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g

Tactic:
exact ⟨G, hG_meas, fun x => hG_mem (mem_range_self x), hG_ae_eq⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
h_1 : Nontrivial α
inhabit : ∀ (inhabited_h : Inhabited α), AEMeasurable (codRestrict f s hfs) μ
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
inhabit α
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
h_1 : Nontrivial α
inhabited_h : Inhabited α
⊢ ∃ (g : α → β), Measurable g ∧ range g ⊆ s ∧ f =ᶠ[ae μ] g

Tactic:
h.exists_ae_eq_range_subset (Eventually.of_forall hfs) ⟨_, hfs default⟩

Premises used: Inhabited.default, AEMeasurable.exists_ae_eq_range_subset, Filter.Eventually.of_forall, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
h_1 : Nontrivial α
inhabited_h : Inhabited α
obtain :
  ∀ (g : α → β) (g_meas : Measurable g) (hg : range g ⊆ s) (fg : f =ᶠ[ae μ] g), AEMeasurable (codRestrict f s hfs) μ
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
obtain ⟨g, g_meas, hg, fg⟩ : ∃ g : α → β, Measurable g ∧ range g ⊆ s ∧ f =ᵐ[μ] g :=
    h.exists_ae_eq_range_subset (Eventually.of_forall hfs) ⟨_, hfs default⟩

Premises used: Inhabited.default, AEMeasurable.exists_ae_eq_range_subset, Filter.Eventually.of_forall, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
h_1 : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
⟨codRestrict g s fun x => hg (mem_range_self _), Measurable.subtype_mk g_meas, ?_⟩

Premises used: Set.mem_range_self, AEMeasurable, Measurable.subtype_mk, And.intro, Exists.intro, Set.codRestrict
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
h_1 : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
refine : codRestrict f s hfs =ᶠ[ae μ] codRestrict g s ⋯
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
refine ⟨codRestrict g s fun x => hg (mem_range_self _), Measurable.subtype_mk g_meas, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
h_1 : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
h₁ : ∀ (x : α) (hx : f x = g x), codRestrict f s hfs x = codRestrict g s ⋯ x
⊢ codRestrict f s hfs =ᶠ[ae μ] codRestrict g s ⋯

Tactic:
filter_upwards [fg] with x hx
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
h_1 : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ codRestrict f s hfs x = codRestrict g s ⋯ x

Tactic:
simpa [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
inl : ∀ (h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y), AEMeasurable (_m := m0) f 0
inr : ∀ (hμ : μ ≠ 0), AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
rcases eq_or_ne μ 0 with (rfl | hμ)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y
⊢ AEMeasurable (_m := m0) f 0

Tactic:
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 : α → β
h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y
⊢ AEMeasurable (_m := m0) f 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 α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
⊢ (ae μ).NeBot

Tactic:
haveI := ae_neBot.2 hμ
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : (ae μ).NeBot
inr : ∀ (x : α) (hx : ∀ᵐ (y : α) ∂μ, f x = f y), AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
rcases h.exists with ⟨x, hx⟩

Premises used: Filter.Eventually.exists
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : (ae μ).NeBot
x : α
hx : ∀ᵐ (y : α) ∂μ, f x = f y
⊢ AEMeasurable f μ

Tactic:
⟨const α (f x), measurable_const, EventuallyEq.symm hx⟩

Premises used: AEMeasurable, And.intro, Exists.intro, Function.const, measurable_const, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : (ae μ).NeBot
x : α
hx : ∀ᵐ (y : α) ∂μ, f x = f y
⊢ AEMeasurable f μ

Tactic:
exact ⟨const α (f x), measurable_const, EventuallyEq.symm hx⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : LinearOrder α
f : α → β
a b : α
rw :
  AEMeasurable f (μ.restrict (Ioc a b ∪ Ioc b a)) ↔
    AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a))
rw₁ rw₂ :
  AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a)) ↔
    AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a))
⊢ AEMeasurable f (μ.restrict (Ι a b)) ↔ AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a))

Tactic:
rw [uIoc_eq_union, aemeasurable_union_iff]

Premises used: aemeasurable_union_iff, Set.uIoc_eq_union
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : μ.IsComplete
⊢ AEMeasurable f μ ↔ Measurable f

Tactic:
⟨fun h => h.nullMeasurable.measurable_of_complete, fun h => h.aemeasurable⟩

Premises used: AEMeasurable.nullMeasurable, Measurable.aemeasurable, MeasureTheory.NullMeasurable.measurable_of_complete, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
⊢ AEMeasurable (_m := inst) g (Measure.map f μ) ↔ AEMeasurable (g ∘ f) μ

Tactic:
⟨fun H => H.comp_measurable hf.measurable, ?_⟩

Premises used: AEMeasurable.comp_measurable, Iff.intro, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
refine : AEMeasurable (g ∘ f) μ → AEMeasurable (_m := inst) g (Measure.map f μ)
⊢ AEMeasurable (_m := inst) g (Measure.map f μ) ↔ AEMeasurable (g ∘ f) μ

Tactic:
refine ⟨fun H => H.comp_measurable hf.measurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
g₁ : α → γ
hgm₁ : Measurable g₁
heq : g ∘ f =ᶠ[ae μ] g₁
rcases :
  ∀ (g₂ : β → γ) (hgm₂ : Measurable g₂) (hgm₁ : Measurable (g₂ ∘ f)) (heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f),
    AEMeasurable (_m := inst) g (Measure.map f μ)
⊢ AEMeasurable (_m := inst) g (Measure.map f μ)

Tactic:
rcases hf.exists_measurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩

Premises used: Nonempty.intro, MeasurableEmbedding.exists_measurable_extend, rfl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
g₂ : β → γ
hgm₂ : Measurable g₂
hgm₁ : Measurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEMeasurable (_m := inst) g (Measure.map f μ)

Tactic:
⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩

Premises used: Iff.mpr, AEMeasurable, And.intro, Exists.intro, MeasurableEmbedding.ae_map_iff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
g₂ : β → γ
hgm₂ : Measurable g₂
hgm₁ : Measurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEMeasurable (_m := inst) g (Measure.map f μ)

Tactic:
exact ⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩
-- 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 α
⊢ AEMeasurable (g ∘ f) μ ↔ AEMeasurable f μ

Tactic:
⟨fun H => ?_, hg.measurable.comp_aemeasurable⟩

Premises used: Iff.intro, Measurable.comp_aemeasurable, MeasurableEmbedding.measurable
-- 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 α
refine : ∀ (H : AEMeasurable (g ∘ f) μ), AEMeasurable f μ
⊢ AEMeasurable (g ∘ f) μ ↔ AEMeasurable f μ

Tactic:
refine ⟨fun H => ?_, hg.measurable.comp_aemeasurable⟩