awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 β
rw :
  IntegrableOn (mα := mα) (f ∘ e) (e ⁻¹' range e) (Measure.comap e μ) ↔
    @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ)
rw₁ : IntegrableOn (mα := mα) (f ∘ e) univ (Measure.comap e μ) ↔ @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ)
rw₂ rw₃ : @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ) ↔ @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ)
⊢ IntegrableOn f (range e) μ ↔ @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ)

Tactic:
rw [he.integrableOn_iff_comap .rfl, preimage_range, integrableOn_univ]

Premises used: Set.preimage_range, Set.Subset.rfl, MeasurableEmbedding.integrableOn_iff_comap, MeasureTheory.integrableOn_univ
-- 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 : α ≃ᵐ β
f : β → ε
μ : Measure α
s : Set β
⊢ IntegrableOn (mα := inst_2) f s (Measure.map (⇑e : (a : α) → β) μ) ↔
    IntegrableOn (f ∘ (⇑e : (a : α) → β)) ((⇑e : (a : α) → β) ⁻¹' s) μ

Tactic:
simp only [IntegrableOn, e.restrict_map, integrable_map_equiv e]

Premises used: MeasureTheory.integrable_map_equiv, MeasurableEquiv.restrict_map, MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : MeasurableSpace β
e : α → β
ν : Measure β
h₁ : MeasurePreserving e μ ν
h₂ : MeasurableEmbedding e
f : β → ε
s : Set β
⊢ IntegrableOn (f ∘ e) (e ⁻¹' s) μ ↔ IntegrableOn f s ν

Tactic:
(h₁.restrict_preimage_emb h₂ s).integrable_comp_emb h₂

Premises used: MeasureTheory.MeasurePreserving.integrable_comp_emb, MeasureTheory.IntegrableOn, MeasureTheory.MeasurePreserving.restrict_preimage_emb
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : MeasurableSpace β
e : α → β
ν : Measure β
h₁ : MeasurePreserving e μ ν
h₂ : MeasurableEmbedding e
f : β → ε
s : Set α
⊢ IntegrableOn f (e '' s) ν ↔ IntegrableOn (f ∘ e) s μ

Tactic:
((h₁.restrict_image_emb h₂ s).integrable_comp_emb h₂).symm

Premises used: MeasureTheory.MeasurePreserving.integrable_comp_emb, MeasureTheory.MeasurePreserving.restrict_image_emb, MeasureTheory.IntegrableOn, Iff.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hs : MeasurableSet s
simp_rw : Integrable (s.indicator f) μ ↔ Integrable f (μ.restrict s)
simp_rw₁ :
  AEStronglyMeasurable (s.indicator f) μ ∧ HasFiniteIntegral (s.indicator f) μ ↔
    AEStronglyMeasurable f (μ.restrict s) ∧ HasFiniteIntegral f (μ.restrict s)
simp_rw₂ :
  AEStronglyMeasurable (s.indicator f) μ ∧ ∫⁻ (a : α), ‖s.indicator f a‖ₑ ∂μ < ∞ ↔
    AEStronglyMeasurable f (μ.restrict s) ∧ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ < ∞
simp_rw₃ :
  AEStronglyMeasurable (s.indicator f) μ ∧ ∫⁻ (a : α), s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a ∂μ < ∞ ↔
    AEStronglyMeasurable f (μ.restrict s) ∧ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ < ∞
simp_rw₄ :
  AEStronglyMeasurable (s.indicator f) μ ∧ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ < ∞ ↔
    AEStronglyMeasurable f (μ.restrict s) ∧ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ < ∞
⊢ Integrable (s.indicator f) μ ↔ IntegrableOn f s μ

Tactic:
simp_rw [IntegrableOn, Integrable, hasFiniteIntegral_iff_enorm,
    enorm_indicator_eq_indicator_enorm, lintegral_indicator hs,
    aestronglyMeasurable_indicator_iff hs]

Premises used: MeasureTheory.Integrable, MeasureTheory.IntegrableOn, MeasureTheory.lintegral_indicator, MeasureTheory.hasFiniteIntegral_iff_enorm, enorm_indicator_eq_indicator_enorm, aestronglyMeasurable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
h : IntegrableOn f s μ
hs : MeasurableSet s
⊢ Integrable (s.indicator f) μ

Tactic:
(integrable_indicator_iff hs).2 h

Premises used: Iff.mpr, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
h : IntegrableOn f s μ
hs : NullMeasurableSet s μ
⊢ Integrable (s.indicator f) μ

Tactic:
(h.congr_set_ae hs.toMeasurable_ae_eq).integrable_indicator
    (measurableSet_toMeasurable μ s) |>.congr
    (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq)

Premises used: MeasureTheory.IntegrableOn.integrable_indicator, indicator_ae_eq_of_ae_eq_set, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.Integrable.congr, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, MeasureTheory.IntegrableOn.congr_set_ae
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
h : Integrable f μ
hs : MeasurableSet s
⊢ Integrable (s.indicator f) μ

Tactic:
h.integrableOn.integrable_indicator hs

Premises used: MeasureTheory.IntegrableOn.integrable_indicator, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
h : Integrable f μ
hs : NullMeasurableSet s μ
⊢ Integrable (s.indicator f) μ

Tactic:
h.integrableOn.integrable_indicator₀ hs

Premises used: MeasureTheory.IntegrableOn.integrable_indicator₀, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s t : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
h : IntegrableOn f s μ
ht : MeasurableSet t
⊢ IntegrableOn (t.indicator f) s μ

Tactic:
Integrable.indicator h ht

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
rw : c = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) μ

Tactic:
rw [integrable_congr indicatorConstLp_coeFn, integrable_indicator_iff hs, IntegrableOn,
    integrable_const_iff, isFiniteMeasure_restrict]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.IntegrableOn, MeasureTheory.isFiniteMeasure_restrict, MeasureTheory.integrable_const_iff, MeasureTheory.indicatorConstLp_coeFn, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ c = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
.inr hμs

Premises used: Or.inr
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ c = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact .inr hμs
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s t : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hs : MeasurableSet s
simp_rw : Integrable (s.indicator f) (μ.restrict t) ↔ Integrable f (μ.restrict (s ∩ t))
simp_rw₁ : IntegrableOn f s (μ.restrict t) ↔ Integrable f (μ.restrict (s ∩ t))
simp_rw₂ : Integrable f ((μ.restrict t).restrict s) ↔ Integrable f (μ.restrict (s ∩ t))
⊢ IntegrableOn (s.indicator f) t μ ↔ IntegrableOn f (s ∩ t) μ

Tactic:
simp_rw [IntegrableOn, integrable_indicator_iff hs, IntegrableOn, Measure.restrict_restrict hs]

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_restrict, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
rcases :
  ∀ (u : ℕ → ℝ≥0∞),
    StrictAnti u →
      ∀ (u_pos : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) (u n)) (u_lim : Tendsto u atTop (𝓝 0)),
        μ.restrict (toMeasurable μ s) = μ.restrict s
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s

