awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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 α
⊢ AEMeasurable (codRestrict f s hfs) μ
have obtain : ∀ (g : α → β) (g_meas : Measurable g) (hg : range g ⊆ s) (fg : f =ᶠ[ae μ] g), 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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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) μ
have refine : codRestrict f s hfs =ᶠ[ae μ] codRestrict g s sorry
Tactic: refine ⟨codRestrict g s fun x => hg (mem_range_self _), Measurable.subtype_mk g_meas, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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
⊢ codRestrict f s hfs =ᶠ[ae μ] codRestrict g s ⋯
have h₁ : ∀ (x : α) (hx : f x = g x), codRestrict f s hfs x = codRestrict g s sorry x
Tactic: filter_upwards [fg] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
⊢ AEMeasurable f μ
have inl : ∀ (h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y), AEMeasurable (_m := m0) f 0
Tactic: rcases eq_or_ne μ 0 with (rfl | hμ)
Cleared hypotheses: μ, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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
⊢ AEMeasurable f μ
have inr : ∀ (hμ : μ ≠ 0), AEMeasurable f μ
Tactic: rcases eq_or_ne μ 0 with (rfl | hμ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
⊢ AEMeasurable f μ
have this : (ae μ).NeBot
Tactic: haveI := ae_neBot.2 hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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
⊢ AEMeasurable f μ
have inr : ∀ (x : α) (hx : ∀ᵐ (y : α) ∂μ, f x = f y), AEMeasurable f μ
Tactic: rcases h.exists with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : LinearOrder α
f : α → β
a b : α
⊢ AEMeasurable f (μ.restrict (Ι a b)) ↔ AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a))
have rw : AEMeasurable f (μ.restrict (Ioc a b ∪ Ioc b a)) ↔
  AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a))
Tactic: rw [uIoc_eq_union, aemeasurable_union_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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))
⊢ AEMeasurable f (μ.restrict (Ι a b)) ↔ AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a))
have 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))
Tactic: rw [uIoc_eq_union, aemeasurable_union_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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) μ
have refine : AEMeasurable (g ∘ f) μ → AEMeasurable (_m := inst) g (Measure.map f μ)
Tactic: refine ⟨fun H => H.comp_measurable hf.measurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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₁
⊢ AEMeasurable (_m := inst) g (Measure.map f μ)
have rcases : ∀ (g₂ : β → γ) (hgm₂ : Measurable g₂) (hgm₁ : Measurable (g₂ ∘ f)) (heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f),
  AEMeasurable (_m := inst) g (Measure.map f μ)
Tactic: rcases hf.exists_measurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩
Cleared hypotheses: g₁, hgm₁, heq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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 μ
have refine : ∀ (H : AEMeasurable (g ∘ f) μ), AEMeasurable f μ
Tactic: refine ⟨fun H => ?_, hg.measurable.comp_aemeasurable⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
this : AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ
⊢ AEMeasurable f μ
have rwa : ∀ (this : AEMeasurable (_root_.id ∘ f) μ), AEMeasurable f μ
Tactic: rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
⊢ AEMeasurable f μ
have suffices : AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ
Tactic: suffices AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ by
    rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
s : Set α
hs : MeasurableSet s
μ : Measure α
f : α → β
⊢ AEMeasurable f (μ.restrict s) ↔
    AEMeasurable (α := (↑s : Type u_2)) (_m := Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)
have rw : AEMeasurable (_m := m0) f
    (Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)) ↔
  AEMeasurable (α := (↑s : Type u_2)) (_m := Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
    (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)
Tactic: rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).aemeasurable_map_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
s : Set α
hs : MeasurableSet s
μ : Measure α
f : α → β
rw :
  AEMeasurable (_m := m0) f
      (Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)) ↔
    AEMeasurable (α := (↑s : Type u_2)) (_m := Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)
⊢ AEMeasurable f (μ.restrict s) ↔
    AEMeasurable (α := (↑s : Type u_2)) (_m := Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)
