awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x : α | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
A : IntegrableOn f v μ
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ v
h'x : x ∉ s
⊢ 0 = f x

Tactic:
(hxt ⟨hx.1, h'x⟩).symm

Premises used: And.left, And.intro, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x : α | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
A : IntegrableOn f v μ
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ v
h'x : x ∉ s
⊢ 0 = f x

Tactic:
exact (hxt ⟨hx.1, h'x⟩).symm

Premises used: And.left, And.intro, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x : α | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
A : IntegrableOn f v μ
⊢ IntegrableOn f (t \ v) μ

Tactic:
have B : IntegrableOn f (t \ v) μ := by
    apply integrableOn_zero.congr
    filter_upwards [ae_restrict_of_ae h't,
      ae_restrict_mem₀ (ht.diff (measurableSet_toMeasurable μ u).nullMeasurableSet)] with x hxt hx
    by_cases h'x : x ∈ s
    · by_contra H
      exact hx.2 (subset_toMeasurable μ u ⟨h'x, Ne.symm H⟩)
    · exact (hxt ⟨hx.1, h'x⟩).symm
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x : α | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
A : IntegrableOn f v μ
B : IntegrableOn f (t \ v) μ
apply : t ⊆ v ∪ t \ v
⊢ IntegrableOn f t μ

Tactic:
apply (A.union B).mono_set _

Premises used: MeasureTheory.IntegrableOn.union, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x : α | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
A : IntegrableOn f v μ
B : IntegrableOn f (t \ v) μ
rw : t ⊆ v ∪ t
⊢ t ⊆ v ∪ t \ v

Tactic:
rw [union_diff_self]

Premises used: Set.union_diff_self
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x : α | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
A : IntegrableOn f v μ
B : IntegrableOn f (t \ v) μ
⊢ t ⊆ v ∪ t

Tactic:
subset_union_right

Premises used: Set.subset_union_right
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x : α | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
A : IntegrableOn f v μ
B : IntegrableOn f (t \ v) μ
⊢ t ⊆ v ∪ t

Tactic:
exact subset_union_right

Premises used: Set.subset_union_right
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : MeasurableSet t
h't : ∀ x ∈ t \ s, f x = 0
⊢ IntegrableOn f t μ

Tactic:
hf.of_ae_diff_eq_zero ht.nullMeasurableSet (Eventually.of_forall h't)

Premises used: MeasurableSet.nullMeasurableSet, Filter.Eventually.of_forall, MeasureTheory.IntegrableOn.of_ae_diff_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
rw : IntegrableOn f univ μ
⊢ Integrable f μ

Tactic:
rw [← integrableOn_univ]

Premises used: MeasureTheory.integrableOn_univ
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
apply : ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0
⊢ IntegrableOn f univ μ

Tactic:
apply hf.of_ae_diff_eq_zero nullMeasurableSet_univ

Premises used: MeasureTheory.nullMeasurableSet_univ, MeasureTheory.IntegrableOn.of_ae_diff_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
x : α
hx : x ∉ s → f x = 0
h'x : x ∈ univ \ s
⊢ f x = 0

Tactic:
hx h'x.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∉ s → f x = 0) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ univ \ s → f x = 0) x} x}
      a
h₁ h₂ : ∀ (x : α) (hx : x ∉ s → f x = 0) (h'x : x ∈ univ \ s), f x = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0

Tactic:
filter_upwards [h't] with x hx h'x using hx h'x.2
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ x ∉ s, f x = 0
⊢ Integrable f μ

Tactic:
hf.integrable_of_ae_notMem_eq_zero (Eventually.of_forall fun x hx => h't x hx)

Premises used: Filter.Eventually.of_forall, MeasureTheory.IntegrableOn.integrable_of_ae_notMem_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hs : MeasurableSet s
hf : IntegrableOn f (s ∩ support f) μ
⊢ IntegrableOn f s μ

Tactic:
simpa using hf.of_forall_diff_eq_zero hs

Premises used: MeasureTheory.IntegrableOn.of_forall_diff_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
⊢ IntegrableOn f s μ ↔ Integrable f μ

Tactic:
⟨fun h => ?_, fun h => h.integrableOn⟩

Premises used: Iff.intro, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
refine : ∀ (h : IntegrableOn f s μ), Integrable f μ
⊢ IntegrableOn f s μ ↔ Integrable f μ

Tactic:
refine ⟨fun h => ?_, fun h => h.integrableOn⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
h : IntegrableOn f s μ
⊢ Integrable f μ

Tactic:
h.integrable_of_forall_notMem_eq_zero fun x hx => ?_

Premises used: MeasureTheory.IntegrableOn.integrable_of_forall_notMem_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
h : IntegrableOn f s μ
refine : ∀ (x : α) (hx : x ∉ s), f x = 0
⊢ Integrable f μ

Tactic:
refine h.integrable_of_forall_notMem_eq_zero fun x hx => ?_

Premises used: MeasureTheory.IntegrableOn.integrable_of_forall_notMem_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
h : IntegrableOn f s μ
x : α
hx : x ∉ s
contrapose! : ∀ (hx : f x ≠ 0), x ∈ s
⊢ f x = 0

Tactic:
contrapose! hx
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
h : IntegrableOn f s μ
x : α
hx : f x ≠ 0
⊢ x ∈ s

Tactic:
h1s (mem_support.2 hx)

Premises used: Iff.mpr, Function.mem_support
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
h : IntegrableOn f s μ
x : α
hx : f x ≠ 0
⊢ x ∈ s

Tactic:
exact h1s (mem_support.2 hx)

Premises used: Iff.mpr, Function.mem_support
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (↑(↑f : α →ₘ[μ] E) : α → E) s μ

Tactic:
memLp_one_iff_integrable.mp ?_

Premises used: MeasureTheory.IntegrableOn, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : MemLp (↑(↑f : α →ₘ[μ] E) : α → E) 1 (μ.restrict s)
⊢ IntegrableOn (↑(↑f : α →ₘ[μ] E) : α → E) s μ

Tactic:
refine memLp_one_iff_integrable.mp ?_

Premises used: Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply, lt_top_iff_ne_top]

Premises used: MeasureTheory.Measure.restrict_apply, lt_top_iff_ne_top, Set.univ_inter, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hμ_restrict_univ : (μ.restrict s) Set.univ < ∞ := by
    simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply, lt_top_iff_ne_top]
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ_restrict_univ : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure (μ.restrict s)

Tactic:
haveI hμ_finite : IsFiniteMeasure (μ.restrict s) := ⟨hμ_restrict_univ⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ_restrict_univ : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ_finite : IsFiniteMeasure (μ.restrict s)
⊢ MemLp (↑(↑f : α →ₘ[μ] E) : α → E) 1 (μ.restrict s)

Tactic:
((Lp.memLp _).restrict s).mono_exponent hp

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.MemLp.mono_exponent, MeasureTheory.MemLp.restrict
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ_restrict_univ : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ_finite : IsFiniteMeasure (μ.restrict s)
⊢ MemLp (↑(↑f : α →ₘ[μ] E) : α → E) 1 (μ.restrict s)

Tactic:
exact ((Lp.memLp _).restrict s).mono_exponent hp

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.MemLp.mono_exponent, MeasureTheory.MemLp.restrict
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ < ∞

Tactic:
calc
    (∫⁻ x, ENNReal.ofReal (f x) ∂μ) ≤ ∫⁻ x, ↑‖f x‖₊ ∂μ := lintegral_ofReal_le_lintegral_enorm f
    _ < ∞ := hf.2

Premises used: Trans.trans, MeasureTheory.lintegral_ofReal_le_lintegral_enorm, And.right
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
s : Set α
hf : IntegrableOn f s μ
⊢ ∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ < ∞

Tactic:
Integrable.lintegral_lt_top hf

Premises used: MeasureTheory.Integrable.lintegral_lt_top
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
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 : IntegrableOn f s μ
⊢ IntegrableOn.{u_1, u_7} (ε := E) ((⇑L : (a : H) → E) ∘ f) s μ

Tactic:
L.integrable_comp hf

Premises used: MeasureTheory.IntegrableOn, ContinuousLinearMap.integrable_comp
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
simp_rw : (∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) ↔ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ
⊢ IntegrableAtFilter (mα := inst_2) f (map e l) (Measure.map e μ) ↔ IntegrableAtFilter (f ∘ e) l μ

Tactic:
simp_rw [IntegrableAtFilter, he.integrableOn_map_iff]

Premises used: MeasurableEmbedding.integrableOn_map_iff, MeasureTheory.IntegrableAtFilter
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
mp : (∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) → ∃ s ∈ l, IntegrableOn (f ∘ e) s μ
mpr : (∃ s ∈ l, IntegrableOn (f ∘ e) s μ) → ∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ
⊢ (∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) ↔ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
s : Set β
hs : s ∈ map e l ∧ IntegrableOn (f ∘ e) (e ⁻¹' s) μ
⊢ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ

Tactic:
⟨_, hs⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
s : Set β
hs : s ∈ map e l ∧ IntegrableOn (f ∘ e) (e ⁻¹' s) μ
⊢ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ

Tactic:
exact ⟨_, hs⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
s : Set α
hs : s ∈ l ∧ IntegrableOn (f ∘ e) s μ
rwa : e ⁻¹' e '' s ∈ l ∧ IntegrableOn (f ∘ e) (e ⁻¹' e '' s) μ
rwa₁ rwa₂ rwa₃ rwa₄ : s ∈ l ∧ IntegrableOn (f ∘ e) s μ
⊢ e '' s ∈ map e l ∧ IntegrableOn (f ∘ e) (e ⁻¹' e '' s) μ

Tactic:
rwa [mem_map, he.injective.preimage_image]

Premises used: MeasurableEmbedding.injective, Function.Injective.preimage_image, Filter.mem_map
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
s : Set α
hs : s ∈ l ∧ IntegrableOn (f ∘ e) s μ
⊢ ∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ

Tactic:
exact ⟨e '' s, by rwa [mem_map, he.injective.preimage_image]⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
simp_rw : (∃ s ∈ map e l, IntegrableOn f s μ) ↔ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
⊢ IntegrableAtFilter f (map e l) μ ↔ IntegrableAtFilter (mα := mα) (f ∘ e) l (Measure.comap e μ)

Tactic:
simp_rw [← he.integrableAtFilter_map_iff, IntegrableAtFilter, he.map_comap]

Premises used: MeasureTheory.IntegrableAtFilter, MeasurableEmbedding.integrableAtFilter_map_iff, MeasurableEmbedding.map_comap
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
mp : (∃ s ∈ map e l, IntegrableOn f s μ) → ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
mpr : (∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))) → ∃ s ∈ map e l, IntegrableOn f s μ
⊢ (∃ s ∈ map e l, IntegrableOn f s μ) ↔ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ∈ map e l
int : IntegrableOn f s μ
⊢ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))

Tactic:
⟨s, hs, int.mono_measure <| μ.restrict_le_self⟩

Premises used: MeasureTheory.Measure.restrict_le_self, And.intro, Exists.intro, MeasureTheory.IntegrableOn.mono_measure
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ∈ map e l
int : IntegrableOn f s μ
⊢ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))

Tactic:
exact ⟨s, hs, int.mono_measure <| μ.restrict_le_self⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ∈ map e l
int : IntegrableOn f s (μ.restrict (range e))
⊢ ∃ s ∈ map e l, IntegrableOn f s μ

Tactic:
⟨_, inter_mem hs range_mem_map, int.inter_of_restrict⟩

Premises used: Filter.inter_mem, MeasureTheory.IntegrableOn.inter_of_restrict, And.intro, Exists.intro, Filter.range_mem_map
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ∈ map e l
int : IntegrableOn f s (μ.restrict (range e))
⊢ ∃ s ∈ map e l, IntegrableOn f s μ

Tactic:
exact ⟨_, inter_mem hs range_mem_map, int.inter_of_restrict⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : Integrable f μ
l : Filter α
⊢ IntegrableAtFilter f l μ

Tactic:
⟨univ, Filter.univ_mem, integrableOn_univ.2 h⟩

Premises used: Iff.mpr, Set.univ, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro, Filter.univ_mem, MeasureTheory.integrableOn_univ
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
h : IntegrableAtFilter f l μ
⊢ ∀ᶠ (s : Set α) in l.smallSets, IntegrableOn f s μ

Tactic:
Iff.mpr (eventually_smallSets' fun _s _t hst ht => ht.mono_set hst) h

Premises used: Iff.mpr, MeasureTheory.IntegrableOn.mono_set, Filter.eventually_smallSets'
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
inst_4 : Nonempty α
⊢ IntegrableAtFilter f atBot μ ↔ ∃ (a : α), IntegrableOn f (Iic a) μ

Tactic:
⟨fun ⟨s, hs, hi⟩ ↦ ?_, fun ⟨a, ha⟩ ↦ ⟨Iic a, Iic_mem_atBot a, ha⟩⟩

Premises used: _private.0.MeasureTheory.integrableAtFilter_atBot_iff.match_1, Exists, MeasureTheory.IntegrableOn, MeasureTheory.IntegrableAtFilter, Filter.Iic_mem_atBot, And.intro, Iff.intro, Exists.intro, Filter.atBot, Set.Iic, _private.0.MeasureTheory.integrableAtFilter_atBot_iff.match_2
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
inst_4 : Nonempty α
refine :
  IntegrableAtFilter f atBot μ →
    ∀ (s : Set α) (hs : Membership.mem (γ := Filter α) atBot s) (hi : IntegrableOn f s μ),
      ∃ (a : α), IntegrableOn f (Iic a) μ
⊢ IntegrableAtFilter f atBot μ ↔ ∃ (a : α), IntegrableOn f (Iic a) μ

Tactic:
refine ⟨fun ⟨s, hs, hi⟩ ↦ ?_, fun ⟨a, ha⟩ ↦ ⟨Iic a, Iic_mem_atBot a, ha⟩⟩