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
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
a b : X
xab : x ∈ Icc a b
hab : Icc a b ∈ 𝓝 x
abU : Icc a b ⊆ U
⊢ a ≤ b

Tactic:
have ab : a ≤ b := xab.1.trans xab.2
-- 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
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
a b : X
xab : x ∈ Icc a b
hab : Icc a b ∈ 𝓝 x
abU : Icc a b ⊆ U
ab : a ≤ b
⊢ IntegrableAtFilter f (𝓝 x) μ

Tactic:
⟨Icc a b, hab, ?_⟩

Premises used: MeasureTheory.IntegrableAtFilter, Set.Icc, And.intro, Exists.intro
-- 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
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
a b : X
xab : x ∈ Icc a b
hab : Icc a b ∈ 𝓝 x
abU : Icc a b ⊆ U
ab : a ≤ b
refine : IntegrableOn f (Icc a b) μ
⊢ IntegrableAtFilter f (𝓝 x) μ

Tactic:
refine ⟨Icc a b, hab, ?_⟩
-- 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
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
a b : X
xab : x ∈ Icc a b
hab : Icc a b ∈ 𝓝 x
abU : Icc a b ⊆ U
ab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ

Tactic:
(hmono.monotoneOn _).integrableOn_of_measure_ne_top (isLeast_Icc ab) (isGreatest_Icc ab)
      ((measure_mono abU).trans_lt h'U).ne measurableSet_Icc

Premises used: isLeast_Icc, measurableSet_Icc, MeasureTheory.measure_mono, MonotoneOn.integrableOn_of_measure_ne_top, isGreatest_Icc, Monotone.monotoneOn, LE.le.trans_lt, LT.lt.ne
-- 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
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
a b : X
xab : x ∈ Icc a b
hab : Icc a b ∈ 𝓝 x
abU : Icc a b ⊆ U
ab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ

Tactic:
exact
    (hmono.monotoneOn _).integrableOn_of_measure_ne_top (isLeast_Icc ab) (isGreatest_Icc ab)
      ((measure_mono abU).trans_lt h'U).ne measurableSet_Icc

Premises used: isLeast_Icc, measurableSet_Icc, MeasureTheory.measure_mono, MonotoneOn.integrableOn_of_measure_ne_top, isGreatest_Icc, Monotone.monotoneOn, LE.le.trans_lt, LT.lt.ne
-- 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
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hanti : Antitone f
⊢ LocallyIntegrable f μ

Tactic:
hanti.dual_right.locallyIntegrable

Premises used: Monotone.locallyIntegrable, Antitone.dual_right, OrderDual
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
A K : Set X
inst_3 : NormedRing R
inst_4 : SecondCountableTopologyEither X R
g g' : X → R
hg : IntegrableOn g A μ
hg' : ContinuousOn g' K
hA : MeasurableSet A
hK : IsCompact K
hAK : A ⊆ K
rcases : ∀ (C : ℝ) (hC : ∀ x ∈ K, ‖g' x‖ ≤ C), IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ
⊢ IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ

Tactic:
rcases IsCompact.exists_bound_of_continuousOn hK hg' with ⟨C, hC⟩

Premises used: IsCompact.exists_bound_of_continuousOn
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
A K : Set X
inst_3 : NormedRing R
inst_4 : SecondCountableTopologyEither X R
g g' : X → R
hg : IntegrableOn g A μ
hg' : ContinuousOn g' K
hA : MeasurableSet A
hK : IsCompact K
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g' x‖ ≤ C
⊢ IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ

Tactic:
hg.mul_bdd ((hg'.mono hAK).aestronglyMeasurable hA)
    (ae_restrict_of_forall_mem hA fun x hx => hC x (hAK hx))

Premises used: MeasureTheory.ae_restrict_of_forall_mem, MeasureTheory.IntegrableOn, ContinuousOn.aestronglyMeasurable, MeasureTheory.Integrable.mul_bdd, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
A K : Set X
inst_3 : NormedRing R
inst_4 : SecondCountableTopologyEither X R
g g' : X → R
hg : IntegrableOn g A μ
hg' : ContinuousOn g' K
hA : MeasurableSet A
hK : IsCompact K
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g' x‖ ≤ C
⊢ IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ

Tactic:
exact hg.mul_bdd ((hg'.mono hAK).aestronglyMeasurable hA)
    (ae_restrict_of_forall_mem hA fun x hx => hC x (hAK hx))

Premises used: MeasureTheory.ae_restrict_of_forall_mem, ContinuousOn.aestronglyMeasurable, MeasureTheory.Integrable.mul_bdd, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
K : Set X
inst_3 : NormedRing R
inst_4 : SecondCountableTopologyEither X R
g g' : X → R
inst_5 : T2Space X
hg : IntegrableOn g K μ
hg' : ContinuousOn g' K
hK : IsCompact K
⊢ IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) K μ

Tactic:
hg.mul_continuousOn_of_subset hg' hK.measurableSet hK (Subset.refl _)

Premises used: Set.Subset.refl, MeasureTheory.IntegrableOn.mul_continuousOn_of_subset, IsCompact.measurableSet
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
A K : Set X
inst_3 : NormedRing R
inst_4 : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : IntegrableOn g' A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
rcases : ∀ (C : ℝ) (hC : ∀ x ∈ K, ‖g x‖ ≤ C), IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ
⊢ IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ

Tactic:
rcases IsCompact.exists_bound_of_continuousOn hK hg with ⟨C, hC⟩

Premises used: IsCompact.exists_bound_of_continuousOn
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
A K : Set X
inst_3 : NormedRing R
inst_4 : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : IntegrableOn g' A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
⊢ IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ

Tactic:
hg'.bdd_mul ((hg.mono hAK).aestronglyMeasurable hA)
    (ae_restrict_of_forall_mem hA fun x hx => hC x (hAK hx))

Premises used: MeasureTheory.Integrable.bdd_mul, MeasureTheory.ae_restrict_of_forall_mem, MeasureTheory.IntegrableOn, ContinuousOn.aestronglyMeasurable, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
A K : Set X
inst_3 : NormedRing R
inst_4 : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : IntegrableOn g' A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
⊢ IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ

Tactic:
exact hg'.bdd_mul ((hg.mono hAK).aestronglyMeasurable hA)
    (ae_restrict_of_forall_mem hA fun x hx => hC x (hAK hx))

Premises used: MeasureTheory.Integrable.bdd_mul, MeasureTheory.ae_restrict_of_forall_mem, ContinuousOn.aestronglyMeasurable, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
K : Set X
inst_3 : NormedRing R
inst_4 : SecondCountableTopologyEither X R
g g' : X → R
inst_5 : T2Space X
hg : ContinuousOn g K
hg' : IntegrableOn g' K μ
hK : IsCompact K
⊢ IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) K μ

Tactic:
hg'.continuousOn_mul_of_subset hg hK hK.measurableSet Subset.rfl

Premises used: MeasureTheory.IntegrableOn.continuousOn_mul_of_subset, Set.Subset.rfl, 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
inst_3 : OpensMeasurableSpace X
A K : Set X
𝕜 : Type u_9
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : SecondCountableTopologyEither X 𝕜
f : X → 𝕜
hf : ContinuousOn f K
g : X → E
hg : IntegrableOn g A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
rcases : ∀ (C : ℝ) (hC : ∀ x ∈ K, ‖f x‖ ≤ C), IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ
⊢ IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ

Tactic:
rcases IsCompact.exists_bound_of_continuousOn hK hf with ⟨C, hC⟩

Premises used: IsCompact.exists_bound_of_continuousOn
-- 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
inst_3 : OpensMeasurableSpace X
A K : Set X
𝕜 : Type u_9
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : SecondCountableTopologyEither X 𝕜
f : X → 𝕜
hf : ContinuousOn f K
g : X → E
hg : IntegrableOn g A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖f x‖ ≤ C
⊢ IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ

Tactic:
hg.bdd_smul C ((hf.mono hAK).aestronglyMeasurable hA)
    (ae_restrict_of_forall_mem hA fun x hx => hC x (hAK hx))

Premises used: MeasureTheory.ae_restrict_of_forall_mem, MeasureTheory.IntegrableOn, ContinuousOn.aestronglyMeasurable, MeasureTheory.Integrable.bdd_smul, ContinuousOn.mono
-- 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
inst_3 : OpensMeasurableSpace X
A K : Set X
𝕜 : Type u_9
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : SecondCountableTopologyEither X 𝕜
f : X → 𝕜
hf : ContinuousOn f K
g : X → E
hg : IntegrableOn g A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖f x‖ ≤ C
⊢ IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ

Tactic:
exact hg.bdd_smul C ((hf.mono hAK).aestronglyMeasurable hA)
    (ae_restrict_of_forall_mem hA fun x hx => hC x (hAK hx))

Premises used: MeasureTheory.ae_restrict_of_forall_mem, ContinuousOn.aestronglyMeasurable, MeasureTheory.Integrable.bdd_smul, ContinuousOn.mono
-- 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
inst_3 : OpensMeasurableSpace X
K : Set X
𝕜 : Type u_9
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : T2Space X
inst_8 : SecondCountableTopologyEither X 𝕜
g : X → E
hg : IntegrableOn g K μ
f : X → 𝕜
hf : ContinuousOn f K
hK : IsCompact K
⊢ IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) K μ

Tactic:
hg.continuousOn_smul_of_subset hf hK hK.measurableSet Subset.rfl

Premises used: Set.Subset.rfl, MeasureTheory.IntegrableOn.continuousOn_smul_of_subset, 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
inst_3 : OpensMeasurableSpace X
A K : Set X
𝕜 : Type u_9
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f A μ
g : X → E
hg : ContinuousOn g K
hA : MeasurableSet A
hK : IsCompact K
hAK : A ⊆ K
rcases : ∀ (C : ℝ) (hC : ∀ x ∈ K, ‖g x‖ ≤ C), IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ
⊢ IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ

Tactic:
rcases IsCompact.exists_bound_of_continuousOn hK hg with ⟨C, hC⟩

Premises used: IsCompact.exists_bound_of_continuousOn
-- 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
inst_3 : OpensMeasurableSpace X
A K : Set X
𝕜 : Type u_9
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f A μ
g : X → E
hg : ContinuousOn g K
hA : MeasurableSet A
hK : IsCompact K
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
⊢ IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ

Tactic:
hf.smul_bdd C ((hg.mono hAK).aestronglyMeasurable hA)
    (ae_restrict_of_forall_mem hA fun x hx => hC x (hAK hx))

Premises used: MeasureTheory.Integrable.smul_bdd, MeasureTheory.ae_restrict_of_forall_mem, MeasureTheory.IntegrableOn, ContinuousOn.aestronglyMeasurable, ContinuousOn.mono
-- 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
inst_3 : OpensMeasurableSpace X
A K : Set X
𝕜 : Type u_9
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f A μ
g : X → E
hg : ContinuousOn g K
hA : MeasurableSet A
hK : IsCompact K
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
⊢ IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ

Tactic:
exact hf.smul_bdd C ((hg.mono hAK).aestronglyMeasurable hA)
    (ae_restrict_of_forall_mem hA fun x hx => hC x (hAK hx))

Premises used: MeasureTheory.Integrable.smul_bdd, MeasureTheory.ae_restrict_of_forall_mem, ContinuousOn.aestronglyMeasurable, ContinuousOn.mono
-- 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
inst_3 : OpensMeasurableSpace X
K : Set X
𝕜 : Type u_9
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : T2Space X
inst_8 : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f K μ
g : X → E
hg : ContinuousOn g K
hK : IsCompact K
⊢ IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) K μ

Tactic:
hf.smul_continuousOn_of_subset hg hK.measurableSet hK (Subset.refl _)

Premises used: Set.Subset.refl, MeasureTheory.IntegrableOn.smul_continuousOn_of_subset, IsCompact.measurableSet
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
inst_3 : LocallyCompactSpace X
inst_4 : T2Space X
inst_5 : NormedRing R
inst_6 : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
rw :
  ∀ (hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ) (hg : ContinuousOn g s) (hs : IsLocallyClosed s),
    ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * f x) k μ
⊢ LocallyIntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * f x) s μ

Tactic:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

Premises used: MeasureTheory.locallyIntegrableOn_iff
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
inst_3 : LocallyCompactSpace X
inst_4 : T2Space X
inst_5 : NormedRing R
inst_6 : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * f x) k μ

