awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
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 (s.piecewise (β := fun (a : α) ↦ ε') f g) μ
have hg₁ : Integrable g (μ.restrict sᶜ)
Tactic: rw [IntegrableOn] at hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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ᶜ)
⊢ Integrable (s.piecewise (β := fun (a : α) ↦ ε') f g) μ
have rw : ∀ (hf : MemLp f 1 (μ.restrict s)) (hg : MemLp g 1 (μ.restrict sᶜ)), MemLp (s.piecewise (β := fun (a : α) ↦ ε') f g) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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
have h : ∀ (a : α) (ha : Membership.mem (γ := Set α) {x} a), f a = f x
Tactic: filter_upwards [ae_restrict_mem (measurableSet_singleton x)] with _ ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst_2 : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
⊢ IntegrableOn f {x} μ ↔ ‖f x‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞)
have this : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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 α
⊢ IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ
have empty : IntegrableOn f (⋃ (i : β), ⋃ (_ : Membership.mem (γ := Set β) ∅ i), t i) μ ↔
  ∀ (i : β), Membership.mem (γ := Set β) ∅ i → IntegrableOn f (t i) μ
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hf => simp [hf, or_imp, forall_and]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ
have 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 a s, t i) μ ↔ ∀ i ∈ insert a 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]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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 α
⊢ IntegrableOn f (⋃ (i : β), t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ
have intro : ∀ (val : Fintype β), IntegrableOn f (⋃ (i : β), t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ
Tactic: cases nonempty_fintype β
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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 (↑s : Set α) μ
have rw : IntegrableOn f (⋃ x ∈ (↑s : Set α), {x}) μ
Tactic: rw [← (s : Set α).biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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)
have rw : Integrable f (μ.restrict s + ν.restrict s)
Tactic: rw [Measure.restrict_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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 β
⊢ IntegrableOn (mα := inst_2) f s (Measure.map e μ) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ
have simp_rw : @Integrable _ _ _ _ inst_2 f (Measure.restrict (Measure.map e μ) s) ↔ Integrable (f ∘ e) (μ.restrict (e ⁻¹' s))
Tactic: simp_rw [IntegrableOn, he.restrict_map, he.integrable_map_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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))
⊢ IntegrableOn (mα := inst_2) f s (Measure.map e μ) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ
have simp_rw₁ : @Integrable _ _ _ _ inst_2 f (Measure.map e (μ.restrict (e ⁻¹' s))) ↔ Integrable (f ∘ e) (μ.restrict (e ⁻¹' s))
Tactic: simp_rw [IntegrableOn, he.restrict_map, he.integrable_map_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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
⊢ IntegrableOn f s μ ↔ IntegrableOn (mα := mα) (f ∘ e) (e ⁻¹' s) (Measure.comap e μ)
have simp_rw : IntegrableOn f s μ ↔ IntegrableOn (mα := inst_2) f s (Measure.map e (Measure.comap e μ))
Tactic: simp_rw [← he.integrableOn_map_iff, he.map_comap, IntegrableOn,
    Measure.restrict_restrict_of_subset hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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 μ))
⊢ IntegrableOn f s μ ↔ IntegrableOn (mα := mα) (f ∘ e) (e ⁻¹' s) (Measure.comap e μ)
have simp_rw₁ : IntegrableOn f s μ ↔ IntegrableOn f s (μ.restrict (range e))
Tactic: simp_rw [← he.integrableOn_map_iff, he.map_comap, IntegrableOn,
    Measure.restrict_restrict_of_subset hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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))
⊢ IntegrableOn f s μ ↔ IntegrableOn (mα := mα) (f ∘ e) (e ⁻¹' s) (Measure.comap e μ)
have simp_rw₂ : Integrable f (μ.restrict s) ↔ Integrable f ((μ.restrict (range e)).restrict s)
Tactic: simp_rw [← he.integrableOn_map_iff, he.map_comap, IntegrableOn,
    Measure.restrict_restrict_of_subset hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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 β
⊢ IntegrableOn f (range e) μ ↔ @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ)
have rw : IntegrableOn (mα := mα) (f ∘ e) (e ⁻¹' range e) (Measure.comap e μ) ↔ @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ)
Tactic: rw [he.integrableOn_iff_comap .rfl, preimage_range, integrableOn_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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 μ)
⊢ IntegrableOn f (range e) μ ↔ @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ)
have rw₁ : IntegrableOn (mα := mα) (f ∘ e) univ (Measure.comap e μ) ↔ @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ)
Tactic: rw [he.integrableOn_iff_comap .rfl, preimage_range, integrableOn_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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 μ)
⊢ IntegrableOn f (range e) μ ↔ @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ)
have rw₂ : @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ) ↔ @Integrable _ _ _ _ mα (f ∘ e) (Measure.comap e μ)
Tactic: rw [he.integrableOn_iff_comap .rfl, preimage_range, integrableOn_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hs : MeasurableSet s
⊢ Integrable (s.indicator f) μ ↔ IntegrableOn f s μ
have simp_rw : Integrable (s.indicator f) μ ↔ Integrable f (μ.restrict s)
Tactic: simp_rw [IntegrableOn, Integrable, hasFiniteIntegral_iff_enorm,
    enorm_indicator_eq_indicator_enorm, lintegral_indicator hs,
    aestronglyMeasurable_indicator_iff hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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)
⊢ Integrable (s.indicator f) μ ↔ IntegrableOn f s μ
have simp_rw₁ : AEStronglyMeasurable (s.indicator f) μ ∧ HasFiniteIntegral (s.indicator f) μ ↔
  AEStronglyMeasurable f (μ.restrict s) ∧ HasFiniteIntegral f (μ.restrict s)
Tactic: simp_rw [IntegrableOn, Integrable, hasFiniteIntegral_iff_enorm,
    enorm_indicator_eq_indicator_enorm, lintegral_indicator hs,
    aestronglyMeasurable_indicator_iff hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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)
⊢ Integrable (s.indicator f) μ ↔ IntegrableOn f s μ
have simp_rw₂ : AEStronglyMeasurable (s.indicator f) μ ∧ ∫⁻ (a : α), ‖s.indicator f a‖ₑ ∂μ < ∞ ↔
  AEStronglyMeasurable f (μ.restrict s) ∧ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ < ∞
Tactic: simp_rw [IntegrableOn, Integrable, hasFiniteIntegral_iff_enorm,
    enorm_indicator_eq_indicator_enorm, lintegral_indicator hs,
    aestronglyMeasurable_indicator_iff hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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‖ₑ ∂μ < ∞
⊢ Integrable (s.indicator f) μ ↔ IntegrableOn f s μ
have simp_rw₃ : AEStronglyMeasurable (s.indicator f) μ ∧ ∫⁻ (a : α), s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a ∂μ < ∞ ↔
  AEStronglyMeasurable f (μ.restrict s) ∧ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ < ∞
Tactic: simp_rw [IntegrableOn, Integrable, hasFiniteIntegral_iff_enorm,
    enorm_indicator_eq_indicator_enorm, lintegral_indicator hs,
    aestronglyMeasurable_indicator_iff hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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‖ₑ ∂μ < ∞
⊢ Integrable (s.indicator f) μ ↔ IntegrableOn f s μ
have simp_rw₄ : AEStronglyMeasurable (s.indicator f) μ ∧ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ < ∞ ↔
  AEStronglyMeasurable f (μ.restrict s) ∧ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ < ∞
Tactic: simp_rw [IntegrableOn, Integrable, hasFiniteIntegral_iff_enorm,
    enorm_indicator_eq_indicator_enorm, lintegral_indicator hs,
    aestronglyMeasurable_indicator_iff hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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
⊢ Integrable (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) μ
have rw : c = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [integrable_congr indicatorConstLp_coeFn, integrable_indicator_iff hs, IntegrableOn,
    integrable_const_iff, isFiniteMeasure_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s t : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f : α → ε'
hs : MeasurableSet s
⊢ IntegrableOn (s.indicator f) t μ ↔ IntegrableOn f (s ∩ t) μ
have simp_rw : Integrable (s.indicator f) (μ.restrict t) ↔ Integrable f (μ.restrict (s ∩ t))
Tactic: simp_rw [IntegrableOn, integrable_indicator_iff hs, IntegrableOn, Measure.restrict_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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))
⊢ IntegrableOn (s.indicator f) t μ ↔ IntegrableOn f (s ∩ t) μ
have simp_rw₁ : IntegrableOn f s (μ.restrict t) ↔ Integrable f (μ.restrict (s ∩ t))
Tactic: simp_rw [IntegrableOn, integrable_indicator_iff hs, IntegrableOn, Measure.restrict_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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))
⊢ IntegrableOn (s.indicator f) t μ ↔ IntegrableOn f (s ∩ t) μ
have simp_rw₂ : Integrable f ((μ.restrict t).restrict s) ↔ Integrable f (μ.restrict (s ∩ t))
Tactic: simp_rw [IntegrableOn, integrable_indicator_iff hs, IntegrableOn, Measure.restrict_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s
have 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
Tactic: rcases exists_seq_strictAnti_tendsto' ENNReal.zero_lt_top with ⟨u, _, u_pos, u_lim⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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∞)
have rw : Ne (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | u n ≤ ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [inter_comm, ← Measure.restrict_apply (measurableSet_toMeasurable _ _),
      measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
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‖ₑ}
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s
have A : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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∞)
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s
have apply : s ⊆ ⋃ (n : ℕ), v n
Tactic: apply Measure.restrict_toMeasurable_of_cover _ A
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), v n) x
have obtain : ∀ (n : ℕ) (hn : u n < ‖f 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
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 t μ
have hu : IntegrableOn f u μ
Tactic: have hu : IntegrableOn f u μ := hf.mono_set fun x hx => hx.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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 μ
have rw : Integrable f (μ.restrict u)
Tactic: rw [IntegrableOn, hu.restrict_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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)
⊢ IntegrableOn f v μ
have rw₁ : ∀ x ∈ u, ‖f x‖ₑ ≠ 0
Tactic: rw [IntegrableOn, hu.restrict_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
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 t μ
have A : IntegrableOn f v μ
Tactic: have A : IntegrableOn f v μ := by
    rw [IntegrableOn, hu.restrict_toMeasurable]
    · exact hu
    · intro x hx; simpa using hx.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x : α | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
A : IntegrableOn f v μ
⊢ IntegrableOn f (t \ v) μ
have apply : (fun (x : α) ↦ 0) =ᶠ[ae (μ.restrict (t \ v))] f
Tactic: apply integrableOn_zero.congr