awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
ν : Measure α
φ : ι → Set α
hφ : AECover μ l φ
hle : ν ≪ μ
⊢ AECover ν l φ

Tactic:
⟨hle hφ.1, hφ.2⟩

Premises used: MeasureTheory.AECover.mk, MeasureTheory.AECover.measurableSet, MeasureTheory.AECover.ae_eventually_mem
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
ν : Measure α
φ : ι → Set α
hφ : AECover μ l φ
hle : ν ≤ μ
⊢ AECover ν l φ

Tactic:
hφ.mono_ac hle.absolutelyContinuous

Premises used: LE.le.absolutelyContinuous, MeasureTheory.AECover.mono_ac
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
h : ∀ (y : α), ∀ᶠ (i : ι) in l, y ∈ Metric.ball x (r i)
⊢ ∀ᵐ (x_1 : α) ∂μ, ∀ᶠ (i : ι) in l, x_1 ∈ Metric.ball x (r i)

Tactic:
filter_upwards with y
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
a : ι
ha : a ∈ r ⁻¹' Ioi (dist x y)
⊢ y ∈ Metric.ball x (r a)

Tactic:
simpa [dist_comm] using ha

Premises used: dist_comm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        x_1 ∈ r ⁻¹' Ioi (dist x y) →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (i : ι) ↦ y ∈ Metric.ball x (r i)) x_2} x_1}
      a
h₁ h₂ : ∀ (a : ι) (ha : a ∈ r ⁻¹' Ioi (dist x y)), y ∈ Metric.ball x (r a)
⊢ ∀ᶠ (i : ι) in l, y ∈ Metric.ball x (r i)

Tactic:
filter_upwards [hr (Ioi_mem_atTop (dist x y))] with a ha using by simpa [dist_comm] using ha

Premises used: Filter.Ioi_mem_atTop, Dist.dist
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
h : ∀ (y : α), ∀ᶠ (i : ι) in l, y ∈ Metric.closedBall x (r i)
⊢ ∀ᵐ (x_1 : α) ∂μ, ∀ᶠ (i : ι) in l, x_1 ∈ Metric.closedBall x (r i)

Tactic:
filter_upwards with y
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
a : ι
ha : a ∈ r ⁻¹' Ici (dist x y)
⊢ y ∈ Metric.closedBall x (r a)

Tactic:
simpa [dist_comm] using ha

Premises used: dist_comm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        x_1 ∈ r ⁻¹' Ici (dist x y) →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (i : ι) ↦ y ∈ Metric.closedBall x (r i)) x_2} x_1}
      a
h₁ h₂ : ∀ (a : ι) (ha : a ∈ r ⁻¹' Ici (dist x y)), y ∈ Metric.closedBall x (r a)
⊢ ∀ᶠ (i : ι) in l, y ∈ Metric.closedBall x (r i)

Tactic:
filter_upwards [hr (Ici_mem_atTop (dist x y))] with a ha using by simpa [dist_comm] using ha

Premises used: Filter.Ici_mem_atTop, Dist.dist
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
b : ι → α
hb : Tendsto b l atTop
⊢ AECover μ l fun (i : ι) ↦ Iic (b i)

Tactic:
aecover_Ici (α := αᵒᵈ) hb

Premises used: setOf, MeasureTheory.aecover_Ici, Set.Iic, OrderDual
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
ha : Tendsto a l atBot
hb : Tendsto b l atTop
⊢ AECover μ l fun (i : ι) ↦ Icc (a i) (b i)

Tactic:
(aecover_Ici ha).inter (aecover_Iic hb)

Premises used: Set.Ici, MeasureTheory.aecover_Iic, Set.Mem, MeasureTheory.AECover.inter, setOf, Set.inter, MeasureTheory.aecover_Ici, Set.Icc
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
b : ι → α
hb : Tendsto b l atTop
inst_5 : NoMaxOrder α
⊢ AECover μ l fun (i : ι) ↦ Iio (b i)

Tactic:
aecover_Ioi (α := αᵒᵈ) hb

Premises used: setOf, MeasureTheory.aecover_Ioi, OrderDual, Set.Iio
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
ha : Tendsto a l atBot
hb : Tendsto b l atTop
inst_5 : NoMinOrder α
inst_6 : NoMaxOrder α
⊢ AECover μ l fun (i : ι) ↦ Ioo (a i) (b i)

Tactic:
(aecover_Ioi ha).inter (aecover_Iio hb)

Premises used: Set.Ioi, Set.Mem, MeasureTheory.AECover.inter, setOf, MeasureTheory.aecover_Ioi, Set.inter, MeasureTheory.aecover_Iio, Set.Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
ha : Tendsto a l atBot
hb : Tendsto b l atTop
inst_5 : NoMinOrder α
⊢ AECover μ l fun (i : ι) ↦ Ioc (a i) (b i)

Tactic:
(aecover_Ioi ha).inter (aecover_Iic hb)

Premises used: Set.Ioc, Set.Ioi, MeasureTheory.aecover_Iic, Set.Mem, MeasureTheory.AECover.inter, setOf, MeasureTheory.aecover_Ioi, Set.inter
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
ha : Tendsto a l atBot
hb : Tendsto b l atTop
inst_5 : NoMaxOrder α
⊢ AECover μ l fun (i : ι) ↦ Ico (a i) (b i)

Tactic:
(aecover_Ici ha).inter (aecover_Iio hb)

Premises used: Set.Ici, Set.Mem, MeasureTheory.AECover.inter, setOf, Set.inter, Set.Ico, MeasureTheory.aecover_Ici, MeasureTheory.aecover_Iio
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
b : ι → α
B : α
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Iio B)) l fun (i : ι) ↦ Iio (b i)

