awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
l l' : Filter α
⊢ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ → IntegrableAtFilter f (l ⊔ l') μ

Tactic:
exact fun ⟨⟨s, hsl, hs⟩, ⟨t, htl, ht⟩⟩ ↦ ⟨s ∪ t, union_mem_sup hsl htl, hs.union ht⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
l : Filter α
E : Type u_7
H : Type u_8
𝕜 : Type u_9
𝕜' : Type u_10
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜' E
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
f : α → H
L : H →SL[σ] E
hf : IntegrableAtFilter f l μ
⊢ IntegrableAtFilter.{u_1, u_7} (ε := E) ((⇑L : (a : H) → E) ∘ f) l μ

Tactic:
let ⟨s, hs, hf⟩ := hf; ⟨s, hs, L.integrableOn_comp hf⟩

Premises used: Function.comp, MeasureTheory.IntegrableAtFilter, _private.0.ContinuousLinearMap.integrableAtFilter_comp.match_1, And.intro, Exists.intro, DFunLike.coe, ContinuousLinearMap.integrableOn_comp
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 : ℝ), ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C

Tactic:
hf.imp fun C hC => eventually_smallSets.2 ⟨_, hC, fun t => id⟩

Premises used: Iff.mpr, Norm.norm, _private.Mathlib.Data.Real.Basic.0.Real.le, Filter.eventually_smallSets, id, Exists.imp, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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)
obtain : ∀ (C : ℝ) (hC : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C), IntegrableAtFilter f l μ
⊢ 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⟩

Premises used: Iff.mpr, Filter.smallSets, Filter.eventually_smallSets, id, Exists.imp, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
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 μ
⊢ IntegrableAtFilter f l μ

Tactic:
rcases (hfm.eventually.and (hμ.eventually.and hC)).exists_measurable_mem_of_smallSets with
    ⟨s, hsl, hsm, hfm, hμ, hC⟩

Premises used: Filter.Eventually.exists_measurable_mem_of_smallSets, Filter.Eventually.and, StronglyMeasurableAtFilter.eventually, MeasureTheory.Measure.FiniteAtFilter.eventually
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ

Tactic:
⟨s, hsl, ⟨hfm, .restrict_of_bounded hμ (C := C) ?_⟩⟩

Premises used: MeasureTheory.HasFiniteIntegral.restrict_of_bounded, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
refine : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ IntegrableAtFilter f l μ

Tactic:
refine ⟨s, hsl, ⟨hfm, .restrict_of_bounded hμ (C := C) ?_⟩⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
rw : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C

Tactic:
rw [ae_restrict_eq hsm, eventually_inf_principal]

Premises used: Filter.eventually_inf_principal, MeasureTheory.ae_restrict_eq
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 : α) ∂μ, x ∈ s → ‖f x‖ ≤ C

Tactic:
Eventually.of_forall hC

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 : α) ∂μ, x ∈ s → ‖f x‖ ≤ C

Tactic:
exact Eventually.of_forall hC

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
b : E
hf : Tendsto f (l ⊓ ae μ) (𝓝 b)
⊢ IntegrableAtFilter f l μ

Tactic:
(hμ.inf_of_left.integrableAtFilter (hfm.filter_mono inf_le_left)
      hf.norm.isBoundedUnder_le).of_inf_ae

Premises used: MeasureTheory.Measure.FiniteAtFilter.inf_of_left, Filter.Tendsto.isBoundedUnder_le, StronglyMeasurableAtFilter.filter_mono, Filter.Tendsto.norm, MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter, inf_le_left, MeasureTheory.IntegrableAtFilter.of_inf_ae
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
b : E
hf : Tendsto f l (𝓝 b)
⊢ IntegrableAtFilter f l μ

Tactic:
hμ.integrableAtFilter hfm hf.norm.isBoundedUnder_le

Premises used: Filter.Tendsto.isBoundedUnder_le, Filter.Tendsto.norm, MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
s : Set α
μ : Measure α
f : α → E
s_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f_mble : AEStronglyMeasurable f μ
M : ℝ
f_bdd : ∀ᵐ (a : α) ∂μ.restrict s, ‖f a‖ ≤ M
⊢ IntegrableOn f s μ

Tactic:
⟨f_mble.restrict, .restrict_of_bounded (C := M) s_finite.lt_top f_bdd⟩

