awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
hf₁ : MeasurableSet (u ∩ s ∪ (fun (x : α) ↦ f default) ⁻¹' t \ s)
⊢ MeasurableSet ((s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) ⁻¹' t)

Tactic:
rw [piecewise_preimage, Set.ite, hu]

Premises used: Set.ite, Set.piecewise_preimage
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 (u ∩ s ∪ (fun (x : α) ↦ f default) ⁻¹' t \ s)

Tactic:
(u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)

Premises used: MeasurableSet.diff, IsOpen.measurableSet, MeasurableSet.union, measurable_const, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 (u ∩ s ∪ (fun (x : α) ↦ f default) ⁻¹' t \ s)

Tactic:
exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)

Premises used: MeasurableSet.diff, IsOpen.measurableSet, MeasurableSet.union, measurable_const, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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)
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)
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 (u ∩ s ∪ (fun (x : α) ↦ f default) ⁻¹' t \ s)
⊢ 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)

Premises used: Set.ite, measurable_of_isOpen, Set.piecewise_preimage, Set
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 : NullMeasurableSet s μ
rcases : ∀ (t : Set α) (ts : t ⊆ s) (ht : MeasurableSet t) (t_eq_s : t =ᶠ[ae μ] s), AEMeasurable f (μ.restrict s)
⊢ AEMeasurable f (μ.restrict s)

Tactic:
rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩

Premises used: MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 : NullMeasurableSet s μ
t : Set α
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
rw : AEMeasurable f (μ.restrict t)
⊢ AEMeasurable f (μ.restrict s)

Tactic:
rw [← Measure.restrict_congr_set t_eq_s]

Premises used: MeasureTheory.Measure.restrict_congr_set
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 : NullMeasurableSet s μ
t : Set α
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
⊢ AEMeasurable f (μ.restrict t)

Tactic:
ContinuousOn.aemeasurable (hf.mono ts) ht

Premises used: ContinuousOn.aemeasurable, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 : NullMeasurableSet s μ
t : Set α
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
⊢ AEMeasurable f (μ.restrict t)

Tactic:
exact ContinuousOn.aemeasurable (hf.mono ts) ht

Premises used: ContinuousOn.aemeasurable, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
rw : AEMeasurable f (μ.restrict s) ∧ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ t
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
rw [aestronglyMeasurable_iff_aemeasurable_separable]

Premises used: aestronglyMeasurable_iff_aemeasurable_separable
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
⊢ AEMeasurable f (μ.restrict s) ∧ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ t

Tactic:
⟨hf.aemeasurable hs, f '' s, hf.isSeparable_image h's, ?_⟩

Premises used: ContinuousOn.isSeparable_image, And.intro, Exists.intro, ContinuousOn.aemeasurable, Set.image
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
refine : ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ f '' s
⊢ AEMeasurable f (μ.restrict s) ∧ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ t

Tactic:
refine ⟨hf.aemeasurable hs, f '' s, hf.isSeparable_image h's, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ f '' s

Tactic:
mem_of_superset (self_mem_ae_restrict hs) (subset_preimage_image _ _)

Premises used: Filter.Eventually, Set.subset_preimage_image, MeasureTheory.self_mem_ae_restrict, Filter.mem_of_superset
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ f '' s

Tactic:
exact mem_of_superset (self_mem_ae_restrict hs) (subset_preimage_image _ _)

Premises used: Set.subset_preimage_image, MeasureTheory.self_mem_ae_restrict, Filter.mem_of_superset
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
aestronglyMeasurable_iff_aemeasurable_separable.2
      ⟨hf.aemeasurable hs, f '' s, ?_,
        mem_of_superset (self_mem_ae_restrict hs) (subset_preimage_image _ _)⟩

Premises used: Iff.mpr, aestronglyMeasurable_iff_aemeasurable_separable, And.intro, Exists.intro, ContinuousOn.aemeasurable, Set.image, Set.subset_preimage_image, MeasureTheory.self_mem_ae_restrict, Filter.mem_of_superset
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
f₁ : IsSeparable (f '' s)
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
refine
    aestronglyMeasurable_iff_aemeasurable_separable.2
      ⟨hf.aemeasurable hs, f '' s, ?_,
        mem_of_superset (self_mem_ae_restrict hs) (subset_preimage_image _ _)⟩

Premises used: Iff.mpr, aestronglyMeasurable_iff_aemeasurable_separable, And.intro, Exists.intro, ContinuousOn.aemeasurable, Set.image, Set.subset_preimage_image, MeasureTheory.self_mem_ae_restrict, Filter.mem_of_superset
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
inl : SecondCountableTopology α → IsSeparable (f '' s)
inr : SecondCountableTopology β → IsSeparable (f '' s)
⊢ IsSeparable (f '' s)

Tactic:
cases h.out

Premises used: SecondCountableTopologyEither.out
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_1 : SecondCountableTopology α
inl : IsSeparable.{u_2} (α := β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
⊢ IsSeparable (f '' s)

Tactic:
rw [image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_1 : SecondCountableTopology α
⊢ IsSeparable.{u_2} (α := β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α))

Tactic:
isSeparable_range <| continuousOn_iff_continuous_restrict.1 hf

Premises used: continuousOn_iff_continuous_restrict, Iff.mp, TopologicalSpace.isSeparable_range
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_1 : SecondCountableTopology α
⊢ IsSeparable.{u_2} (α := β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α))

Tactic:
exact isSeparable_range <| continuousOn_iff_continuous_restrict.1 hf

Premises used: continuousOn_iff_continuous_restrict, Iff.mp, TopologicalSpace.isSeparable_range
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_1 : SecondCountableTopology β
⊢ IsSeparable (f '' s)

Tactic:
.of_separableSpace _

Premises used: TopologicalSpace.IsSeparable.of_separableSpace
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_1 : SecondCountableTopology β
⊢ IsSeparable (f '' s)

Tactic:
exact .of_separableSpace _
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
rw : AEMeasurable f (μ.restrict t) ∧ ∃ (t_1 : Set β), IsSeparable t_1 ∧ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ t_1
⊢ AEStronglyMeasurable f (μ.restrict t)

Tactic:
rw [aestronglyMeasurable_iff_aemeasurable_separable]

Premises used: aestronglyMeasurable_iff_aemeasurable_separable
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ AEMeasurable f (μ.restrict t) ∧ ∃ (t_1 : Set β), IsSeparable t_1 ∧ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ t_1

Tactic:
⟨(hf.mono hts).aemeasurable ht, f '' s, ?_, ?_⟩

Premises used: And.intro, Exists.intro, ContinuousOn.aemeasurable, ContinuousOn.mono, Set.image
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
refine_1 : IsSeparable (f '' s)
refine_2 : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ f '' s
⊢ AEMeasurable f (μ.restrict t) ∧ ∃ (t_1 : Set β), IsSeparable t_1 ∧ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ t_1

Tactic:
refine ⟨(hf.mono hts).aemeasurable ht, f '' s, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ IsSeparable (f '' s)

Tactic:
(hs.image_of_continuousOn hf).isSeparable

Premises used: IsCompact.isSeparable, IsCompact.image_of_continuousOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ IsSeparable (f '' s)

Tactic:
exact (hs.image_of_continuousOn hf).isSeparable

Premises used: IsCompact.isSeparable, IsCompact.image_of_continuousOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
a : α
ha : a ∈ t
⊢ f a ∈ f '' s

Tactic:
image_mono hts (mem_image_of_mem f ha)

Premises used: Set.image_mono, Set.mem_image_of_mem
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ f '' s) x} x}
      a