Tactic:
fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_mul (hg.mono hk_sub) hk_c

Premises used: MeasureTheory.IntegrableOn.continuousOn_mul, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
inst_3 : LocallyCompactSpace X
inst_4 : T2Space X
inst_5 : NormedRing R
inst_6 : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * f x) k μ

Tactic:
exact fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_mul (hg.mono hk_sub) hk_c

Premises used: MeasureTheory.IntegrableOn.continuousOn_mul, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
inst_3 : LocallyCompactSpace X
inst_4 : T2Space X
inst_5 : NormedRing R
inst_6 : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
rw :
  ∀ (hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ) (hg : ContinuousOn g s) (hs : IsLocallyClosed s),
    ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ f x * g x) k μ
⊢ LocallyIntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ f x * g x) s μ

Tactic:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

Premises used: MeasureTheory.locallyIntegrableOn_iff
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
inst_3 : LocallyCompactSpace X
inst_4 : T2Space X
inst_5 : NormedRing R
inst_6 : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ f x * g x) k μ

Tactic:
fun k hk_sub hk_c => (hf k hk_sub hk_c).mul_continuousOn (hg.mono hk_sub) hk_c

Premises used: ContinuousOn.mono, MeasureTheory.IntegrableOn.mul_continuousOn
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
inst_3 : LocallyCompactSpace X
inst_4 : T2Space X
inst_5 : NormedRing R
inst_6 : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ f x * g x) k μ

