awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace Y
inst_3 : TopologicalSpace Y
inst_4 : TopologicalSpace ε''
inst_5 : ESeminormedAddMonoid ε''
inst_6 : BorelSpace X
inst_7 : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable (f ∘ (⇑e : (a : X) → Y)) μ
x : Y
U : Set X
hU : Membership.mem (γ := Filter X) (𝓝 ((e.symm : (a : Y) → X) x) : Filter X) U
h'U : IntegrableOn (f ∘ (⇑e : (a : X) → Y)) U μ
⊢ preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U) = U
have h₁ : ∀ (x : X),
  Membership.mem (γ := Set X) (preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U)) x ↔
    x ∈ U
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
⊢ Integrable.{u_6, u_1} (ε := E) (fun (x : X) ↦ g x • f x) μ
have hK : IsCompact K
Tactic: have hK : IsCompact K := h'g
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
have apply : (support.{u_1, u_6} (M := E) fun (x : X) ↦ g x • f x) ⊆ K
Tactic: apply indicator_eq_self.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ (support.{u_1, u_6} (M := E) fun (x : X) ↦ g x • f x) ⊆ K
have apply : ∀ x ∉ K, g x • f x = 0
Tactic: apply support_subset_iff'.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ Integrable.{u_6, u_1} (ε := E) (fun (x : X) ↦ g x • f x) μ
have this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
Tactic: have : K.indicator (fun x ↦ g x • f x) = (fun x ↦ g x • f x) := by
    apply indicator_eq_self.2
    apply support_subset_iff'.2
    intro x hx
    simp [image_eq_zero_of_notMem_tsupport hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
⊢ Integrable.{u_6, u_1} (ε := E) (fun (x : X) ↦ g x • f x) μ
have rw : Integrable.{u_6, u_1} (ε := E) (fun (a : X) ↦ g a • K.indicator f a) μ
Tactic: rw [← this, indicator_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
⊢ Integrable.{u_6, u_1} (ε := E) (fun (a : X) ↦ g a • K.indicator f a) μ
have hf₁ : Integrable (K.indicator f) μ
Tactic: apply Integrable.smul_of_top_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
hf₁ : Integrable (K.indicator f) μ
⊢ Integrable.{u_6, u_1} (ε := E) (fun (a : X) ↦ g a • K.indicator f a) μ
have hφ : MemLp g ∞ μ
Tactic: apply Integrable.smul_of_top_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x
⊢ Integrable (K.indicator f) μ
have hf₁ : IntegrableOn f K μ
Tactic: rw [integrable_indicator_iff hK.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
⊢ Integrable.{u_6, u_1} (ε := E) (fun (x : X) ↦ f x • g x) μ
have hK : IsCompact K
Tactic: have hK : IsCompact K := h'g
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
have apply : (support.{u_1, u_6} (M := E) fun (x : X) ↦ f x • g x) ⊆ K
Tactic: apply indicator_eq_self.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ (support.{u_1, u_6} (M := E) fun (x : X) ↦ f x • g x) ⊆ K
have apply : ∀ x ∉ K, f x • g x = 0
Tactic: apply support_subset_iff'.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ Integrable.{u_6, u_1} (ε := E) (fun (x : X) ↦ f x • g x) μ
have this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
Tactic: have : K.indicator (fun x ↦ f x • g x) = (fun x ↦ f x • g x) := by
    apply indicator_eq_self.2
    apply support_subset_iff'.2
    intro x hx
    simp [image_eq_zero_of_notMem_tsupport hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
⊢ Integrable.{u_6, u_1} (ε := E) (fun (x : X) ↦ f x • g x) μ
have rw : Integrable.{u_6, u_1} (ε := E) (fun (a : X) ↦ K.indicator f a • g a) μ
Tactic: rw [← this, indicator_smul_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
⊢ Integrable.{u_6, u_1} (ε := E) (fun (a : X) ↦ K.indicator f a • g a) μ
have hφ : Integrable (K.indicator f) μ
Tactic: apply Integrable.smul_of_top_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
hφ : Integrable (K.indicator f) μ
⊢ Integrable.{u_6, u_1} (ε := E) (fun (a : X) ↦ K.indicator f a • g a) μ
have hf₁ : MemLp g ∞ μ
Tactic: apply Integrable.smul_of_top_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ f x • g x) fun (x : X) ↦ f x • g x
⊢ Integrable (K.indicator f) μ
have hφ : IntegrableOn f K μ
Tactic: rw [integrable_indicator_iff hK.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
⊢ Integrable f μ ↔ IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
have refine : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ →
  ∀ (s : Set X) (hsc : s ∈ cocompact X) (hs : IntegrableOn f s μ) (hloc : LocallyIntegrable f μ), Integrable f μ
Tactic: refine ⟨fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩, fun ⟨⟨s, hsc, hs⟩, hloc⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
h : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
⊢ Integrable f μ
have obtain : ∀ (t : Set X) (htc : IsCompact t) (ht : sᶜ ⊆ t), Integrable f μ
Tactic: obtain ⟨t, htc, ht⟩ := mem_cocompact'.mp hsc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
h : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
t : Set X
htc : IsCompact t
ht : sᶜ ⊆ t
⊢ Integrable f μ
have rewrite : IntegrableOn f sᶜ μ ∧ IntegrableOn f s μ
Tactic: rewrite [← integrableOn_univ, ← compl_union_self s, integrableOn_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
inst_4 : PseudoMetrizableSpace ε''
f : X → ε''
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
⊢ Integrable f μ ↔ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
have mp : Integrable f μ → (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
inst_4 : PseudoMetrizableSpace ε''
f : X → ε''
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
mp : Integrable f μ → (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
⊢ Integrable f μ ↔ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
have mpr : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
inst_4 : PseudoMetrizableSpace ε''
f : X → ε''
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
⊢ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ
have mpr : ∀ (h : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ),
  IntegrableAtFilter f (cocompact X) μ
Tactic: refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LinearOrder X
inst_6 : OrderTop X
inst_7 : CompactIccSpace X
⊢ Integrable f μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
have mp : Integrable f μ → IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LinearOrder X
inst_6 : OrderTop X
inst_7 : CompactIccSpace X
mp : Integrable f μ → IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
⊢ Integrable f μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
have mpr : IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LinearOrder X
inst_6 : OrderTop X
inst_7 : CompactIccSpace X
⊢ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ
have mpr : ∀ (h : IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ), IntegrableAtFilter f (cocompact X) μ
Tactic: refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
⊢ IntegrableOn f (Iic a) μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
have refine : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ →
  ∀ (s : Set X) (hsl : Membership.mem (γ := Filter X) atBot s) (hs : IntegrableOn f s μ)
    (h : LocallyIntegrableOn f (Iic a) μ), IntegrableOn f (Iic a) μ
Tactic: refine ⟨fun h ↦ ⟨⟨Iic a, Iic_mem_atBot a, h⟩, h.locallyIntegrableOn⟩, fun ⟨⟨s, hsl, hs⟩, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
h_1 : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : Membership.mem (γ := Filter X) atBot s
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
⊢ IntegrableOn f (Iic a) μ
have this : Nonempty X
Tactic: haveI : Nonempty X := Nonempty.intro a
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
h_1 : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : Membership.mem (γ := Filter X) atBot s
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
⊢ IntegrableOn f (Iic a) μ
have obtain : ∀ (a' : X) (ha' : ∀ b ≤ a', b ∈ s), IntegrableOn f (Iic a) μ
Tactic: obtain ⟨a', ha'⟩ := mem_atBot_sets.mp hsl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
h_1 : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : Membership.mem (γ := Filter X) atBot s
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≤ a', b ∈ s
⊢ IntegrableOn f (Iic a) μ
have refine : IntegrableOn f (Icc a' a) μ
Tactic: refine (integrableOn_union.mpr ⟨hs.mono ha' le_rfl, ?_⟩).mono Iic_subset_Iic_union_Icc le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
⊢ IntegrableOn f (Iio a) μ ↔
    IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ
have mp : IntegrableOn f (Iio a) μ →
  IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
mp :
  IntegrableOn f (Iio a) μ →
    IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ
⊢ IntegrableOn f (Iio a) μ ↔
    IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ
have mpr : IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ →
  IntegrableOn f (Iio a) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
⊢ IntegrableOn f (Iio a) μ
have mpr : ∀ (s' : X) (hs'_mono : s' ∈ Iio a) (hs' : Ioo s' a ⊆ s), IntegrableOn f (Iio a) μ
Tactic: obtain ⟨s', ⟨hs'_mono, hs'⟩⟩ := mem_nhdsLT_iff_exists_Ioo_subset.mp hsl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
⊢ IntegrableOn f (Iio a) μ
have mpr : IntegrableOn f (Iic s') μ
Tactic: refine (integrableOn_union.mpr ⟨?_, hs.mono hs' le_rfl⟩).mono Iio_subset_Iic_union_Ioo le_rfl