awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})) l
        (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (ENNReal.toNNReal ∘ fun (x : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) l
    (𝓝 (ENNReal.toNNReal 0))

Tactic:
exact h ε hε
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f : ι → α → E
g : α → E
v : Filter ι
huv : v ≤ l
hg : TendstoInMeasure μ f l g
⊢ TendstoInMeasure μ f v g

Tactic:
fun ε hε => (hg ε hε).mono_left huv

Premises used: MeasureTheory.TendstoInMeasure, Filter.Tendsto.mono_left
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f : ι → α → E
g : α → E
v : Filter κ
ns : κ → ι
hg : TendstoInMeasure μ f l g
hns : Tendsto ns v l
⊢ TendstoInMeasure μ (f ∘ ns) v g

Tactic:
fun ε hε ↦ (hg ε hε).comp hns

Premises used: setOf, MeasureTheory.TendstoInMeasure, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
⊢ TendstoInMeasure μ (fun (i : ι) ↦ s.indicator (f i)) l (s.indicator g)

Tactic:
fun ε hε => tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (hg ε hε) ?_ ?_

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, MeasureTheory.TendstoInMeasure
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
refine_1 :
  ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
    LE.le.{u_2} (α := ι → ℝ≥0∞) (fun (x : ι) ↦ 0) fun (i : ι) ↦
      (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) i x) (s.indicator g x)}
refine_2 :
  ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
    LE.le.{u_2} (α := ι → ℝ≥0∞)
      (fun (i : ι) ↦
        (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) i x) (s.indicator g x)})
      fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}
⊢ TendstoInMeasure μ (fun (i : ι) ↦ s.indicator (f i)) l (s.indicator g)

Tactic:
refine fun ε hε => tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (hg ε hε) ?_ ?_

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
i : ι
⊢ LE.le (α := (fun (a : ι) ↦ ℝ≥0∞) i) ((fun (x : ι) ↦ (0 : ℝ≥0∞)) i)
    ((fun (i : ι) ↦
        ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) i x) (s.indicator g x)} : ℝ≥0∞))
      i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
⊢ LE.le.{u_2} (α := ι → ℝ≥0∞)
    (fun (i : ι) ↦
      (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) i x) (s.indicator g x)})
    fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}

Tactic:
fun n => measure_mono (fun x hx => ?_)

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
refine_2 :
  ∀ (n : ι) (x : α)
    (hx : Membership.mem (γ := Set α) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) n x) (s.indicator g x)} x),
    Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x
⊢ LE.le.{u_2} (α := ι → ℝ≥0∞)
    (fun (i : ι) ↦
      (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) i x) (s.indicator g x)})
    fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}

Tactic:
refine fun n => measure_mono (fun x hx => ?_)

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : Membership.mem (γ := Set α) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) n x) (s.indicator g x)} x
pos : x ∈ s → Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x
neg : x ∉ s → Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x
⊢ Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x

Tactic:
by_cases x ∈ s
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : Membership.mem (γ := Set α) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) n x) (s.indicator g x)} x
h : x ∈ s
⊢ Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : Membership.mem (γ := Set α) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) n x) (s.indicator g x)} x
h : x ∉ s
⊢ Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
this :
  l.EventuallyEq (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) fun (i : ι) ↦
    (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}
rw : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) l (𝓝 0)

