awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
refine_1 : ∀ (x : ι), Measurable (β := ℝ≥0∞) ((As x).indicator 1)
refine_2 : ∀ᶠ (n : ι) in L, ∀ᵐ (a : α) ∂μ, LE.le (α := ℝ≥0∞) ((As n).indicator 1 a) (B.indicator 1 a)
refine_3 : ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞
refine_4 : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (a : α), (As i).indicator 1 a ∂μ) L (𝓝 (∫⁻ (a : α), A.indicator 1 a ∂μ))

Tactic:
refine tendsto_lintegral_filter_of_dominated_convergence (B.indicator (1 : α → ℝ≥0∞))
          (Eventually.of_forall ?_) ?_ ?_ ?_

Premises used: Set.indicator, Filter.Eventually.of_forall, MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ (x : ι), Measurable (β := ℝ≥0∞) ((As x).indicator 1)

Tactic:
fun i ↦ Measurable.indicator measurable_const (As_mble i)

Premises used: Measurable.indicator, measurable_const
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ (x : ι), Measurable (β := ℝ≥0∞) ((As x).indicator 1)

Tactic:
exact fun i ↦ Measurable.indicator measurable_const (As_mble i)

Premises used: Measurable.indicator, measurable_const
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h : ∀ (i : ι) (hi : As i ⊆ B), ∀ᵐ (a : α) ∂μ, LE.le (α := ℝ≥0∞) ((As i).indicator 1 a) (B.indicator 1 a)
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : α) ∂μ, LE.le (α := ℝ≥0∞) ((As n).indicator 1 a) (B.indicator 1 a)

Tactic:
filter_upwards [As_le_B] with i hi
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
i : ι
hi : As i ⊆ B
x : α
h₁ : LE.le (α := ℝ≥0∞) 0 (1 x)
grw grw₁ : LE.le (α := ℝ≥0∞) (B.indicator 1 x) (B.indicator 1 x)
⊢ LE.le (α := ℝ≥0∞) ((As i).indicator 1 x) (B.indicator 1 x)

Tactic:
grw [hi]
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
i : ι
hi : As i ⊆ B
⊢ ∀ᵐ (a : α) ∂μ, LE.le (α := ℝ≥0∞) ((As i).indicator 1 a) (B.indicator 1 a)

Tactic:
exact Eventually.of_forall fun x ↦ by grw [hi]

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
refine_3 refine_3₁ refine_3₂ refine_3₃ :
  ∀ (B_finmeas : ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞) (As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B)
    (h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A), ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞

Tactic:
rwa [← lintegral_indicator_one B_mble] at B_finmeas

Premises used: MeasureTheory.lintegral_indicator_one
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))

Tactic:
simpa only [Pi.one_def, tendsto_indicator_const_apply_iff_eventually] using h_lim

Premises used: tendsto_indicator_const_apply_iff_eventually, Pi.one_def
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst_2 : IsFiniteMeasure μ
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
inl :
  ∀ [IsCountablyGenerated.{u_2} (α := ι) ⊥] (As_le_B : ∀ᶠ (i : ι) in ⊥, As i ⊆ B)
    (h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) ⊥
      (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
inr :
  L.NeBot →
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
      (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)

Tactic:
rcases L.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
inst_1 : IsCountablyGenerated.{u_2} (α := ι) ⊥
As_le_B : ∀ᶠ (i : ι) in ⊥, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) ⊥
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)

Tactic:
tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
inst_1 : IsCountablyGenerated.{u_2} (α := ι) ⊥
As_le_B : ∀ᶠ (i : ι) in ⊥, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) ⊥
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)

Tactic:
exact tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h : L.NeBot
apply : MeasurableSet A
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)

Tactic:
apply tendsto_measure_of_ae_tendsto_indicator L ?_ As_mble B_mble B_finmeas As_le_B
        (ae_of_all μ h_lim)

Premises used: MeasureTheory.ae_of_all, MeasureTheory.tendsto_measure_of_ae_tendsto_indicator
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h : L.NeBot
⊢ MeasurableSet A

Tactic:
measurableSet_of_tendsto_indicator L As_mble h_lim

Premises used: measurableSet_of_tendsto_indicator
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h : L.NeBot
⊢ MeasurableSet A

Tactic:
exact measurableSet_of_tendsto_indicator L As_mble h_lim

Premises used: measurableSet_of_tendsto_indicator
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst_2 : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
inl :
  ∀ [IsCountablyGenerated.{u_2} (α := ι) ⊥] (h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) ⊥
      (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
inr :
  L.NeBot →
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
      (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)

Tactic:
rcases L.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
inst_1 : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
inst_2 : IsCountablyGenerated.{u_2} (α := ι) ⊥
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) ⊥
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)

Tactic:
tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
inst_1 : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
inst_2 : IsCountablyGenerated.{u_2} (α := ι) ⊥
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) ⊥
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)

Tactic:
exact tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst_2 : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h : L.NeBot
apply : MeasurableSet A
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)

Tactic:
apply tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure L ?_ As_mble (ae_of_all μ h_lim)

Premises used: MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure, MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst_2 : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h : L.NeBot
⊢ MeasurableSet A

Tactic:
measurableSet_of_tendsto_indicator L As_mble h_lim

Premises used: measurableSet_of_tendsto_indicator
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst_2 : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h : L.NeBot
⊢ MeasurableSet A

Tactic:
exact measurableSet_of_tendsto_indicator L As_mble h_lim