Tactic:
rcases exists_seq_strictAnti_tendsto' ENNReal.zero_lt_top with ⟨u, _, u_pos, u_lim⟩

Premises used: exists_seq_strictAnti_tendsto', ENNReal.zero_lt_top
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left : StrictAnti u
u_pos : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable (μ.restrict s) {x : α | u n ≤ ‖f x‖ₑ}
n : ℕ
rw : Ne (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | u n ≤ ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [inter_comm, ← Measure.restrict_apply (measurableSet_toMeasurable _ _),
      measure_toMeasurable]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.measure_toMeasurable, Set.inter_comm, MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left : StrictAnti u
u_pos : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable (μ.restrict s) {x : α | u n ≤ ‖f x‖ₑ}
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | u n ≤ ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(hf.measure_enorm_ge_lt_top (u_pos n).1 (u_pos n).2.ne).ne

Premises used: MeasureTheory.Integrable.measure_enorm_ge_lt_top, And.right, And.left, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left : StrictAnti u
u_pos : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable (μ.restrict s) {x : α | u n ≤ ‖f x‖ₑ}
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | u n ≤ ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact (hf.measure_enorm_ge_lt_top (u_pos n).1 (u_pos n).2.ne).ne

Premises used: MeasureTheory.Integrable.measure_enorm_ge_lt_top, And.right, And.left, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left : StrictAnti u
u_pos : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable (μ.restrict s) {x : α | u n ≤ ‖f x‖ₑ}
⊢ ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have A : ∀ n, μ (s ∩ v n) ≠ ∞ := by
    intro n
    rw [inter_comm, ← Measure.restrict_apply (measurableSet_toMeasurable _ _),
      measure_toMeasurable]
    exact (hf.measure_enorm_ge_lt_top (u_pos n).1 (u_pos n).2.ne).ne
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left : StrictAnti u
u_pos : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable (μ.restrict s) {x : α | u n ≤ ‖f x‖ₑ}
A : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
apply : s ⊆ ⋃ (n : ℕ), v n
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s

Tactic:
apply Measure.restrict_toMeasurable_of_cover _ A

Premises used: MeasureTheory.Measure.restrict_toMeasurable_of_cover
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left : StrictAnti u
u_pos : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable (μ.restrict s) {x : α | u n ≤ ‖f x‖ₑ}
A : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∈ s
⊢ ∃ (n : ℕ), u n < ‖f x‖ₑ

Tactic:
((tendsto_order.1 u_lim).2 _ (pos_of_ne_zero (h's x hx))).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.right, pos_of_ne_zero, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left : StrictAnti u
u_pos : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable (μ.restrict s) {x : α | u n ≤ ‖f x‖ₑ}
A : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∈ s
obtain : ∀ (n : ℕ) (hn : u n < ‖f x‖ₑ), Membership.mem (γ := Set α) (⋃ (n : ℕ), v n) x
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), v n) x

Tactic:
obtain ⟨n, hn⟩ : ∃ n, u n < ‖f x‖ₑ :=
    ((tendsto_order.1 u_lim).2 _ (pos_of_ne_zero (h's x hx))).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.right, pos_of_ne_zero, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left : StrictAnti u
u_pos : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable (μ.restrict s) {x : α | u n ≤ ‖f x‖ₑ}
A : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∈ s
n : ℕ
hn : u n < ‖f x‖ₑ
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), v n) x

Tactic:
mem_iUnion.2 ⟨n, subset_toMeasurable _ _ hn.le⟩

Premises used: Iff.mpr, Set.mem_iUnion, LT.lt.le, MeasureTheory.subset_toMeasurable, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left : StrictAnti u
u_pos : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable (μ.restrict s) {x : α | u n ≤ ‖f x‖ₑ}
A : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∈ s
n : ℕ
hn : u n < ‖f x‖ₑ
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), v n) x

Tactic:
exact mem_iUnion.2 ⟨n, subset_toMeasurable _ _ hn.le⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- 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}
⊢ IntegrableOn f u μ

