awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
f : α → E
l : Filter α
inst_1 : l.IsMeasurablyGenerated
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)
⊢ IntegrableAtFilter f l μ
have obtain : ∀ (C : ℝ) (hC : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C), IntegrableAtFilter f l μ
Tactic: obtain ⟨C, hC⟩ : ∃ C, ∀ᶠ s in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C :=
    hf.imp fun C hC => eventually_smallSets.2 ⟨_, hC, fun t => id⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
f : α → E
l : Filter α
inst_1 : l.IsMeasurablyGenerated
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
⊢ IntegrableAtFilter f l μ
have rcases : ∀ (s : Set α) (hsl : s ∈ l) (hsm : MeasurableSet s) (hfm : AEStronglyMeasurable f (μ.restrict s))
  (hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (hC : ∀ x ∈ s, ‖f x‖ ≤ C),
  IntegrableAtFilter f l μ
Tactic: rcases (hfm.eventually.and (hμ.eventually.and hC)).exists_measurable_mem_of_smallSets with
    ⟨s, hsl, hsm, hfm, hμ, hC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
f : α → E
l : Filter α
inst_1 : l.IsMeasurablyGenerated
hfm_1 : StronglyMeasurableAtFilter f l μ
hμ_1 : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC_1 : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (μ.restrict s)
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ IntegrableAtFilter f l μ
have refine : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C
Tactic: refine ⟨s, hsl, ⟨hfm, .restrict_of_bounded hμ (C := C) ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
f : α → E
l : Filter α
inst_1 : l.IsMeasurablyGenerated
hfm_1 : StronglyMeasurableAtFilter f l μ
hμ_1 : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC_1 : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (μ.restrict s)
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C
have rw : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
Tactic: rw [ae_restrict_eq hsm, eventually_inf_principal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ
have refine_1 : ∀ (hfg : Integrable (f + g) μ), Integrable f μ
Tactic: refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
refine_1 : ∀ (hfg : Integrable (f + g) μ), Integrable f μ
⊢ Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ
have refine_2 : ∀ (hfg : Integrable (f + g) μ), Integrable g μ
Tactic: refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable f μ
have refine_1 : Integrable ((support f).indicator (f + g)) μ
Tactic: rw [← indicator_add_eq_left h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable g μ
have refine_2 : Integrable ((support g).indicator (f + g)) μ
Tactic: rw [← indicator_add_eq_right h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h : IntegrableAtFilter f l μ
h' : ∀ s ∈ l, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : E
hf : Tendsto f l (𝓝 a)
⊢ a = 0
have by_contra : ∀ (H : ¬a = 0), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h : IntegrableAtFilter f l μ
h' : ∀ s ∈ l, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
⊢ False
have obtain : ∀ (ε : ℝ) (εpos : 0 < ε) (hε : ε < ‖a‖), False
Tactic: obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ), 0 < ε ∧ ε < ‖a‖ := exists_between (norm_pos_iff.mpr H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h : IntegrableAtFilter f l μ
h' : ∀ s ∈ l, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
⊢ False
have rcases : ∀ (u : Set α) (ul : u ∈ l) (hu : IntegrableOn f u μ), False
Tactic: rcases h with ⟨u, ul, hu⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h' : ∀ s ∈ l, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b : α | ε < ‖f b‖}
⊢ False
have hv : IntegrableOn f v μ
Tactic: have hv : IntegrableOn f v μ := hu.mono_set inter_subset_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h' : ∀ s ∈ l, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b : α | ε < ‖f b‖}
hv : IntegrableOn f v μ
⊢ False
have vl : v ∈ l
Tactic: have vl : v ∈ l := inter_mem ul ((tendsto_order.1 hf.norm).1 _ hε)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h' : ∀ s ∈ l, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b : α | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
⊢ False
have this : LT.lt (α := ℝ≥0∞) ((μ.restrict v : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have : μ.restrict v v < ∞ := lt_of_le_of_lt (measure_mono inter_subset_right)
    (Integrable.measure_gt_lt_top hv.norm εpos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h' : ∀ s ∈ l, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b : α | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
this : LT.lt (α := ℝ≥0∞) ((μ.restrict v : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ False
have this₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have : μ v ≠ ∞ := ne_of_lt (by simpa only [Measure.restrict_apply_self])
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
⊢ AEMeasurable f (μ.restrict s)
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h : Nontrivial α
⊢ AEMeasurable f (μ.restrict s)
have inhabit : ∀ (inhabited_h : Inhabited α), AEMeasurable f (μ.restrict s)
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f (μ.restrict s)
have this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f
Tactic: have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h : Nontrivial α
inhabited_h : Inhabited α
this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f
⊢ AEMeasurable f (μ.restrict s)
have refine : Measurable (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default)
Tactic: refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h : Nontrivial α
inhabited_h : Inhabited α
this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f
⊢ Measurable (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default)
have hf₁ : ∀ (s_1 : Set β),
  IsOpen[inst_3] s_1 → MeasurableSet ((s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) ⁻¹' s_1)
Tactic: apply measurable_of_isOpen
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h : Nontrivial α
inhabited_h : Inhabited α
this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f
t : Set β
ht : IsOpen[inst_3] t
⊢ MeasurableSet ((s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) ⁻¹' t)
have hf₁ : ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : f ⁻¹' t ∩ s = u ∩ s),
  MeasurableSet ((s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) ⁻¹' t)
Tactic: obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
    _root_.continuousOn_iff'.1 hf t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h : Nontrivial α
inhabited_h : Inhabited α
this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f
t : Set β
ht : IsOpen[inst_3] t
u : Set α
u_open : IsOpen[inst] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet ((s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) ⁻¹' t)
have hf₁ : MeasurableSet (u ∩ s ∪ (fun (x : α) ↦ f default) ⁻¹' t \ s)
Tactic: rw [piecewise_preimage, Set.ite, hu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
⊢ AEMeasurable f (μ.restrict s)
have nontriviality : Subsingleton α → AEMeasurable f (μ.restrict s)
Tactic: classical
  nontriviality α; inhabit α
  have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
  refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
  apply measurable_of_isOpen
  intro t ht
  obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
    _root_.continuousOn_iff'.1 hf t ht
  rw [piecewise_preimage, Set.ite, hu]
  exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
nontriviality : Subsingleton α → AEMeasurable f (μ.restrict s)
⊢ AEMeasurable f (μ.restrict s)
have nontriviality₁ : Nontrivial α → AEMeasurable f (μ.restrict s)
Tactic: classical
  nontriviality α; inhabit α
  have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
  refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
  apply measurable_of_isOpen
  intro t ht
  obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
    _root_.continuousOn_iff'.1 hf t ht
  rw [piecewise_preimage, Set.ite, hu]
  exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
nontriviality : Subsingleton α → AEMeasurable f (μ.restrict s)
nontriviality₁ nontriviality₂ : Nontrivial α → AEMeasurable f (μ.restrict s)
⊢ AEMeasurable f (μ.restrict s)
have nontriviality₃ : Nontrivial α → ∀ (inhabited_h : Inhabited α), AEMeasurable f (μ.restrict s)
Tactic: classical
  nontriviality α; inhabit α
  have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
  refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
  apply measurable_of_isOpen
  intro t ht
  obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
    _root_.continuousOn_iff'.1 hf t ht
  rw [piecewise_preimage, Set.ite, hu]
  exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
nontriviality : Subsingleton α → AEMeasurable f (μ.restrict s)
nontriviality₁ nontriviality₂ : Nontrivial α → AEMeasurable f (μ.restrict s)
nontriviality₃ : Nontrivial α → ∀ (inhabited_h : Inhabited α), AEMeasurable f (μ.restrict s)
⊢ AEMeasurable f (μ.restrict s)
have nontriviality₄ : Nontrivial α →
  ∀ (inhabited_h : Inhabited α)
    (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f),
    AEMeasurable f (μ.restrict s)
Tactic: classical
  nontriviality α; inhabit α
  have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
  refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
  apply measurable_of_isOpen
  intro t ht
  obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
    _root_.continuousOn_iff'.1 hf t ht
  rw [piecewise_preimage, Set.ite, hu]
  exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
nontriviality : Subsingleton α → AEMeasurable f (μ.restrict s)
nontriviality₁ nontriviality₂ : Nontrivial α → AEMeasurable f (μ.restrict s)
nontriviality₃ : Nontrivial α → ∀ (inhabited_h : Inhabited α), AEMeasurable f (μ.restrict s)
nontriviality₄ :
  Nontrivial α →
    ∀ (inhabited_h : Inhabited α)
      (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f),
      AEMeasurable f (μ.restrict s)
⊢ AEMeasurable f (μ.restrict s)
have nontriviality₅ : Nontrivial α →
  ∀ (inhabited_h : Inhabited α)
    (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f),
    Measurable (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default)
Tactic: classical
  nontriviality α; inhabit α
  have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
  refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
  apply measurable_of_isOpen
  intro t ht
  obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
    _root_.continuousOn_iff'.1 hf t ht
  rw [piecewise_preimage, Set.ite, hu]
  exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
nontriviality : Subsingleton α → AEMeasurable f (μ.restrict s)
nontriviality₁ nontriviality₂ : Nontrivial α → AEMeasurable f (μ.restrict s)
nontriviality₃ : Nontrivial α → ∀ (inhabited_h : Inhabited α), AEMeasurable f (μ.restrict s)
nontriviality₄ :
  Nontrivial α →
    ∀ (inhabited_h : Inhabited α)
      (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f),
      AEMeasurable f (μ.restrict s)
nontriviality₅ :
  Nontrivial α →
    ∀ (inhabited_h : Inhabited α)
      (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f),
      Measurable (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default)
⊢ AEMeasurable f (μ.restrict s)
have hf₁ : Nontrivial α →
  ∀ (inhabited_h : Inhabited α)
    (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f) (s_1 : Set β),
    IsOpen[inst_3] s_1 → MeasurableSet ((s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) ⁻¹' s_1)
Tactic: classical
  nontriviality α; inhabit α
  have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
  refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
  apply measurable_of_isOpen
  intro t ht
  obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
    _root_.continuousOn_iff'.1 hf t ht
  rw [piecewise_preimage, Set.ite, hu]
  exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
nontriviality : Subsingleton α → AEMeasurable f (μ.restrict s)
nontriviality₁ nontriviality₂ : Nontrivial α → AEMeasurable f (μ.restrict s)
nontriviality₃ : Nontrivial α → ∀ (inhabited_h : Inhabited α), AEMeasurable f (μ.restrict s)
nontriviality₄ :
  Nontrivial α →
    ∀ (inhabited_h : Inhabited α)
      (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f),
      AEMeasurable f (μ.restrict s)
nontriviality₅ :
  Nontrivial α →
    ∀ (inhabited_h : Inhabited α)
      (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f),
      Measurable (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default)
hf₁ hf₂ :
  Nontrivial α →
    ∀ (inhabited_h : Inhabited α)
      (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f) (t : Set β)
      (ht : IsOpen[inst_3] t), MeasurableSet ((s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) ⁻¹' t)
⊢ AEMeasurable f (μ.restrict s)
have hf₃ : Nontrivial α →
  ∀ (inhabited_h : Inhabited α)
    (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f) (t : Set β)
    (ht : IsOpen[inst_3] t) (u : Set α) (u_open : IsOpen[inst] u) (hu : f ⁻¹' t ∩ s = u ∩ s),
    MeasurableSet ((s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) ⁻¹' t)
Tactic: classical
  nontriviality α; inhabit α
  have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
  refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
  apply measurable_of_isOpen
  intro t ht
  obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
    _root_.continuousOn_iff'.1 hf t ht
  rw [piecewise_preimage, Set.ite, hu]
  exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)