have rw₁ : AEMeasurable (α := { x : α // x ∈ s }) (_m := Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
    (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ) ↔
  AEMeasurable (α := (↑s : Type u_2)) (_m := Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
    (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)
Tactic: rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).aemeasurable_map_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
⊢ AEMeasurable g (μ.restrict (Ioi x))
have this : Nonempty α
Tactic: haveI : Nonempty α := ⟨x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
⊢ AEMeasurable g (μ.restrict (Ioi x))
have obtain : ∀ (u : ℕ → α) (hu_tendsto : Tendsto u atTop atTop), AEMeasurable g (μ.restrict (Ioi x))
Tactic: obtain ⟨u, hu_tendsto⟩ := exists_seq_tendsto (atTop : Filter α)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ Ioi x = ⋃ (n : ℕ), Ioc x (u n)
have rw : ∀ (x_1 : α), x < x_1 → ∃ (i : ℕ), x_1 ≤ u i
Tactic: rw [iUnion_Ioc_eq_Ioi_self_iff.mpr _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ AEMeasurable g (μ.restrict (Ioi x))
have Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
Tactic: have Ioi_eq_iUnion : Ioi x = ⋃ n : ℕ, Ioc x (u n) := by
    rw [iUnion_Ioc_eq_Ioi_self_iff.mpr _]
    exact fun y _ => (hu_tendsto.eventually (eventually_ge_atTop y)).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
⊢ AEMeasurable g (μ.restrict (Ioi x))
have rw : ∀ (i : ℕ), AEMeasurable g (μ.restrict (Ioc x (u i)))
Tactic: rw [Ioi_eq_iUnion, aemeasurable_iUnion_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))
have inl : ∀ (h : x < u n), AEMeasurable g (μ.restrict (Ioc x (u n)))
Tactic: rcases lt_or_ge x (u n) with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
inl : ∀ (h : x < u n), AEMeasurable g (μ.restrict (Ioc x (u n)))
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))
have inr : ∀ (h : u n ≤ x), AEMeasurable g (μ.restrict (Ioc x (u n)))
Tactic: rcases lt_or_ge x (u n) with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst : LinearOrder α
inst_1 : IsCountablyGenerated.{u_2} (α := α) atTop
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))
have inr : AEMeasurable (_m := m0) g 0
Tactic: rw [Ioc_eq_empty (not_lt.mpr h), Measure.restrict_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
have mp : AEMeasurable (s.indicator f) μ → AEMeasurable f (μ.restrict s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
mp : AEMeasurable (s.indicator f) μ → AEMeasurable f (μ.restrict s)
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
have mpr : AEMeasurable f (μ.restrict s) → AEMeasurable (s.indicator f) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
⊢ AEMeasurable (s.indicator f) μ
have mpr : s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)
Tactic: refine ⟨indicator s (h.mk f), h.measurable_mk.indicator hs, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)
have A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEMeasurable.mk f h)
Tactic: have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (AEMeasurable.mk f h) :=
      (indicator_ae_eq_restrict hs).trans (h.ae_eq_mk.trans <| (indicator_ae_eq_restrict hs).symm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)
have B : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] s.indicator (AEMeasurable.mk f h)
Tactic: have B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (AEMeasurable.mk f h) :=
      (indicator_ae_eq_restrict_compl hs).trans (indicator_ae_eq_restrict_compl hs).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s : Set α
hs : NullMeasurableSet s μ
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
have rcases : ∀ (t : Set α) (ht : MeasurableSet t) (hst : s =ᶠ[ae μ] t),
  AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
Tactic: rcases hs with ⟨t, ht, hst⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s t : Set α
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
have rw : AEMeasurable (t.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
Tactic: rw [← aemeasurable_congr (indicator_ae_eq_of_ae_eq_set hst.symm), aemeasurable_indicator_iff ht,
      restrict_congr_set hst]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s t : Set α
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
rw : AEMeasurable (t.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
have rw₁ : AEMeasurable f (μ.restrict t) ↔ AEMeasurable f (μ.restrict s)
Tactic: rw [← aemeasurable_congr (indicator_ae_eq_of_ae_eq_set hst.symm), aemeasurable_indicator_iff ht,
      restrict_congr_set hst]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : Zero β
s t : Set α
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
rw : AEMeasurable (t.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
rw₁ : AEMeasurable f (μ.restrict t) ↔ AEMeasurable f (μ.restrict s)
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
have rw₂ : AEMeasurable f (μ.restrict t) ↔ AEMeasurable f (μ.restrict t)
Tactic: rw [← aemeasurable_congr (indicator_ae_eq_of_ae_eq_set hst.symm), aemeasurable_indicator_iff ht,
      restrict_congr_set hst]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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
⊢ AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ ↔ NullMeasurableSet s μ
have mp : AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ → NullMeasurableSet s μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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 μ
⊢ AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ ↔ NullMeasurableSet s μ
have mpr : NullMeasurableSet s μ → AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : Zero β
s : Set α
inst_2 : MeasurableSingletonClass β
b : β
inst_3 : NeZero b
h : AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ
⊢ NullMeasurableSet s μ
have h₁ : s = preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ
Tactic: convert! h.nullMeasurable (MeasurableSet.singleton (0 : β)).compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : Zero β
s : Set α
inst_2 : MeasurableSingletonClass β
b : β
inst_3 : NeZero b
h : AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ
⊢ s = preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ
have h₁ : s = (if Membership.mem (γ := Set β) {0}ᶜ b then s else ∅) ∪ if Membership.mem (γ := Set β) {0}ᶜ 0 then sᶜ else ∅
Tactic: rw [indicator_const_preimage_eq_union s {0}ᶜ b]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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
⊢ AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ ↔ NullMeasurableSet s μ
have mp : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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 μ
⊢ AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ ↔ NullMeasurableSet s μ
have mpr : NullMeasurableSet s μ → AEMeasurable.{u_2, u_3} (β := β) (s.indicator fun (x : α) ↦ b) μ
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ Eq (α := Measure δ) (restrict (map f μ) s) (restrict (map (AEMeasurable.mk f hf) μ) s)
have e_μ : Eq (α := Measure δ) (map f μ) (map (AEMeasurable.mk f hf) μ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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 (μ.restrict (AEMeasurable.mk f hf ⁻¹' s))) (map f (μ.restrict (f ⁻¹' s)))
have h : μ.restrict (AEMeasurable.mk f hf ⁻¹' s) = μ.restrict (f ⁻¹' s)
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ μ.restrict (AEMeasurable.mk f hf ⁻¹' s) = μ.restrict (f ⁻¹' s)
have 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∞)
Tactic: ext1 t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (AEMeasurable.mk f hf ⁻¹' s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict (f ⁻¹' s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ AEMeasurable.mk f hf ⁻¹' s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f ⁻¹' s) : ℝ≥0∞)
Tactic: simp only [ht, Measure.restrict_apply]