h₁ h₂ : ∀ (a : α) (ha : a ∈ t), f a ∈ f '' s
⊢ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ f '' s

Tactic:
filter_upwards [ae_restrict_mem ht] with a ha using image_mono hts (mem_image_of_mem f ha)

Premises used: MeasureTheory.ae_restrict_mem
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
hf.aestronglyMeasurable_of_subset_isCompact hs h's Subset.rfl

Premises used: ContinuousOn.aestronglyMeasurable_of_subset_isCompact, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : CompactSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
μ : Measure α
f : α → β
hf : Continuous[inst, inst_3] f
⊢ AEStronglyMeasurable f μ

Tactic:
simpa using hf.continuousOn.aestronglyMeasurable_of_isCompact isCompact_univ .univ

Premises used: ContinuousOn.aestronglyMeasurable_of_isCompact, Continuous.continuousOn, isCompact_univ, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : TopologicalSpace α
inst_2 : PseudoMetrizableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
a : α
t : Set α
f : α → E
hft : ContinuousOn f t
ht : MeasurableSet t
h't : IsSeparable t
ha : a ∈ t
⊢ IntegrableAtFilter f (𝓝[t] a) μ

Tactic:
haveI : (𝓝[t] a).IsMeasurablyGenerated := ht.nhdsWithin_isMeasurablyGenerated _
  (hft a ha).integrableAtFilter
    ⟨_, self_mem_nhdsWithin, hft.aestronglyMeasurable_of_isSeparable ht h't⟩
    (μ.finiteAt_nhdsWithin _ _)

Premises used: self_mem_nhdsWithin, And.intro, Filter.Tendsto.integrableAtFilter, Exists.intro, MeasureTheory.Measure.finiteAt_nhdsWithin, ContinuousOn.aestronglyMeasurable_of_isSeparable