Premises used: measurableSet_of_tendsto_indicator
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace β
μ : Measure α
f : α → β
⊢ AEStronglyMeasurable f (μ.restrict ∅)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace β
l : Filter α
f : α → β
μ : Measure α
h : StronglyMeasurableAtFilter f l μ
⊢ ∀ᶠ (s : Set α) in l.smallSets, AEStronglyMeasurable f (μ.restrict s)

Tactic:
(eventually_smallSets' fun _ _ => AEStronglyMeasurable.mono_set).2 h

Premises used: Iff.mpr, MeasureTheory.AEStronglyMeasurable.mono_set, Filter.eventually_smallSets'
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace β
l l' : Filter α
f : α → β
μ : Measure α
h : StronglyMeasurableAtFilter f l μ
h' : l' ≤ l
⊢ StronglyMeasurableAtFilter f l' μ

Tactic:
let ⟨s, hsl, hs⟩ := h
  ⟨s, h' hsl, hs⟩

Premises used: _private.0.StronglyMeasurableAtFilter.filter_mono.match_1, StronglyMeasurableAtFilter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace β
l : Filter α
f : α → β
μ : Measure α
h rwa rwa₁ rwa₂ rwa₃ : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f (μ.restrict univ)

Tactic:
rwa [Measure.restrict_univ]

Premises used: MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace β
l : Filter α
f : α → β
μ : Measure α
s : Set α
h : AEStronglyMeasurable f (μ.restrict s)
hl : s ∈ l
⊢ StronglyMeasurableAtFilter f l μ

Tactic:
⟨s, hl, h⟩

Premises used: StronglyMeasurableAtFilter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace β
l : Filter α
f : α → β
μ : Measure α
h : StronglyMeasurable f
⊢ StronglyMeasurableAtFilter f l μ

Tactic:
h.aestronglyMeasurable.stronglyMeasurableAtFilter

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C
rwa rwa₁ rwa₂ rwa₃ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [Measure.restrict_apply_univ]

Premises used: MeasureTheory.Measure.restrict_apply_univ
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
C : ℝ≥0∞
hC : ‖C‖ₑ ≠ ∞
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ₑ ≤ C
rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply_univ]

Premises used: MeasureTheory.Measure.restrict_apply_univ
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
C : ℝ≥0∞
hC : ‖C‖ₑ ≠ ∞
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ₑ ≤ C
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
hs.lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
C : ℝ≥0∞
hC : ‖C‖ₑ ≠ ∞
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ₑ ≤ C
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact hs.lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f s μ
⊢ Integrable f (μ.restrict s)

Tactic:
h

Premises used: MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
⊢ IntegrableOn f ∅ μ

Tactic:
simp [IntegrableOn]

Premises used: MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
rw : Integrable f (μ.restrict univ) ↔ Integrable f μ
rw₁ rw₂ : Integrable f μ ↔ Integrable f μ
⊢ IntegrableOn f univ μ ↔ Integrable f μ

Tactic:
rw [IntegrableOn, Measure.restrict_univ]

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
⊢ IntegrableOn.{u_1, u_4} (ε := ε') (fun (x : α) ↦ 0) s μ

Tactic:
integrable_zero _ _ _

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.integrable_zero
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IntegrableOn f s μ

Tactic:
simp [IntegrableOn, Measure.restrict_eq_zero.2 hs]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_eq_zero, MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
C : ε'
hC : ‖C‖ₑ ≠ ∞
rw :
  Integrable.{u_4, u_1} (ε := ε') (fun (x : α) ↦ C) (μ.restrict s) ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw₁ :
  ‖C‖ₑ = 0 ∨ IsFiniteMeasure (μ.restrict s) ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw₂ :
  ‖C‖ₑ = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw₃ rw₄ :
  ‖C‖ₑ = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    ‖C‖ₑ = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn.{u_1, u_4} (ε := ε') (fun (x : α) ↦ C) s μ ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [IntegrableOn, integrable_const_iff_enorm hC, isFiniteMeasure_restrict, lt_top_iff_ne_top]

Premises used: MeasureTheory.IntegrableOn, lt_top_iff_ne_top, MeasureTheory.isFiniteMeasure_restrict, MeasureTheory.integrable_const_iff_enorm
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
C : ε'
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ‖C‖ₑ ≠ ∞
⊢ IntegrableOn.{u_1, u_4} (ε := ε') (fun (x : α) ↦ C) s μ

Tactic:
(integrableOn_const_iff hC).2 <| Or.inr <| lt_top_iff_ne_top.2 hs

Premises used: Iff.mpr, MeasureTheory.integrableOn_const_iff, lt_top_iff_ne_top, Or.inr
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f t ν
hs : s ⊆ t
hμ : μ ≤ ν
⊢ IntegrableOn f s μ

Tactic:
h.mono_measure <| Measure.restrict_mono hs hμ

Premises used: MeasureTheory.Integrable.mono_measure, MeasureTheory.Measure.restrict_mono, MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f t μ
hst : s ⊆ t
⊢ IntegrableOn f s μ

Tactic:
h.mono hst le_rfl

Premises used: le_rfl, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f s ν
hμ : μ ≤ ν
⊢ IntegrableOn f s μ

Tactic:
h.mono (Subset.refl _) hμ

Premises used: Set.Subset.refl, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f s ν
hμ : μ.restrict s ≤ ν.restrict s
⊢ IntegrableOn f s μ

Tactic:
Integrable.mono_measure h hμ

Premises used: MeasureTheory.Integrable.mono_measure, MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f t μ
hst : s ≤ᶠ[ae μ] t
⊢ IntegrableOn f s μ

Tactic:
h.integrable.mono_measure <| Measure.restrict_mono_ae hst

Premises used: MeasureTheory.Integrable.mono_measure, MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_mono_ae, MeasureTheory.IntegrableOn.integrable