Tactic:
exact fun k hk_sub hk_c => (hf k hk_sub hk_c).mul_continuousOn (hg.mono hk_sub) hk_c

Premises used: ContinuousOn.mono, MeasureTheory.IntegrableOn.mul_continuousOn
-- 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
inst_3 : OpensMeasurableSpace X
inst_4 : LocallyCompactSpace X
inst_5 : T2Space X
𝕜 : Type u_9
inst_6 : NormedRing 𝕜
inst_7 : SecondCountableTopologyEither X 𝕜
inst_8 : Module 𝕜 E
inst_9 : NormSMulClass 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsLocallyClosed s
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
rw :
  ∀ (hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ) (hg : ContinuousOn g s),
    ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ g x • f x) k μ
⊢ LocallyIntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ g x • f x) s μ

Tactic:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

Premises used: MeasureTheory.locallyIntegrableOn_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
inst_3 : OpensMeasurableSpace X
inst_4 : LocallyCompactSpace X
inst_5 : T2Space X
𝕜 : Type u_9
inst_6 : NormedRing 𝕜
inst_7 : SecondCountableTopologyEither X 𝕜
inst_8 : Module 𝕜 E
inst_9 : NormSMulClass 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ g x • f x) k μ

Tactic:
fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_smul (hg.mono hk_sub) hk_c