Premises used: MeasureTheory.HasFiniteIntegral.restrict_of_bounded, MeasureTheory.Integrable, MeasureTheory.IntegrableOn, MeasureTheory.AEStronglyMeasurable.restrict, Ne.lt_top, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ

Tactic:
⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩

Premises used: And.right, And.left, And.intro, Iff.intro, MeasureTheory.Integrable.add
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
refine_2 : ∀ (hfg : Integrable (f + g) μ), Integrable g μ
⊢ Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ

Tactic:
refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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) μ
refine_1 : Integrable ((support f).indicator (f + g)) μ
⊢ Integrable f μ

Tactic:
rw [← indicator_add_eq_left h]

Premises used: Set.indicator_add_eq_left
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 ((support f).indicator (f + g)) μ

Tactic:
hfg.indicator hf.measurableSet_support

Premises used: MeasureTheory.StronglyMeasurable.measurableSet_support, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 ((support f).indicator (f + g)) μ

Tactic:
exact hfg.indicator hf.measurableSet_support

Premises used: MeasureTheory.StronglyMeasurable.measurableSet_support, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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) μ
refine_2 : Integrable ((support g).indicator (f + g)) μ
⊢ Integrable g μ

Tactic:
rw [← indicator_add_eq_right h]

Premises used: Set.indicator_add_eq_right
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 ((support g).indicator (f + g)) μ

Tactic:
hfg.indicator hg.measurableSet_support

Premises used: MeasureTheory.StronglyMeasurable.measurableSet_support, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 ((support g).indicator (f + g)) μ

Tactic:
exact hfg.indicator hg.measurableSet_support

Premises used: MeasureTheory.StronglyMeasurable.measurableSet_support, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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)
by_contra : ∀ (H : ¬a = 0), False
⊢ a = 0

Tactic:
by_contra H
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
⊢ ∃ (ε : ℝ), 0 < ε ∧ ε < ‖a‖

Tactic:
exists_between (norm_pos_iff.mpr H)

Premises used: Iff.mpr, norm_pos_iff, exists_between
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
obtain : ∀ (ε : ℝ) (εpos : 0 < ε) (hε : ε < ‖a‖), False
⊢ False

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ), 0 < ε ∧ ε < ‖a‖ := exists_between (norm_pos_iff.mpr H)

Premises used: Iff.mpr, norm_pos_iff, exists_between
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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‖
rcases : ∀ (u : Set α) (ul : u ∈ l) (hu : IntegrableOn f u μ), False
⊢ False

Tactic:
rcases h with ⟨u, ul, hu⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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‖}
⊢ IntegrableOn f v μ

Tactic:
have hv : IntegrableOn f v μ := hu.mono_set inter_subset_left
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
⊢ v ∈ l

Tactic:
have vl : v ∈ l := inter_mem ul ((tendsto_order.1 hf.norm).1 _ hε)
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
⊢ 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)
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa only [Measure.restrict_apply_self]

Premises used: MeasureTheory.Measure.restrict_apply_self
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have : μ v ≠ ∞ := ne_of_lt (by simpa only [Measure.restrict_apply_self])
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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_1 : LT.lt (α := ℝ≥0∞) ((μ.restrict v : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ False

Tactic:
this (h' v vl)
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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_1 : LT.lt (α := ℝ≥0∞) ((μ.restrict v : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ False

Tactic:
exact this (h' v vl)
-- 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
⊢ Nontrivial α

Tactic:
nontriviality α
-- 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 α
inhabit : ∀ (inhabited_h : Inhabited α), AEMeasurable f (μ.restrict s)
⊢ AEMeasurable f (μ.restrict s)

Tactic:
inhabit α
-- 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 α
⊢ (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
-- 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
⊢ AEMeasurable f (μ.restrict s)

Tactic:
⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩

Premises used: Inhabited.default, AEMeasurable, And.intro, Exists.intro, Set.piecewise, Filter.EventuallyEq.symm
-- 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
refine : Measurable (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default)
⊢ AEMeasurable f (μ.restrict s)

Tactic:
refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
-- 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
hf₁ :
  ∀ (s_1 : Set β),
    IsOpen[inst_3] s_1 → MeasurableSet ((s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) ⁻¹' s_1)
⊢ Measurable (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default)

Tactic:
apply measurable_of_isOpen

Premises used: measurable_of_isOpen
-- 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 α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
_root_.continuousOn_iff'.1 hf t ht

Premises used: Iff.mp, continuousOn_iff'
-- 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
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)
⊢ 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

Premises used: Iff.mp, continuousOn_iff', Set