Tactic:
aecover_Ioi_of_Ioi (α := αᵒᵈ) hb

Premises used: MeasureTheory.aecover_Ioi_of_Ioi, setOf, OrderDual, Set.Iio
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a : ι → α
A : α
ha : Tendsto a l (𝓝 A)
⊢ AECover (μ.restrict (Ioi A)) l fun (i : ι) ↦ Ici (a i)

Tactic:
(aecover_Ioi_of_Ioi ha).superset (fun _ ↦ Ioi_subset_Ici_self) fun _ ↦ measurableSet_Ici

Premises used: MeasureTheory.aecover_Ioi_of_Ioi, Set.Ioi_subset_Ici_self, MeasureTheory.AECover.superset, measurableSet_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
b : ι → α
B : α
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Iio B)) l fun (i : ι) ↦ Iic (b i)

Tactic:
aecover_Ioi_of_Ici (α := αᵒᵈ) hb

Premises used: MeasureTheory.aecover_Ioi_of_Ici, setOf, Set.Iic, OrderDual, Set.Iio
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
b c : ι → α
B : α
hb : Tendsto b l (𝓝 B)
hc : Tendsto c l atBot
⊢ ∀ᵐ (x : α) ∂μ.restrict (Iio B), ∀ᶠ (i : ι) in l, x ∈ Ico (c i) (b i)

Tactic:
(ae_restrict_mem measurableSet_Iio).mono fun _x hx ↦ ?_

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Iio, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
b c : ι → α
B : α
hb : Tendsto b l (𝓝 B)
hc : Tendsto c l atBot
refine : ∀ (_x : α) (hx : _x ∈ Iio B), ∀ᶠ (i : ι) in l, _x ∈ Ico (c i) (b i)
⊢ ∀ᵐ (x : α) ∂μ.restrict (Iio B), ∀ᶠ (i : ι) in l, x ∈ Ico (c i) (b i)

Tactic:
refine (ae_restrict_mem measurableSet_Iio).mono fun _x hx ↦ ?_

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Iio, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
b c : ι → α
B : α
hb : Tendsto b l (𝓝 B)
hc : Tendsto c l atBot
_x : α
hx : _x ∈ Iio B
simp : (∀ᶠ (x : ι) in l, c x ≤ _x) ∧ ∀ᶠ (x : ι) in l, _x < b x
⊢ ∀ᶠ (i : ι) in l, _x ∈ Ico (c i) (b i)

