awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f t μ
hst : s =ᶠ[ae μ] t
⊢ IntegrableOn f s μ

Tactic:
h.mono_set_ae hst.le

Premises used: Filter.EventuallyEq.le, MeasureTheory.IntegrableOn.mono_set_ae
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hst : s =ᶠ[ae μ] t
⊢ IntegrableOn f s μ ↔ IntegrableOn f t μ

Tactic:
⟨fun h ↦ h.congr_set_ae hst.symm, fun h ↦ h.congr_set_ae hst⟩

Premises used: Iff.intro, MeasureTheory.IntegrableOn.congr_set_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f g : α → ε
s : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f s μ
hst : f =ᶠ[ae (μ.restrict s)] g
⊢ IntegrableOn g s μ

Tactic:
Integrable.congr h hst

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Integrable.congr
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f g : α → ε
s : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hst : f =ᶠ[ae (μ.restrict s)] g
⊢ IntegrableOn f s μ ↔ IntegrableOn g s μ

Tactic:
⟨fun h => h.congr_fun_ae hst, fun h => h.congr_fun_ae hst.symm⟩

Premises used: MeasureTheory.IntegrableOn.congr_fun_ae, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f g : α → ε
s : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f s μ
hst : EqOn f g s
hs : MeasurableSet s
⊢ IntegrableOn g s μ

