awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
rw : Integrable.{u_6, u_1} (ε := E) (fun (a : X) ↦ g a • K.indicator f a) μ
⊢ Integrable.{u_6, u_1} (ε := E) (fun (x : X) ↦ g x • f x) μ

Tactic:
rw [← this, indicator_smul]

Premises used: Set.indicator_smul
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
hf₁ : Integrable (K.indicator f) μ
hφ : MemLp g ∞ μ
⊢ Integrable.{u_6, u_1} (ε := E) (fun (a : X) ↦ g a • K.indicator f a) μ

Tactic:
apply Integrable.smul_of_top_right

Premises used: MeasureTheory.Integrable.smul_of_top_right
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
hf₁ : IntegrableOn f K μ
⊢ Integrable (K.indicator f) μ

Tactic:
rw [integrable_indicator_iff hK.measurableSet]

Premises used: MeasureTheory.integrable_indicator_iff, IsCompact.measurableSet
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
⊢ IntegrableOn f K μ

Tactic:
hf.integrableOn_isCompact hK

Premises used: MeasureTheory.LocallyIntegrable.integrableOn_isCompact
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
⊢ IntegrableOn f K μ

Tactic:
exact hf.integrableOn_isCompact hK

Premises used: MeasureTheory.LocallyIntegrable.integrableOn_isCompact
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
⊢ MemLp g ∞ μ

Tactic:
hg.memLp_top_of_hasCompactSupport h'g μ

Premises used: Continuous.memLp_top_of_hasCompactSupport
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
⊢ MemLp g ∞ μ

Tactic:
exact hg.memLp_top_of_hasCompactSupport h'g μ

Premises used: Continuous.memLp_top_of_hasCompactSupport
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
⊢ IsCompact K

Tactic:
have hK : IsCompact K := h'g
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
apply : (support.{u_1, u_6} (M := E) fun (x : X) ↦ f x • g x) ⊆ K
⊢ Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x

Tactic:
apply indicator_eq_self.2

Premises used: Iff.mpr, Set.indicator_eq_self
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
apply : ∀ x ∉ K, f x • g x = 0
⊢ (support.{u_1, u_6} (M := E) fun (x : X) ↦ f x • g x) ⊆ K

Tactic:
apply support_subset_iff'.2

Premises used: Iff.mpr, Function.support_subset_iff'
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
x : X
hx : x ∉ K
⊢ f x • g x = 0

Tactic:
simp [image_eq_zero_of_notMem_tsupport hx]

Premises used: image_eq_zero_of_notMem_tsupport
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x

Tactic:
have : K.indicator (fun x ↦ f x • g x) = (fun x ↦ f x • g x) := by
    apply indicator_eq_self.2
    apply support_subset_iff'.2
    intro x hx
    simp [image_eq_zero_of_notMem_tsupport hx]
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
rw : Integrable.{u_6, u_1} (ε := E) (fun (a : X) ↦ K.indicator f a • g a) μ
⊢ Integrable.{u_6, u_1} (ε := E) (fun (x : X) ↦ f x • g x) μ

Tactic:
rw [← this, indicator_smul_left]

Premises used: Set.indicator_smul_left
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
hφ : Integrable (K.indicator f) μ
hf₁ : MemLp g ∞ μ
⊢ Integrable.{u_6, u_1} (ε := E) (fun (a : X) ↦ K.indicator f a • g a) μ

Tactic:
apply Integrable.smul_of_top_left

Premises used: MeasureTheory.Integrable.smul_of_top_left
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
hφ : IntegrableOn f K μ
⊢ Integrable (K.indicator f) μ

Tactic:
rw [integrable_indicator_iff hK.measurableSet]

Premises used: MeasureTheory.integrable_indicator_iff, IsCompact.measurableSet
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
⊢ IntegrableOn f K μ

Tactic:
hf.integrableOn_isCompact hK

Premises used: MeasureTheory.LocallyIntegrable.integrableOn_isCompact
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
⊢ IntegrableOn f K μ

Tactic:
exact hf.integrableOn_isCompact hK

Premises used: MeasureTheory.LocallyIntegrable.integrableOn_isCompact
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
⊢ MemLp g ∞ μ

Tactic:
hg.memLp_top_of_hasCompactSupport h'g μ

Premises used: Continuous.memLp_top_of_hasCompactSupport
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
⊢ MemLp g ∞ μ

Tactic:
exact hg.memLp_top_of_hasCompactSupport h'g μ

Premises used: Continuous.memLp_top_of_hasCompactSupport
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
⊢ Integrable f μ ↔ IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ

Tactic:
⟨fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩, fun ⟨⟨s, hsc, hs⟩, hloc⟩ ↦ ?_⟩