Premises used: MeasureTheory.IntegrableOn.continuousOn_smul, ContinuousOn.mono
-- 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
inst_3 : OpensMeasurableSpace X
inst_4 : LocallyCompactSpace X
inst_5 : T2Space X
𝕜 : Type u_9
inst_6 : NormedRing 𝕜
inst_7 : SecondCountableTopologyEither X 𝕜
inst_8 : Module 𝕜 E
inst_9 : NormSMulClass 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ g x • f x) k μ

Tactic:
exact fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_smul (hg.mono hk_sub) hk_c

Premises used: MeasureTheory.IntegrableOn.continuousOn_smul, ContinuousOn.mono
-- 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
inst_3 : OpensMeasurableSpace X
inst_4 : LocallyCompactSpace X
inst_5 : T2Space X
𝕜 : Type u_9
inst_6 : NormedRing 𝕜
inst_7 : SecondCountableTopologyEither X E
inst_8 : Module 𝕜 E
inst_9 : NormSMulClass 𝕜 E
f : X → 𝕜
g : X → E
s : Set X
hs : IsLocallyClosed s
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
rw :
  ∀ (hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ) (hg : ContinuousOn g s),
    ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) k μ
⊢ LocallyIntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) s μ

Tactic:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

Premises used: MeasureTheory.locallyIntegrableOn_iff