Tactic:
h.congr_fun_ae ((ae_restrict_iff' hs).2 (Eventually.of_forall hst))

Premises used: Iff.mpr, MeasureTheory.IntegrableOn.congr_fun_ae, Filter.Eventually.of_forall, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f g : α → ε
s : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hst : EqOn f g s
hs : MeasurableSet s
⊢ IntegrableOn f s μ ↔ IntegrableOn g s μ

Tactic:
⟨fun h => h.congr_fun hst hs, fun h => h.congr_fun hst.symm hs⟩

Premises used: Iff.intro, Set.EqOn.symm, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : Integrable f μ
⊢ IntegrableOn f s μ

Tactic:
h.restrict

Premises used: MeasureTheory.Integrable.restrict, MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
inst_2 : Subsingleton ε'
f : α → ε'
⊢ IntegrableOn f s μ

Tactic:
Integrable.of_subsingleton_codomain

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Integrable.of_subsingleton_codomain
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
inst_1 : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ Integrable f μ

Tactic:
⟨hf, .of_bounded hfC⟩

Premises used: MeasureTheory.Integrable, MeasureTheory.HasFiniteIntegral.of_bounded, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
s : Set α
μ : Measure α
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : α → E
hf : AEStronglyMeasurable f (μ.restrict s)
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ IntegrableOn f s μ

Tactic:
⟨hf, .restrict_of_bounded C hs hfC⟩

Premises used: MeasureTheory.HasFiniteIntegral.restrict_of_bounded, MeasureTheory.Integrable, MeasureTheory.IntegrableOn, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : Integrable f (μ.restrict s)
⊢ Integrable f ((μ.restrict t).restrict s)

Tactic:
h.mono_measure <| Measure.restrict_mono_measure Measure.restrict_le_self _

Premises used: MeasureTheory.Integrable.mono_measure, MeasureTheory.Measure.restrict_mono_measure, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : Integrable f (μ.restrict s)
⊢ Integrable f ((μ.restrict t).restrict s)

Tactic:
exact h.mono_measure <| Measure.restrict_mono_measure Measure.restrict_le_self _

Premises used: MeasureTheory.Integrable.mono_measure, MeasureTheory.Measure.restrict_mono_measure, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f s (μ.restrict t)
⊢ IntegrableOn f (s ∩ t) (μ.restrict t)

Tactic:
have := h.mono_set (inter_subset_left (t := t))
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f s (μ.restrict t)
this : IntegrableOn f (s ∩ t) (μ.restrict t)
rwa : ∀ (this : Integrable f ((μ.restrict t).restrict (s ∩ t))), IntegrableOn f (s ∩ t) μ
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : Integrable f (μ.restrict (s ∩ t))), IntegrableOn f (s ∩ t) μ
⊢ IntegrableOn f (s ∩ t) μ

Tactic:
rwa [IntegrableOn, μ.restrict_restrict_of_subset inter_subset_right] at this

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_restrict_of_subset, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f g : α → ε'
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : IntegrableOn f s μ
hg : IntegrableOn g sᶜ μ
⊢ Integrable f (μ.restrict s)

Tactic:
rw [IntegrableOn] at hf hg

Premises used: MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f g : α → ε'
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : IntegrableOn f s μ
hg : IntegrableOn g sᶜ μ
hf₁ : Integrable f (μ.restrict s)
⊢ Integrable g (μ.restrict sᶜ)

Tactic:
rw [IntegrableOn] at hf hg

Premises used: MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f g : α → ε'
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : Integrable f (μ.restrict s)
hg : Integrable g (μ.restrict sᶜ)
rw :
  ∀ (hf : MemLp f 1 (μ.restrict s)) (hg : MemLp g 1 (μ.restrict sᶜ)),
    MemLp (s.piecewise (β := fun (a : α) ↦ ε') f g) 1 μ
⊢ Integrable (s.piecewise (β := fun (a : α) ↦ ε') f g) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hg ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f g : α → ε'
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : MemLp f 1 (μ.restrict s)
hg : MemLp g 1 (μ.restrict sᶜ)
⊢ MemLp (s.piecewise (β := fun (a : α) ↦ ε') f g) 1 μ

Tactic:
MemLp.piecewise hs hf hg

Premises used: MeasureTheory.MemLp.piecewise
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f g : α → ε'
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : MemLp f 1 (μ.restrict s)
hg : MemLp g 1 (μ.restrict sᶜ)
⊢ MemLp (s.piecewise (β := fun (a : α) ↦ ε') f g) 1 μ

Tactic:
exact MemLp.piecewise hs hf hg

Premises used: MeasureTheory.MemLp.piecewise
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f (s ∪ t) μ
⊢ IntegrableOn f s μ

Tactic:
h.mono_set subset_union_left

Premises used: Set.subset_union_left, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f (s ∪ t) μ
⊢ IntegrableOn f t μ

Tactic:
h.mono_set subset_union_right

Premises used: Set.subset_union_right, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
hs : IntegrableOn f s μ
ht : IntegrableOn f t μ
⊢ IntegrableOn f (s ∪ t) μ

Tactic:
(hs.add_measure ht).mono_measure <| Measure.restrict_union_le _ _

Premises used: MeasureTheory.Integrable.mono_measure, MeasureTheory.IntegrableOn, MeasureTheory.Integrable.add_measure, MeasureTheory.Measure.restrict_union_le
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
⊢ IntegrableOn f (s ∪ t) μ ↔ IntegrableOn f s μ ∧ IntegrableOn f t μ

Tactic:
⟨fun h => ⟨h.left_of_union, h.right_of_union⟩, fun h => h.1.union h.2⟩

Premises used: MeasureTheory.IntegrableOn.right_of_union, MeasureTheory.IntegrableOn.union, And.right, And.left, And.intro, Iff.intro, MeasureTheory.IntegrableOn.left_of_union
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst_2 : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
h : ∀ (a : α) (ha : Membership.mem (γ := Set α) {x} a), f a = f x
⊢ f =ᶠ[ae (μ.restrict {x})] fun (x_1 : α) ↦ f x

Tactic:
filter_upwards [ae_restrict_mem (measurableSet_singleton x)] with _ ha

Premises used: MeasureTheory.ae_restrict_mem, MeasurableSingletonClass.measurableSet_singleton
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst_2 : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
a : α
ha : Membership.mem (γ := Set α) {x} a
⊢ f a = f x

Tactic:
simp only [mem_singleton_iff.1 ha]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst_2 : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
⊢ f =ᶠ[ae (μ.restrict {x})] fun (x_1 : α) ↦ f x

Tactic:
have : f =ᵐ[μ.restrict {x}] fun _ => f x := by
    filter_upwards [ae_restrict_mem (measurableSet_singleton x)] with _ ha
    simp only [mem_singleton_iff.1 ha]
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst_2 : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᶠ[ae (μ.restrict {x})] fun (x_1 : α) ↦ f x
rw : ‖f x‖ₑ ≠ ∞
⊢ IntegrableOn f {x} μ ↔ ‖f x‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [IntegrableOn, integrable_congr this, integrable_const_iff_enorm, isFiniteMeasure_restrict,
    lt_top_iff_ne_top]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.IntegrableOn, lt_top_iff_ne_top, MeasureTheory.isFiniteMeasure_restrict, MeasureTheory.integrable_const_iff_enorm
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst_2 : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᶠ[ae (μ.restrict {x})] fun (x_1 : α) ↦ f x
⊢ ‖f x‖ₑ ≠ ∞

Tactic:
hfx
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst_2 : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᶠ[ae (μ.restrict {x})] fun (x_1 : α) ↦ f x
⊢ ‖f x‖ₑ ≠ ∞

Tactic:
exact hfx
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst_2 : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
hx : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn f {x} μ

Tactic:
(integrableOn_singleton_iff hfx).mpr (Or.inr hx)

Premises used: Iff.mpr, MeasureTheory.integrableOn_singleton_iff, Or.inr
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
s : Set β
t : β → Set α
⊢ IntegrableOn f (⋃ (i : β), ⋃ (_ : Membership.mem (γ := Set β) ∅ i), t i) μ ↔
    ∀ (i : β), Membership.mem (γ := Set β) ∅ i → IntegrableOn f (t i) μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
s : Set β
t : β → Set α
a : β
s_1 : Set β
h : a ∉ s_1
hs : s_1.Finite
hf : IntegrableOn f (⋃ i ∈ s_1, t i) μ ↔ ∀ i ∈ s_1, IntegrableOn f (t i) μ
⊢ IntegrableOn f (⋃ i ∈ insert a s_1, t i) μ ↔ ∀ i ∈ insert a s_1, IntegrableOn f (t i) μ

Tactic:
simp [hf, or_imp, forall_and]

Premises used: or_imp, forall_and
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
s : Set β
hs : s.Finite
t : β → Set α
empty :
  IntegrableOn f (⋃ (i : β), ⋃ (_ : Membership.mem (γ := Set β) ∅ i), t i) μ ↔
    ∀ (i : β), Membership.mem (γ := Set β) ∅ i → IntegrableOn f (t i) μ
insert :
  ∀ {a : β} {s : Set β},
    a ∉ s →
      s.Finite →
        ∀ (hf : IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ),
          IntegrableOn f (⋃ i ∈ Insert.insert a s, t i) μ ↔ ∀ i ∈ Insert.insert a s, IntegrableOn f (t i) μ
⊢ IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ

Tactic:
induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hf => simp [hf, or_imp, forall_and]

Premises used: Insert.insert, or_imp, forall_and
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
s : Finset β
t : β → Set α
⊢ IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ

Tactic:
integrableOn_finite_biUnion s.finite_toSet

Premises used: Finset.finite_toSet, MeasureTheory.integrableOn_finite_biUnion
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
inst_3 : Finite β
t : β → Set α
intro : ∀ (val : Fintype β), IntegrableOn f (⋃ (i : β), t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ
⊢ IntegrableOn f (⋃ (i : β), t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
inst_3 : Finite β
t : β → Set α
val : Fintype β
⊢ IntegrableOn f (⋃ (i : β), t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ

Tactic:
simpa using integrableOn_finset_iUnion (f := f) (μ := μ) (s := Finset.univ) (t := t)

Premises used: MeasureTheory.integrableOn_finset_iUnion
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : MeasurableSingletonClass α
μ : Measure α
inst_2 : IsFiniteMeasure μ
s : Finset α
f : α → E
rw : IntegrableOn f (⋃ x ∈ (↑s : Set α), {x}) μ
⊢ IntegrableOn f (↑s : Set α) μ

Tactic:
rw [← (s : Set α).biUnion_of_singleton]

Premises used: Set.biUnion_of_singleton, SetLike.coe
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : MeasurableSingletonClass α
μ : Measure α
inst_2 : IsFiniteMeasure μ
s : Finset α
f : α → E
⊢ IntegrableOn f (⋃ x ∈ (↑s : Set α), {x}) μ

Tactic:
simp [integrableOn_finset_iUnion, measure_lt_top]

Premises used: MeasureTheory.integrableOn_finset_iUnion, MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : MeasurableSingletonClass α
μ : Measure α
inst_2 : IsFiniteMeasure μ
s : Set α
hs : s.Finite
f : α → E
⊢ IntegrableOn f s μ

Tactic:
simpa using IntegrableOn.finset (s := hs.toFinset)

Premises used: MeasureTheory.IntegrableOn.finset
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : MeasurableSingletonClass α
μ : Measure α
inst_2 : IsFiniteMeasure μ
s : Set α
hs : s.Subsingleton
f : α → E
⊢ IntegrableOn f s μ

Tactic:
.of_finite hs.finite

Premises used: MeasureTheory.IntegrableOn.of_finite, Set.Subsingleton.finite
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
hμ : IntegrableOn f s μ
hν : IntegrableOn f s ν
rw : Integrable f (μ.restrict s + ν.restrict s)
⊢ Integrable f ((μ + ν).restrict s)

Tactic:
rw [Measure.restrict_add]

Premises used: MeasureTheory.Measure.restrict_add
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
hμ : IntegrableOn f s μ
hν : IntegrableOn f s ν
⊢ Integrable f (μ.restrict s + ν.restrict s)

Tactic:
hμ.integrable.add_measure hν

Premises used: MeasureTheory.Integrable.add_measure, MeasureTheory.IntegrableOn.integrable
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
hμ : IntegrableOn f s μ
hν : IntegrableOn f s ν
⊢ Integrable f (μ.restrict s + ν.restrict s)

Tactic:
exact hμ.integrable.add_measure hν

Premises used: MeasureTheory.Integrable.add_measure, MeasureTheory.IntegrableOn.integrable
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
inst_2 : ContinuousAdd ε'
f g : α → ε'
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
⊢ IntegrableOn (f + g) s μ

Tactic:
Integrable.add hf hg

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Integrable.add
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
s : Set α
μ : Measure α
f g : α → E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
⊢ IntegrableOn (f - g) s μ

Tactic:
Integrable.sub hf hg

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
s : Set α
μ : Measure α
f : α → E
hf : IntegrableOn f s μ
⊢ IntegrableOn (-f) s μ

Tactic:
Integrable.neg hf

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
s : Set α
μ : Measure α
f : α → E
⊢ IntegrableOn (-f) s μ ↔ IntegrableOn f s μ

Tactic:
integrable_neg_iff

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.integrable_neg_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
s : Set α
μ : Measure α
f : α → E
⊢ IntegrableOn.{u_1, u_5} (ε := E) (fun (x : α) ↦ -f x) s μ ↔ IntegrableOn f s μ

Tactic:
integrable_neg_iff

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.integrable_neg_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
⊢ IntegrableOn f s (μ + ν) ↔ IntegrableOn f s μ ∧ IntegrableOn f s ν

Tactic:
⟨fun h =>
    ⟨h.mono_measure (Measure.le_add_right le_rfl), h.mono_measure (Measure.le_add_left le_rfl)⟩,
    fun h => h.1.add_measure h.2⟩

Premises used: le_rfl, MeasureTheory.IntegrableOn.add_measure, And.right, And.left, And.intro, Iff.intro, MeasureTheory.IntegrableOn.mono_measure, MeasureTheory.Measure.le_add_right, MeasureTheory.Measure.le_add_left
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure α
s : Set β
simp_rw :
  @Integrable _ _ _ _ inst_2 f (Measure.restrict (Measure.map e μ) s) ↔ Integrable (f ∘ e) (μ.restrict (e ⁻¹' s))
simp_rw₁ :
  @Integrable _ _ _ _ inst_2 f (Measure.map e (μ.restrict (e ⁻¹' s))) ↔ Integrable (f ∘ e) (μ.restrict (e ⁻¹' s))
⊢ IntegrableOn (mα := inst_2) f s (Measure.map e μ) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ

Tactic:
simp_rw [IntegrableOn, he.restrict_map, he.integrable_map_iff]

Premises used: MeasurableEmbedding.restrict_map, MeasureTheory.IntegrableOn, MeasurableEmbedding.integrable_map_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ⊆ range e
simp_rw : IntegrableOn f s μ ↔ IntegrableOn (mα := inst_2) f s (Measure.map e (Measure.comap e μ))
simp_rw₁ : IntegrableOn f s μ ↔ IntegrableOn f s (μ.restrict (range e))
simp_rw₂ : Integrable f (μ.restrict s) ↔ Integrable f ((μ.restrict (range e)).restrict s)
⊢ IntegrableOn f s μ ↔ IntegrableOn (mα := mα) (f ∘ e) (e ⁻¹' s) (Measure.comap e μ)

Tactic:
simp_rw [← he.integrableOn_map_iff, he.map_comap, IntegrableOn,
    Measure.restrict_restrict_of_subset hs]

Premises used: MeasurableEmbedding.integrableOn_map_iff, MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_restrict_of_subset, MeasurableEmbedding.map_comap