Premises used: MeasureTheory.Integrable, MeasureTheory.Integrable.integrableAtFilter, Filter.cocompact, MeasureTheory.Integrable.locallyIntegrable, _private.0.MeasureTheory.integrable_iff_integrableAtFilter_cocompact.match_1, And.intro, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
refine :
  IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ →
    ∀ (s : Set X) (hsc : s ∈ cocompact X) (hs : IntegrableOn f s μ) (hloc : LocallyIntegrable f μ), Integrable f μ
⊢ Integrable f μ ↔ IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ

Tactic:
refine ⟨fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩, fun ⟨⟨s, hsc, hs⟩, hloc⟩ ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
h : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
obtain : ∀ (t : Set X) (htc : IsCompact t) (ht : sᶜ ⊆ t), Integrable f μ
⊢ Integrable f μ

Tactic:
obtain ⟨t, htc, ht⟩ := mem_cocompact'.mp hsc

Premises used: Iff.mp, Filter.mem_cocompact'
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
h : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
t : Set X
htc : IsCompact t
ht : sᶜ ⊆ t
rewrite : IntegrableOn f sᶜ μ ∧ IntegrableOn f s μ
⊢ Integrable f μ

Tactic:
rewrite [← integrableOn_univ, ← compl_union_self s, integrableOn_union]

Premises used: MeasureTheory.integrableOn_union, Set.compl_union_self, MeasureTheory.integrableOn_univ
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
h : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
t : Set X
htc : IsCompact t
ht : sᶜ ⊆ t
⊢ IntegrableOn f sᶜ μ ∧ IntegrableOn f s μ

Tactic:
⟨(hloc.integrableOn_isCompact htc).mono ht le_rfl, hs⟩

Premises used: le_rfl, MeasureTheory.LocallyIntegrable.integrableOn_isCompact, And.intro, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
h : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
t : Set X
htc : IsCompact t
ht : sᶜ ⊆ t
⊢ IntegrableOn f sᶜ μ ∧ IntegrableOn f s μ

Tactic:
exact ⟨(hloc.integrableOn_isCompact htc).mono ht le_rfl, hs⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
inst_4 : PseudoMetrizableSpace ε''
f : X → ε''
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
mp : Integrable f μ → (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
mpr : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ
⊢ Integrable f μ ↔ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
inst_4 : PseudoMetrizableSpace ε''
f : X → ε''
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
⊢ Integrable f μ → (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ

Tactic:
fun hf ↦ ⟨⟨hf.integrableAtFilter _, hf.integrableAtFilter _⟩, hf.locallyIntegrable⟩

Premises used: MeasureTheory.Integrable.integrableAtFilter, Filter.atTop, MeasureTheory.Integrable.locallyIntegrable, And.intro, Filter.atBot
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
inst_4 : PseudoMetrizableSpace ε''
f : X → ε''
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
⊢ Integrable f μ → (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ

Tactic:
exact fun hf ↦ ⟨⟨hf.integrableAtFilter _, hf.integrableAtFilter _⟩, hf.locallyIntegrable⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
inst_4 : PseudoMetrizableSpace ε''
f : X → ε''
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
⊢ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ

Tactic:
fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩

Premises used: Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_cocompact, And.right, And.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
inst_4 : PseudoMetrizableSpace ε''
f : X → ε''
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
mpr :
  ∀ (h : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ),
    IntegrableAtFilter f (cocompact X) μ
⊢ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ

Tactic:
refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩

Premises used: Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_cocompact, And.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
inst_4 : PseudoMetrizableSpace ε''
f : X → ε''
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
h : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ

Tactic:
(IntegrableAtFilter.sup_iff.mpr h.1).filter_mono cocompact_le_atBot_atTop

Premises used: Iff.mpr, And.left, cocompact_le_atBot_atTop, MeasureTheory.IntegrableAtFilter.filter_mono, MeasureTheory.IntegrableAtFilter.sup_iff
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
inst_4 : PseudoMetrizableSpace ε''
f : X → ε''
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
h : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ

Tactic:
exact (IntegrableAtFilter.sup_iff.mpr h.1).filter_mono cocompact_le_atBot_atTop

Premises used: Iff.mpr, And.left, cocompact_le_atBot_atTop, MeasureTheory.IntegrableAtFilter.filter_mono, MeasureTheory.IntegrableAtFilter.sup_iff
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LinearOrder X
inst_6 : OrderTop X
inst_7 : CompactIccSpace X
mp : Integrable f μ → IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
mpr : IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ
⊢ Integrable f μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LinearOrder X
inst_6 : OrderTop X
inst_7 : CompactIccSpace X
⊢ Integrable f μ → IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ

Tactic:
fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩

Premises used: MeasureTheory.Integrable.integrableAtFilter, MeasureTheory.Integrable.locallyIntegrable, And.intro, Filter.atBot
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LinearOrder X
inst_6 : OrderTop X
inst_7 : CompactIccSpace X
⊢ Integrable f μ → IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ

Tactic:
exact fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