awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 μ
⊢ (fun (x : α) ↦ 0) =ᶠ[ae (μ.restrict (t \ v))] f
have h : ∀ (x : α) (hxt : x ∈ t \ s → f x = 0) (hx : x ∈ t \ v), 0 = f x
Tactic: filter_upwards [ae_restrict_of_ae h't,
      ae_restrict_mem₀ (ht.diff (measurableSet_toMeasurable μ u).nullMeasurableSet)] with x hxt hx
-- 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 μ
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ v
⊢ 0 = f x
have pos : ∀ (h'x : x ∈ s), 0 = f x
Tactic: by_cases h'x : x ∈ s
-- 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 μ
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ v
pos : ∀ (h'x : x ∈ s), 0 = f x
⊢ 0 = f x
have neg : ∀ (h'x : x ∉ s), 0 = f x
Tactic: by_cases h'x : x ∈ s
-- 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 μ
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ v
h'x : x ∈ s
⊢ 0 = f x
have pos : ∀ (H : ¬0 = f x), False
Tactic: by_contra H
-- 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
A : IntegrableOn f v μ
⊢ IntegrableOn f t μ
have B : IntegrableOn f (t \ v) μ
Tactic: have B : IntegrableOn f (t \ v) μ := by
    apply integrableOn_zero.congr
    filter_upwards [ae_restrict_of_ae h't,
      ae_restrict_mem₀ (ht.diff (measurableSet_toMeasurable μ u).nullMeasurableSet)] with x hxt hx
    by_cases h'x : x ∈ s
    · by_contra H
      exact hx.2 (subset_toMeasurable μ u ⟨h'x, Ne.symm H⟩)
    · exact (hxt ⟨hx.1, h'x⟩).symm
-- 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 μ
B : IntegrableOn f (t \ v) μ
⊢ IntegrableOn f t μ
have apply : t ⊆ v ∪ t \ v
Tactic: apply (A.union B).mono_set _
-- 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 μ
B : IntegrableOn f (t \ v) μ
⊢ t ⊆ v ∪ t \ v
have rw : t ⊆ v ∪ t
Tactic: rw [union_diff_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
⊢ Integrable f μ
have rw : IntegrableOn f univ μ
Tactic: rw [← integrableOn_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
⊢ IntegrableOn f univ μ
have apply : ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0
Tactic: apply hf.of_ae_diff_eq_zero nullMeasurableSet_univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∉ s → f x = 0) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ univ \ s → f x = 0) x} x}
    a
Tactic: filter_upwards [h't] with x hx h'x using hx h'x.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∉ s → f x = 0) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ univ \ s → f x = 0) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0
have h₁ : ∀ (a : α), (a ∉ s → f a = 0) → a ∈ univ \ s → f a = 0
Tactic: filter_upwards [h't] with x hx h'x using hx h'x.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
⊢ IntegrableOn f s μ ↔ Integrable f μ
have refine : ∀ (h : IntegrableOn f s μ), Integrable f μ
Tactic: refine ⟨fun h => ?_, fun h => h.integrableOn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
h : IntegrableOn f s μ
⊢ Integrable f μ
have refine : ∀ (x : α) (hx : x ∉ s), f x = 0
Tactic: refine h.integrable_of_forall_notMem_eq_zero fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
h : IntegrableOn f s μ
x : α
hx : x ∉ s
⊢ f x = 0
have contrapose! : ∀ (hx : f x ≠ 0), x ∈ s
Tactic: contrapose! hx
Cleared hypotheses: hx
-- 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 α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (↑(↑f : α →ₘ[μ] E) : α → E) s μ
have refine : MemLp (↑(↑f : α →ₘ[μ] E) : α → E) 1 (μ.restrict s)
Tactic: refine memLp_one_iff_integrable.mp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ MemLp (↑(↑f : α →ₘ[μ] E) : α → E) 1 (μ.restrict s)
have hμ_restrict_univ : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hμ_restrict_univ : (μ.restrict s) Set.univ < ∞ := by
    simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ_restrict_univ : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ MemLp (↑(↑f : α →ₘ[μ] E) : α → E) 1 (μ.restrict s)
have hμ_finite : IsFiniteMeasure (μ.restrict s)
Tactic: haveI hμ_finite : IsFiniteMeasure (μ.restrict s) := ⟨hμ_restrict_univ⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
⊢ IntegrableAtFilter (mα := inst_2) f (map e l) (Measure.map e μ) ↔ IntegrableAtFilter (f ∘ e) l μ
have simp_rw : (∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) ↔ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ
Tactic: simp_rw [IntegrableAtFilter, he.integrableOn_map_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
⊢ (∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) ↔ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ
have mp : (∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) → ∃ s ∈ l, IntegrableOn (f ∘ e) s μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
mp : (∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) → ∃ s ∈ l, IntegrableOn (f ∘ e) s μ
⊢ (∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) ↔ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ
have mpr : (∃ s ∈ l, IntegrableOn (f ∘ e) s μ) → ∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
s : Set α
hs : s ∈ l ∧ IntegrableOn (f ∘ e) s μ
⊢ e '' s ∈ map e l ∧ IntegrableOn (f ∘ e) (e ⁻¹' e '' s) μ
have rwa : e ⁻¹' e '' s ∈ l ∧ IntegrableOn (f ∘ e) (e ⁻¹' e '' s) μ
Tactic: rwa [mem_map, he.injective.preimage_image]
-- 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 ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
⊢ IntegrableAtFilter f (map e l) μ ↔ IntegrableAtFilter (mα := mα) (f ∘ e) l (Measure.comap e μ)
have simp_rw : (∃ s ∈ map e l, IntegrableOn f s μ) ↔ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
Tactic: simp_rw [← he.integrableAtFilter_map_iff, IntegrableAtFilter, he.map_comap]
-- 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 ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
⊢ (∃ s ∈ map e l, IntegrableOn f s μ) ↔ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
have mp : (∃ s ∈ map e l, IntegrableOn f s μ) → ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
Tactic: constructor
-- 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 ε
l : Filter α
inst_2 : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
mp : (∃ s ∈ map e l, IntegrableOn f s μ) → ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
⊢ (∃ s ∈ map e l, IntegrableOn f s μ) ↔ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
have mpr : (∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))) → ∃ s ∈ map e l, IntegrableOn f s μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
inst_4 : Nonempty α
⊢ IntegrableAtFilter f atBot μ ↔ ∃ (a : α), IntegrableOn f (Iic a) μ
have refine : IntegrableAtFilter f atBot μ →
  ∀ (s : Set α) (hs : Membership.mem (γ := Filter α) atBot s) (hi : IntegrableOn f s μ),
    ∃ (a : α), IntegrableOn f (Iic a) μ
Tactic: refine ⟨fun ⟨s, hs, hi⟩ ↦ ?_, fun ⟨a, ha⟩ ↦ ⟨Iic a, Iic_mem_atBot a, ha⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
inst_4 : Nonempty α
h : IntegrableAtFilter f atBot μ
s : Set α
hs : Membership.mem (γ := Filter α) atBot s
hi : IntegrableOn f s μ
⊢ ∃ (a : α), IntegrableOn f (Iic a) μ
have obtain : ∀ (t : α) (ht : ∀ b ≤ t, b ∈ s), ∃ (a : α), IntegrableOn f (Iic a) μ
Tactic: obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs
-- 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 ε'
l : Filter α
inst_2 : ContinuousAdd ε'
f g : α → ε'
hf : IntegrableAtFilter f l μ
hg : IntegrableAtFilter g l μ
⊢ IntegrableAtFilter (f + g) l μ
have rcases : ∀ (s : Set α) (sl : s ∈ l) (hs : IntegrableOn f s μ), IntegrableAtFilter (f + g) l μ
Tactic: rcases hf with ⟨s, sl, hs⟩
Cleared hypotheses: hf
-- 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 ε'
l : Filter α
inst_2 : ContinuousAdd ε'
f g : α → ε'
hg : IntegrableAtFilter g l μ
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (f + g) l μ
have rcases : ∀ (t : Set α) (tl : t ∈ l) (ht : IntegrableOn g t μ), IntegrableAtFilter (f + g) l μ
Tactic: rcases hg with ⟨t, tl, ht⟩
Cleared hypotheses: 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 ε'
l : Filter α
inst_2 : ContinuousAdd ε'
f g : α → ε'
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
t : Set α
tl : t ∈ l
ht : IntegrableOn g t μ
⊢ IntegrableAtFilter (f + g) l μ
have refine : IntegrableOn (f + g) (s ∩ t) μ
Tactic: refine ⟨s ∩ t, inter_mem sl tl, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
hf : IntegrableAtFilter f l μ
⊢ IntegrableAtFilter (-f) l μ
have rcases : ∀ (s : Set α) (sl : s ∈ l) (hs : IntegrableOn f s μ), IntegrableAtFilter (-f) l μ
Tactic: rcases hf with ⟨s, sl, hs⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
⊢ IntegrableAtFilter (-f) l μ ↔ IntegrableAtFilter f l μ
have refine : ∀ (h : IntegrableAtFilter (-f) l μ), IntegrableAtFilter f l μ
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.neg⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h : IntegrableAtFilter (-f) l μ
⊢ IntegrableAtFilter f l μ
have h₁ : f = - -f
Tactic: convert! h.neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
hf : IntegrableAtFilter f l μ
hg : IntegrableAtFilter g l μ
⊢ IntegrableAtFilter (f - g) l μ
have rw : IntegrableAtFilter (f + -g) l μ
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : α → E
hf : IntegrableAtFilter f l μ
c : 𝕜
⊢ IntegrableAtFilter (c • f) l μ
have rcases : ∀ (s : Set α) (sl : s ∈ l) (hs : IntegrableOn f s μ), IntegrableAtFilter (c • f) l μ
Tactic: rcases hf with ⟨s, sl, hs⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → E
c : 𝕜
hc : c ≠ 0
⊢ IntegrableAtFilter (c • f) l μ ↔ IntegrableAtFilter f l μ
have refine : ∀ (hf : IntegrableAtFilter (c • f) l μ), IntegrableAtFilter f l μ
Tactic: refine ⟨fun hf ↦ ?_, fun h ↦ h.smul c⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → E
c : 𝕜
hc : c ≠ 0
hf : IntegrableAtFilter (c • f) l μ
⊢ IntegrableAtFilter f l μ
have h : f = c⁻¹ • c • f
Tactic: convert! hf.smul c⁻¹
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → E
c : 𝕜
⊢ IntegrableAtFilter (c • f) l μ ↔ c = 0 ∨ IntegrableAtFilter f l μ
have pos : ∀ (hc : c = 0), IntegrableAtFilter (c • f) l μ ↔ c = 0 ∨ IntegrableAtFilter f l μ
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → E
c : 𝕜
pos : ∀ (hc : c = 0), IntegrableAtFilter (c • f) l μ ↔ c = 0 ∨ IntegrableAtFilter f l μ
⊢ IntegrableAtFilter (c • f) l μ ↔ c = 0 ∨ IntegrableAtFilter f l μ
have neg : ∀ (hc : ¬c = 0), IntegrableAtFilter (c • f) l μ ↔ c = 0 ∨ IntegrableAtFilter f l μ
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
⊢ IntegrableAtFilter f (l ⊓ ae μ) μ ↔ IntegrableAtFilter f l μ
have refine : IntegrableAtFilter f (l ⊓ ae μ) μ → IntegrableAtFilter f l μ
Tactic: refine ⟨?_, fun h ↦ h.filter_mono inf_le_left⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ ae μ
hf : IntegrableOn f (t ∩ u) μ
⊢ IntegrableAtFilter f l μ
have refine : ∀ᵐ (x : α) ∂μ, x ∈ t ↔ x ∈ t ∩ u
Tactic: refine ⟨t, ht, hf.congr_set_ae <| eventuallyEq_set.2 ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ ae μ
hf : IntegrableOn f (t ∩ u) μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ t ↔ x ∈ t ∩ u
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α | x ∈ u → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t ↔ x ∈ t ∩ u) x} x} a
Tactic: filter_upwards [hu] with x hx using (and_iff_left hx).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ ae μ
hf : IntegrableOn f (t ∩ u) μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α | x ∈ u → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t ↔ x ∈ t ∩ u) x} x} a
⊢ ∀ᵐ (x : α) ∂μ, x ∈ t ↔ x ∈ t ∩ u
have h₁ : ∀ a ∈ u, a ∈ t ↔ a ∈ t ∩ u
Tactic: filter_upwards [hu] with x hx using (and_iff_left hx).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
⊢ IntegrableAtFilter f ⊤ μ ↔ Integrable f μ
have refine : ∀ (h : IntegrableAtFilter f ⊤ μ), Integrable f μ
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.integrableAtFilter ⊤⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h : IntegrableAtFilter f ⊤ μ
⊢ Integrable f μ
have obtain : ∀ (s : Set α) (hsf : Membership.mem (γ := Filter α) ⊤ s) (hs : IntegrableOn f s μ), Integrable f μ
Tactic: obtain ⟨s, hsf, hs⟩ := h
Cleared hypotheses: h
-- 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 ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
l l' : Filter α
⊢ IntegrableAtFilter f (l ⊔ l') μ ↔ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ
have mp : IntegrableAtFilter f (l ⊔ l') μ → IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ
Tactic: constructor
-- 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 ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
l l' : Filter α
mp : IntegrableAtFilter f (l ⊔ l') μ → IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ
⊢ IntegrableAtFilter f (l ⊔ l') μ ↔ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ
have mpr : IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ → IntegrableAtFilter f (l ⊔ l') μ
Tactic: constructor