Tactic:
simp only [mem_Ico, eventually_and]

Premises used: Filter.eventually_and, Set.mem_Ico
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
b c : ι → α
B : α
hb : Tendsto b l (𝓝 B)
hc : Tendsto c l atBot
_x : α
hx : _x ∈ Iio B
⊢ (∀ᶠ (x : ι) in l, c x ≤ _x) ∧ ∀ᶠ (x : ι) in l, _x < b x

Tactic:
⟨hc.eventually (eventually_le_atBot _x), hb.eventually (eventually_gt_nhds hx)⟩

Premises used: eventually_gt_nhds, And.intro, Filter.Tendsto.eventually, Filter.eventually_le_atBot
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
b c : ι → α
B : α
hb : Tendsto b l (𝓝 B)
hc : Tendsto c l atBot
_x : α
hx : _x ∈ Iio B
⊢ (∀ᶠ (x : ι) in l, c x ≤ _x) ∧ ∀ᶠ (x : ι) in l, _x < b x

Tactic:
exact ⟨hc.eventually (eventually_le_atBot _x), hb.eventually (eventually_gt_nhds hx)⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst_5 : NoMaxOrder α
⊢ ∀ᵐ (x : α) ∂μ.restrict (Ici B), ∀ᶠ (i : ι) in l, x ∈ Ico B (d i)

Tactic:
(ae_restrict_mem measurableSet_Ici).mono fun _x hx ↦ ?_

Premises used: MeasureTheory.ae_restrict_mem, Filter.Eventually.mono, measurableSet_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst_5 : NoMaxOrder α
refine : ∀ (_x : α) (hx : _x ∈ Ici B), ∀ᶠ (i : ι) in l, _x ∈ Ico B (d i)
⊢ ∀ᵐ (x : α) ∂μ.restrict (Ici B), ∀ᶠ (i : ι) in l, x ∈ Ico B (d i)

Tactic:
refine (ae_restrict_mem measurableSet_Ici).mono fun _x hx ↦ ?_

Premises used: MeasureTheory.ae_restrict_mem, Filter.Eventually.mono, measurableSet_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst_5 : NoMaxOrder α
_x : α
hx : _x ∈ Ici B
simp : (∀ᶠ (x : ι) in l, B ≤ _x) ∧ ∀ᶠ (x : ι) in l, _x < d x
⊢ ∀ᶠ (i : ι) in l, _x ∈ Ico B (d i)

Tactic:
simp only [mem_Ico, eventually_and]

Premises used: Filter.eventually_and, Set.mem_Ico
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst_5 : NoMaxOrder α
_x : α
hx : _x ∈ Ici B
⊢ (∀ᶠ (x : ι) in l, B ≤ _x) ∧ ∀ᶠ (x : ι) in l, _x < d x

Tactic:
⟨.of_forall fun i => hx, hd.eventually (eventually_gt_atTop _x)⟩

Premises used: Filter.Eventually.of_forall, And.intro, Filter.Tendsto.eventually, Filter.eventually_gt_atTop
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst_5 : NoMaxOrder α
_x : α
hx : _x ∈ Ici B
⊢ (∀ᶠ (x : ι) in l, B ≤ _x) ∧ ∀ᶠ (x : ι) in l, _x < d x

Tactic:
exact⟨.of_forall fun i => hx, hd.eventually (eventually_gt_atTop _x)⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ioo A B)) l fun (i : ι) ↦ Ioo (a i) (b i)

Tactic:
((aecover_Ioi_of_Ioi ha).mono <| Measure.restrict_mono Ioo_subset_Ioi_self le_rfl).inter
    ((aecover_Iio_of_Iio hb).mono <| Measure.restrict_mono Ioo_subset_Iio_self le_rfl)

Premises used: MeasureTheory.aecover_Ioi_of_Ioi, Set.Ioi, le_rfl, Set.Mem, MeasureTheory.Measure.restrict_mono, MeasureTheory.AECover.inter, setOf, Set.inter, Set.Ioo_subset_Iio_self, MeasureTheory.aecover_Iio_of_Iio, Set.Ioo_subset_Ioi_self, Set.Ioo, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ioo A B)) l fun (i : ι) ↦ Icc (a i) (b i)