Tactic:
have hu : IntegrableOn f u μ := hf.mono_set fun x hx => hx.1
-- 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
rw : Integrable f (μ.restrict u)
rw₁ : ∀ x ∈ u, ‖f x‖ₑ ≠ 0
⊢ IntegrableOn f v μ

Tactic:
rw [IntegrableOn, hu.restrict_toMeasurable]

Premises used: MeasureTheory.IntegrableOn.restrict_toMeasurable, MeasureTheory.IntegrableOn
-- 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
⊢ Integrable f (μ.restrict u)

Tactic:
hu

Premises used: MeasureTheory.IntegrableOn
-- 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
⊢ Integrable f (μ.restrict u)

Tactic:
exact hu
-- 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
x : α
hx : x ∈ u
⊢ ‖f x‖ₑ ≠ 0

Tactic:
simpa using hx.2

Premises used: And.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
⊢ IntegrableOn f v μ

Tactic:
have A : IntegrableOn f v μ := by
    rw [IntegrableOn, hu.restrict_toMeasurable]
    · exact hu
    · intro x hx; simpa using hx.2
-- 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 μ
apply : (fun (x : α) ↦ 0) =ᶠ[ae (μ.restrict (t \ v))] f
⊢ IntegrableOn f (t \ v) μ

Tactic:
apply integrableOn_zero.congr

Premises used: MeasureTheory.Integrable.congr, MeasureTheory.integrableOn_zero
-- 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 μ
h : ∀ (x : α) (hxt : x ∈ t \ s → f x = 0) (hx : x ∈ t \ v), 0 = f x
⊢ (fun (x : α) ↦ 0) =ᶠ[ae (μ.restrict (t \ v))] f

Tactic:
filter_upwards [ae_restrict_of_ae h't,
      ae_restrict_mem₀ (ht.diff (measurableSet_toMeasurable μ u).nullMeasurableSet)] with x hxt hx

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.ae_restrict_mem₀, MeasureTheory.ae_restrict_of_ae, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.NullMeasurableSet.diff
-- 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
pos : ∀ (h'x : x ∈ s), 0 = f x
neg : ∀ (h'x : x ∉ s), 0 = f x
⊢ 0 = f x

Tactic:
by_cases h'x : x ∈ s
-- 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
pos : ∀ (H : ¬0 = f x), False
⊢ 0 = f x

Tactic:
by_contra H
-- 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
H : ¬0 = f x
⊢ False

Tactic:
hx.2 (subset_toMeasurable μ u ⟨h'x, Ne.symm H⟩)

Premises used: Ne.symm, MeasureTheory.subset_toMeasurable, And.right, And.intro
-- 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
H : ¬0 = f x
⊢ False

Tactic:
exact hx.2 (subset_toMeasurable μ u ⟨h'x, Ne.symm H⟩)

Premises used: Ne.symm, MeasureTheory.subset_toMeasurable, And.right, And.intro