awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
obtain : ∀ (t : α) (ht : ∀ b ≤ t, b ∈ s), ∃ (a : α), IntegrableOn f (Iic a) μ
⊢ ∃ (a : α), IntegrableOn f (Iic a) μ

Tactic:
obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs

Premises used: Iff.mp, Filter.mem_atBot_sets
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
t : α
ht : ∀ b ≤ t, b ∈ s
⊢ ∃ (a : α), IntegrableOn f (Iic a) μ

Tactic:
⟨t, hi.mono_set fun _ hx ↦ ht _ hx⟩

Premises used: MeasureTheory.IntegrableOn.mono_set, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
t : α
ht : ∀ b ≤ t, b ∈ s
⊢ ∃ (a : α), IntegrableOn f (Iic a) μ

Tactic:
exact ⟨t, hi.mono_set fun _ hx ↦ ht _ hx⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : Preorder α
inst_3 : IsDirectedOrder α
inst_4 : Nonempty α
⊢ IntegrableAtFilter f atTop μ ↔ ∃ (a : α), IntegrableOn f (Ici a) μ

Tactic:
integrableAtFilter_atBot_iff (α := αᵒᵈ)

Premises used: Set.Ici, setOf, MeasureTheory.integrableAtFilter_atBot_iff, Filter.atTop, OrderDual
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
hf : IntegrableAtFilter f l μ
h : ν ≤ μ
⊢ IntegrableAtFilter f l ν

Tactic:
let ⟨s, hs, hf⟩ := hf; ⟨s, hs, hf.mono_measure h⟩

Premises used: MeasureTheory.IntegrableAtFilter, _private.0.MeasureTheory.IntegrableAtFilter.mono_measure.match_1, And.intro, Exists.intro, MeasureTheory.IntegrableOn.mono_measure
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f g : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
hf : IntegrableAtFilter f l μ
h : f =ᶠ[ae μ] g
⊢ IntegrableAtFilter g l μ

Tactic:
let ⟨s, hs, hf⟩ := hf; ⟨s, hs, hf.congr h.restrict⟩

Premises used: Filter.EventuallyEq.restrict, MeasureTheory.IntegrableAtFilter, _private.0.MeasureTheory.IntegrableAtFilter.mono_measure.match_1, MeasureTheory.Integrable.congr, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f g : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
h : f =ᶠ[ae μ] g
⊢ IntegrableAtFilter f l μ ↔ IntegrableAtFilter g l μ

Tactic:
⟨(·.congr h), (·.congr h.symm)⟩

Premises used: MeasureTheory.IntegrableAtFilter.congr, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
⊢ univ ∈ l

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
rcases : ∀ (s : Set α) (sl : s ∈ l) (hs : IntegrableOn f s μ), IntegrableAtFilter (f + g) l μ
⊢ IntegrableAtFilter (f + g) l μ

Tactic:
rcases hf with ⟨s, sl, hs⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
rcases : ∀ (t : Set α) (tl : t ∈ l) (ht : IntegrableOn g t μ), IntegrableAtFilter (f + g) l μ
⊢ IntegrableAtFilter (f + g) l μ

Tactic:
rcases hg with ⟨t, tl, ht⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ

Tactic:
⟨s ∩ t, inter_mem sl tl, ?_⟩

Premises used: Filter.inter_mem, Inter.inter, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
refine : IntegrableOn (f + g) (s ∩ t) μ
⊢ IntegrableAtFilter (f + g) l μ

Tactic:
refine ⟨s ∩ t, inter_mem sl tl, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
⊢ IntegrableOn (f + g) (s ∩ t) μ

Tactic:
(hs.mono_set inter_subset_left).add (ht.mono_set inter_subset_right)

Premises used: Set.inter_subset_left, MeasureTheory.IntegrableOn.add, MeasureTheory.IntegrableOn.mono_set, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
⊢ IntegrableOn (f + g) (s ∩ t) μ

Tactic:
exact (hs.mono_set inter_subset_left).add (ht.mono_set inter_subset_right)

Premises used: Set.inter_subset_left, MeasureTheory.IntegrableOn.add, MeasureTheory.IntegrableOn.mono_set, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
hf : IntegrableAtFilter f l μ
rcases : ∀ (s : Set α) (sl : s ∈ l) (hs : IntegrableOn f s μ), IntegrableAtFilter (-f) l μ
⊢ IntegrableAtFilter (-f) l μ

Tactic:
rcases hf with ⟨s, sl, hs⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (-f) l μ

Tactic:
⟨s, sl, hs.neg⟩

Premises used: MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro, MeasureTheory.IntegrableOn.neg
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (-f) l μ

Tactic:
exact ⟨s, sl, hs.neg⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
⊢ IntegrableAtFilter (-f) l μ ↔ IntegrableAtFilter f l μ

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.neg⟩