Tactic:
(aecover_Ioo_of_Ioo ha hb).superset (fun _ ↦ Ioo_subset_Icc_self) fun _ ↦ measurableSet_Icc

Premises used: Set.Ioo_subset_Icc_self, MeasureTheory.AECover.superset, MeasureTheory.aecover_Ioo_of_Ioo, measurableSet_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ioo A B)) l fun (i : ι) ↦ Ico (a i) (b i)

Tactic:
(aecover_Ioo_of_Ioo ha hb).superset (fun _ ↦ Ioo_subset_Ico_self) fun _ ↦ measurableSet_Ico

Premises used: measurableSet_Ico, MeasureTheory.AECover.superset, Set.Ioo_subset_Ico_self, MeasureTheory.aecover_Ioo_of_Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ioo A B)) l fun (i : ι) ↦ Ioc (a i) (b i)

Tactic:
(aecover_Ioo_of_Ioo ha hb).superset (fun _ ↦ Ioo_subset_Ioc_self) fun _ ↦ measurableSet_Ioc

Premises used: MeasureTheory.AECover.superset, MeasureTheory.aecover_Ioo_of_Ioo, Set.Ioo_subset_Ioc_self, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ioc A B)) l fun (i : ι) ↦ Icc (a i) (b i)

Tactic:
(aecover_Ioo_of_Icc ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Ioc).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Ioc, MeasureTheory.aecover_Ioo_of_Icc, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ioc A B)) l fun (i : ι) ↦ Ico (a i) (b i)

Tactic:
(aecover_Ioo_of_Ico ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Ioc).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Ioc, MeasureTheory.aecover_Ioo_of_Ico, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ioc A B)) l fun (i : ι) ↦ Ioc (a i) (b i)

Tactic:
(aecover_Ioo_of_Ioc ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Ioc).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.aecover_Ioo_of_Ioc, MeasureTheory.Ioo_ae_eq_Ioc, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ioc A B)) l fun (i : ι) ↦ Ioo (a i) (b i)

Tactic:
(aecover_Ioo_of_Ioo ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Ioc).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.aecover_Ioo_of_Ioo, MeasureTheory.Ioo_ae_eq_Ioc, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ico A B)) l fun (i : ι) ↦ Icc (a i) (b i)

Tactic:
(aecover_Ioo_of_Icc ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Ico).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Ico, MeasureTheory.aecover_Ioo_of_Icc, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ico A B)) l fun (i : ι) ↦ Ico (a i) (b i)

Tactic:
(aecover_Ioo_of_Ico ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Ico).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Ico, MeasureTheory.aecover_Ioo_of_Ico, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ico A B)) l fun (i : ι) ↦ Ioc (a i) (b i)

Tactic:
(aecover_Ioo_of_Ioc ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Ico).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.aecover_Ioo_of_Ioc, MeasureTheory.Ioo_ae_eq_Ico, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Ico A B)) l fun (i : ι) ↦ Ioo (a i) (b i)

Tactic:
(aecover_Ioo_of_Ioo ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Ico).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Ico, MeasureTheory.aecover_Ioo_of_Ioo, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Icc A B)) l fun (i : ι) ↦ Icc (a i) (b i)

Tactic:
(aecover_Ioo_of_Icc ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Icc).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Icc, MeasureTheory.aecover_Ioo_of_Icc, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Icc A B)) l fun (i : ι) ↦ Ico (a i) (b i)

Tactic:
(aecover_Ioo_of_Ico ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Icc).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Icc, MeasureTheory.aecover_Ioo_of_Ico, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Icc A B)) l fun (i : ι) ↦ Ioc (a i) (b i)

Tactic:
(aecover_Ioo_of_Ioc ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Icc).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Icc, MeasureTheory.aecover_Ioo_of_Ioc, MeasureTheory.AECover.mono