Tactic:
rw [tendsto_congr' this]

Premises used: Filter.tendsto_congr'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
this :
  l.EventuallyEq (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) fun (i : ι) ↦
    (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
h_tendsto ε hε
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
this :
  l.EventuallyEq (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) fun (i : ι) ↦
    (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
exact h_tendsto ε hε
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i :
  l.EventuallyEq (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) fun (i : ι) ↦
    (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) l (𝓝 0)

Tactic:
suffices
    (fun i ↦ μ { x | ε ≤ edist (f' i x) (g' x) }) =ᶠ[l] fun i ↦ μ { x | ε ≤ edist (f i x) (g x) } by
    rw [tendsto_congr' this]
    exact h_tendsto ε hε
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
h :
  ∀ (i : ι) (h_ae_eq : f i =ᶠ[ae μ] f' i),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)} : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞)
⊢ l.EventuallyEq (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) fun (i : ι) ↦
    (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}

Tactic:
filter_upwards [h_left] with i h_ae_eq
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞)

Tactic:
measure_congr ?_

Premises used: MeasureTheory.measure_congr
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
h : {x : α | ε ≤ edist (f' i x) (g' x)} =ᶠ[ae μ] {x : α | ε ≤ edist (f i x) (g x)}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞)

Tactic:
refine measure_congr ?_

Premises used: MeasureTheory.measure_congr
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
h :
  ∀ (x : α) (hxf : f i x = f' i x) (hxg : g x = g' x),
    {x : α | ε ≤ edist (f' i x) (g' x)} x = {x : α | ε ≤ edist (f i x) (g x)} x
⊢ {x : α | ε ≤ edist (f' i x) (g' x)} =ᶠ[ae μ] {x : α | ε ≤ edist (f i x) (g x)}

Tactic:
filter_upwards [h_ae_eq, h_right] with x hxf hxg
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
h : {x : α | ε ≤ edist (f' i x) (g' x)} x ↔ {x : α | ε ≤ edist (f i x) (g x)} x
⊢ {x : α | ε ≤ edist (f' i x) (g' x)} x = {x : α | ε ≤ edist (f i x) (g x)} x

Tactic:
rw [eq_iff_iff]

Premises used: eq_iff_iff
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
h : ε ≤ edist (f' i x) (g' x) ↔ ε ≤ edist (f i x) (g' x)
h₁ h₂ : ε ≤ edist (f' i x) (g' x) ↔ ε ≤ edist (f' i x) (g' x)
⊢ ε ≤ edist (f' i x) (g' x) ↔ ε ≤ edist (f i x) (g x)

Tactic:
rw [hxg, hxf]
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ (i : ι), f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
⊢ TendstoInMeasure μ f' l g'

Tactic:
TendstoInMeasure.congr' (Eventually.of_forall h_left) h_right h_tendsto

Premises used: Filter.Eventually.of_forall, MeasureTheory.TendstoInMeasure.congr'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f f' : ι → α → E
g : α → E
h : ∀ (i : ι), f i =ᶠ[ae μ] f' i
h_tendsto : TendstoInMeasure μ f l g
⊢ TendstoInMeasure μ f' l g

Tactic:
h_tendsto.congr h EventuallyEq.rfl

Premises used: MeasureTheory.TendstoInMeasure.congr, Filter.EventuallyEq.rfl
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
l : Filter ι
f : ι → α → E
g g' : α → E
h : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
⊢ TendstoInMeasure μ f l g'

Tactic:
h_tendsto.congr (fun _ => EventuallyEq.rfl) h

Premises used: MeasureTheory.TendstoInMeasure.congr, Filter.EventuallyEq.rfl
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ TendstoInMeasure μ f atTop g

Tactic:
fun ε hε => ENNReal.tendsto_atTop_zero.mpr fun δ hδ => ?_

Premises used: Iff.mpr, MeasureTheory.TendstoInMeasure, ENNReal.tendsto_atTop_zero
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
refine :
  ∀ (ε : ℝ≥0∞) (hε : 0 < ε) (δ : ℝ≥0∞) (hδ : δ > 0),
    ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ
⊢ TendstoInMeasure μ f atTop g

Tactic:
refine fun ε hε => ENNReal.tendsto_atTop_zero.mpr fun δ hδ => ?_

Premises used: Iff.mpr, ENNReal.tendsto_atTop_zero
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
pos : ∀ (hδi : δ = ∞), ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ
neg : ∀ (hδi : ¬δ = ∞), ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ

Tactic:
by_cases hδi : δ = ∞
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
hδi : δ = ∞
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ

Tactic:
simp only [hδi, imp_true_iff, le_top, exists_const]

Premises used: imp_true_iff, le_top, exists_const
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
hδi : ¬δ = ∞
⊢ δ ≠ ∞

Tactic:
hδi
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
hδi : ¬δ = ∞
neg :
  ∀ (δ : ℝ≥0) (hδ : (↑δ : ℝ≥0∞) > 0),
    ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ

Tactic:
lift δ to ℝ≥0 using hδi
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : (↑δ : ℝ≥0∞) > 0
⊢ 0 < (↑δ : ℝ)

Tactic:
rw [gt_iff_lt, ENNReal.coe_pos, ← NNReal.coe_pos] at hδ

Premises used: ENNReal.coe_pos, gt_iff_lt, NNReal.coe_pos
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < (↑δ : ℝ)
neg :
  ∀ (t : Set α),
    MeasurableSet t →
      ∀ (ht : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal (↑δ : ℝ)) (hunif : TendstoUniformlyOn f g atTop tᶜ),
        ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)

Tactic:
obtain ⟨t, _, ht, hunif⟩ :=
    tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist' hf hfg hδ

Premises used: MeasureTheory.tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < (↑δ : ℝ)
t : Set α
left : MeasurableSet t
ht : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal (↑δ : ℝ)
hunif : TendstoUniformlyOn f g atTop tᶜ
⊢ (μ : (a : Set α) → ℝ≥0∞) t ≤ (↑δ : ℝ≥0∞)

Tactic:
rw [ENNReal.ofReal_coe_nnreal] at ht

Premises used: ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < (↑δ : ℝ)
t : Set α
left : MeasurableSet t
ht : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal (↑δ : ℝ)
hunif : TendstoUniformlyOn f g atTop tᶜ
ht₁ : (μ : (a : Set α) → ℝ≥0∞) t ≤ (↑δ : ℝ≥0∞)
⊢ TendstoUniformlyOn f g atTop tᶜ

Tactic:
rw [ENNReal.ofReal_coe_nnreal] at ht

Premises used: ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < (↑δ : ℝ)
t : Set α
left : MeasurableSet t
ht : (μ : (a : Set α) → ℝ≥0∞) t ≤ (↑δ : ℝ≥0∞)
hunif : TendstoUniformlyOn f g atTop tᶜ
⊢ ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, edist (g x) (f n x) < ε

Tactic:
rw [EMetric.tendstoUniformlyOn_iff] at hunif

Premises used: EMetric.tendstoUniformlyOn_iff
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < (↑δ : ℝ)
t : Set α
left : MeasurableSet t
ht : (μ : (a : Set α) → ℝ≥0∞) t ≤ (↑δ : ℝ≥0∞)
hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, edist (g x) (f n x) < ε
neg :
  ∀ (N : ℕ) (hN : ∀ b ≥ N, ∀ x ∈ tᶜ, edist (g x) (f b x) < ε),
    ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)

Tactic:
obtain ⟨N, hN⟩ := eventually_atTop.1 (hunif ε hε)

Premises used: Iff.mp, Filter.eventually_atTop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < (↑δ : ℝ)
t : Set α
left : MeasurableSet t
ht : (μ : (a : Set α) → ℝ≥0∞) t ≤ (↑δ : ℝ≥0∞)
hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, edist (g x) (f n x) < ε
N : ℕ
hN : ∀ b ≥ N, ∀ x ∈ tᶜ, edist (g x) (f b x) < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)

Tactic:
⟨N, fun n hn => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < (↑δ : ℝ)
t : Set α
left : MeasurableSet t
ht : (μ : (a : Set α) → ℝ≥0∞) t ≤ (↑δ : ℝ≥0∞)
hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, edist (g x) (f n x) < ε
N : ℕ
hN : ∀ b ≥ N, ∀ x ∈ tᶜ, edist (g x) (f b x) < ε
neg : ∀ (n : ℕ) (hn : n ≥ N), (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)

Tactic:
refine ⟨N, fun n hn => ?_⟩