Premises used: MeasureTheory.IntegrableAtFilter.neg, Iff.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
refine : ∀ (h : IntegrableAtFilter (-f) l μ), IntegrableAtFilter f l μ
⊢ IntegrableAtFilter (-f) l μ ↔ IntegrableAtFilter f l μ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.neg⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ

Tactic:
h.neg

Premises used: MeasureTheory.IntegrableAtFilter.neg
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h : IntegrableAtFilter (-f) l μ
h₁ : f = - -f
⊢ IntegrableAtFilter f l μ

Tactic:
convert! h.neg

Premises used: MeasureTheory.IntegrableAtFilter.neg
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h : IntegrableAtFilter (-f) l μ
⊢ f = - -f

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
rw : IntegrableAtFilter (f + -g) l μ
⊢ IntegrableAtFilter (f - g) l μ

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ

Tactic:
hf.add hg.neg

Premises used: MeasureTheory.IntegrableAtFilter.add, MeasureTheory.IntegrableAtFilter.neg
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ

Tactic:
exact hf.add hg.neg

Premises used: MeasureTheory.IntegrableAtFilter.add, MeasureTheory.IntegrableAtFilter.neg
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 : 𝕜
rcases : ∀ (s : Set α) (sl : s ∈ l) (hs : IntegrableOn f s μ), IntegrableAtFilter (c • f) l μ
⊢ IntegrableAtFilter (c • f) l μ

Tactic:
rcases hf with ⟨s, sl, hs⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
c : 𝕜
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (c • f) l μ

Tactic:
⟨s, sl, hs.smul c⟩

Premises used: MeasureTheory.Integrable.smul, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
c : 𝕜
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (c • f) l μ

Tactic:
exact ⟨s, sl, hs.smul c⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ

Tactic:
⟨fun hf ↦ ?_, fun h ↦ h.smul c⟩

Premises used: MeasureTheory.IntegrableAtFilter.smul, Iff.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
refine : ∀ (hf : IntegrableAtFilter (c • f) l μ), IntegrableAtFilter f l μ
⊢ IntegrableAtFilter (c • f) l μ ↔ IntegrableAtFilter f l μ

Tactic:
refine ⟨fun hf ↦ ?_, fun h ↦ h.smul c⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 (c⁻¹ • c • f) l μ

Tactic:
hf.smul c⁻¹

Premises used: MeasureTheory.IntegrableAtFilter.smul, Inv.inv
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
h : f = c⁻¹ • c • f
⊢ IntegrableAtFilter f l μ

Tactic:
convert! hf.smul c⁻¹

Premises used: MeasureTheory.IntegrableAtFilter.smul, Inv.inv
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
⊢ f = c⁻¹ • c • f

Tactic:
simp [← smul_assoc, inv_mul_cancel₀ hc]

Premises used: smul_assoc, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ
neg : ∀ (hc : ¬c = 0), IntegrableAtFilter (c • f) l μ ↔ c = 0 ∨ IntegrableAtFilter f l μ
⊢ IntegrableAtFilter (c • f) l μ ↔ c = 0 ∨ IntegrableAtFilter f l μ

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ ↔ c = 0 ∨ IntegrableAtFilter f l μ

Tactic:
simp [hc]
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ ↔ c = 0 ∨ IntegrableAtFilter f l μ

Tactic:
simpa [hc] using MeasureTheory.integrableAtFilter_smul_iff' hc

Premises used: _private.0.MeasureTheory.integrableAtFilter_smul_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
hf : IntegrableAtFilter f l μ
⊢ IntegrableAtFilter (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) l μ

Tactic:
Exists.casesOn hf fun s hs ↦ ⟨s, hs.1, hs.2.enorm⟩

Premises used: Exists.casesOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
hf : IntegrableAtFilter f l μ
⊢ IntegrableAtFilter (ε := ℝ) (fun (x : α) ↦ ‖f x‖) l μ

Tactic:
Exists.casesOn hf fun s hs ↦ ⟨s, hs.1, hs.2.norm⟩

Premises used: Exists.casesOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l l' : Filter α
hl : l ≤ l'
hl' : IntegrableAtFilter f l' μ
⊢ IntegrableAtFilter f l μ

Tactic:
let ⟨s, hs, hsf⟩ := hl'
  ⟨s, hl hs, hsf⟩

Premises used: MeasureTheory.IntegrableAtFilter, _private.0.MeasureTheory.IntegrableAtFilter.mono_measure.match_1, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l l' : Filter α
hl : IntegrableAtFilter f l μ
⊢ IntegrableAtFilter f (l ⊓ l') μ

Tactic:
hl.filter_mono inf_le_left

Premises used: MeasureTheory.IntegrableAtFilter.filter_mono, inf_le_left
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l l' : Filter α
hl : IntegrableAtFilter f l μ
⊢ IntegrableAtFilter f (l' ⊓ l) μ

Tactic:
hl.filter_mono inf_le_right

Premises used: inf_le_right, MeasureTheory.IntegrableAtFilter.filter_mono
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ

Tactic:
⟨?_, fun h ↦ h.filter_mono inf_le_left⟩

Premises used: Iff.intro, MeasureTheory.IntegrableAtFilter.filter_mono, inf_le_left
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
l : Filter α
refine : IntegrableAtFilter f (l ⊓ ae μ) μ → IntegrableAtFilter f l μ
⊢ IntegrableAtFilter f (l ⊓ ae μ) μ ↔ IntegrableAtFilter f l μ

Tactic:
refine ⟨?_, fun h ↦ h.filter_mono inf_le_left⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ

Tactic:
⟨t, ht, hf.congr_set_ae <| eventuallyEq_set.2 ?_⟩

Premises used: Iff.mpr, Filter.eventuallyEq_set, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro, MeasureTheory.IntegrableOn.congr_set_ae
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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) μ
refine : ∀ᵐ (x : α) ∂μ, x ∈ t ↔ x ∈ t ∩ u
⊢ IntegrableAtFilter f l μ

Tactic:
refine ⟨t, ht, hf.congr_set_ae <| eventuallyEq_set.2 ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 : α
hx : x ∈ u
⊢ x ∈ t ↔ x ∈ t ∩ u

Tactic:
(and_iff_left hx).symm

Premises used: Set.Mem, setOf, and_iff_left, Set.inter, Iff.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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
h₁ h₂ : ∀ (x : α) (hx : x ∈ u), x ∈ t ↔ x ∈ t ∩ u
⊢ ∀ᵐ (x : α) ∂μ, x ∈ t ↔ x ∈ t ∩ u

Tactic:
filter_upwards [hu] with x hx using (and_iff_left hx).symm
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
⊢ IntegrableAtFilter f ⊤ μ ↔ Integrable f μ

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.integrableAtFilter ⊤⟩

Premises used: MeasureTheory.Integrable.integrableAtFilter, Iff.intro, Top.top
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
refine : ∀ (h : IntegrableAtFilter f ⊤ μ), Integrable f μ
⊢ IntegrableAtFilter f ⊤ μ ↔ Integrable f μ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.integrableAtFilter ⊤⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
h : IntegrableAtFilter f ⊤ μ
obtain : ∀ (s : Set α) (hsf : Membership.mem (γ := Filter α) ⊤ s) (hs : IntegrableOn f s μ), Integrable f μ
⊢ Integrable f μ

Tactic:
obtain ⟨s, hsf, hs⟩ := h
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
s : Set α
hsf : Membership.mem (γ := Filter α) ⊤ s
hs : IntegrableOn f s μ
⊢ Integrable f μ

Tactic:
(integrableOn_iff_integrable_of_support_subset fun _ _ ↦ hsf _).mp hs

Premises used: MeasureTheory.integrableOn_iff_integrable_of_support_subset, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst : TopologicalSpace ε'
inst_1 : ENormedAddMonoid ε'
inst_2 : PseudoMetrizableSpace ε'
f : α → ε'
s : Set α
hsf : Membership.mem (γ := Filter α) ⊤ s
hs : IntegrableOn f s μ
⊢ Integrable f μ

Tactic:
exact (integrableOn_iff_integrable_of_support_subset fun _ _ ↦ hsf _).mp hs

Premises used: MeasureTheory.integrableOn_iff_integrable_of_support_subset, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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' μ
mpr : IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ → IntegrableAtFilter f (l ⊔ l') μ
⊢ IntegrableAtFilter f (l ⊔ l') μ ↔ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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' μ

Tactic:
fun h => ⟨h.filter_mono le_sup_left, h.filter_mono le_sup_right⟩

Premises used: le_sup_left, le_sup_right, And.intro, MeasureTheory.IntegrableAtFilter.filter_mono
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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' μ

Tactic:
exact fun h => ⟨h.filter_mono le_sup_left, h.filter_mono le_sup_right⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
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 μ ∧ IntegrableAtFilter f l' μ → IntegrableAtFilter f (l ⊔ l') μ

Tactic:
fun ⟨⟨s, hsl, hs⟩, ⟨t, htl, ht⟩⟩ ↦ ⟨s ∪ t, union_mem_sup hsl htl, hs.union ht⟩

Premises used: MeasureTheory.IntegrableOn.union, MeasureTheory.IntegrableAtFilter, Max.max, Filter.union_mem_sup, And.intro, Exists.intro, Union.union, _private.0.MeasureTheory.IntegrableAtFilter.sup_iff.match_1