awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
hn : n ≥ N
neg : {x : α | ε ≤ edist (f n x) (g x)} ⊆ t
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)

Tactic:
suffices { x : α | ε ≤ edist (f n x) (g x) } ⊆ t from (measure_mono this).trans ht
-- 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 : ℕ
hn : n ≥ N
neg : tᶜ ⊆ {x : α | ε ≤ edist (f n x) (g x)}ᶜ
⊢ {x : α | ε ≤ edist (f n x) (g x)} ⊆ t

Tactic:
rw [← Set.compl_subset_compl]

Premises used: Set.compl_subset_compl
-- 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 : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
neg : edist (g x) (f n x) < ε
⊢ Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)}ᶜ x

Tactic:
rw [Set.mem_compl_iff, Set.notMem_setOf_iff, edist_comm, not_le]

Premises used: not_le, PseudoEMetricSpace.edist_comm, Set.notMem_setOf_iff, Set.mem_compl_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) < ε
N : ℕ
hN : ∀ b ≥ N, ∀ x ∈ tᶜ, edist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ edist (g x) (f n x) < ε

Tactic:
hN n hn x hx
-- 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 : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ edist (g x) (f n x) < ε

Tactic:
exact hN n hn x hx
-- 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 : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ AEStronglyMeasurable g μ

Tactic:
have hg : AEStronglyMeasurable g μ := aestronglyMeasurable_of_tendsto_ae _ hf hfg
-- 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 : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ TendstoInMeasure μ f atTop g

Tactic:
TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.TendstoInMeasure.congr, Filter.EventuallyEq.symm
-- 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 : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
refine : TendstoInMeasure μ (fun (i : ℕ) ↦ AEStronglyMeasurable.mk (f i) ⋯) atTop (AEStronglyMeasurable.mk g hg)
⊢ TendstoInMeasure μ f atTop g

Tactic:
refine TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.TendstoInMeasure.congr, Filter.EventuallyEq.symm
-- 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 : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ TendstoInMeasure μ (fun (i : ℕ) ↦ AEStronglyMeasurable.mk (f i) ⋯) atTop (AEStronglyMeasurable.mk g hg)

Tactic:
tendstoInMeasure_of_tendsto_ae_of_measurable_edist
    (fun n ↦ ((hf n).stronglyMeasurable_mk.edist hg.stronglyMeasurable_mk).measurable) ?_

Premises used: MeasureTheory.StronglyMeasurable.edist, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_measurable_edist, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
-- 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 : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
refine :
  ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))
⊢ TendstoInMeasure μ (fun (i : ℕ) ↦ AEStronglyMeasurable.mk (f i) ⋯) atTop (AEStronglyMeasurable.mk g hg)

Tactic:
refine tendstoInMeasure_of_tendsto_ae_of_measurable_edist
    (fun n ↦ ((hf n).stronglyMeasurable_mk.edist hg.stronglyMeasurable_mk).measurable) ?_

Premises used: MeasureTheory.StronglyMeasurable.edist, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_measurable_edist, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
-- 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 : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x

Tactic:
have hf_eq_ae : ∀ᵐ x ∂μ, ∀ n, (hf n).mk (f n) x = f n x :=
    ae_all_iff.mpr fun n => (hf n).ae_eq_mk.symm
-- 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 : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
h :
  ∀ (x : α) (hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x) (hxg : g x = AEStronglyMeasurable.mk g hg x)
    (hxfg : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))),
    Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))

Tactic:
filter_upwards [hf_eq_ae, hg.ae_eq_mk, hfg] with x hxf hxg hxfg

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- 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 : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg h : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))

Tactic:
rw [← hxg, funext fun n => hxf n]

Premises used: funext
-- 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 : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))

Tactic:
hxfg
-- 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 : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))

Tactic:
exact hxfg
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) 0 2⁻¹

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ edist (f i x) (g x)}) atTop (𝓝 0)

Tactic:
specialize hfg ((2⁻¹ : ℝ≥0∞) ^ n) (ENNReal.pow_pos (by simp) _)

Premises used: Inv.inv, HPow.hPow, ENNReal.pow_pos, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg :
  Tendsto (β := ℝ≥0∞)
    (fun (i : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ edist (f i x) (g x)}) atTop (𝓝 0)
⊢ ∀ ε > 0,
    ∃ (N : ℕ), ∀ n_1 ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ edist (f n_1 x) (g x)} ≤ ε

Tactic:
rw [ENNReal.tendsto_atTop_zero] at hfg

Premises used: 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
n : ℕ
hfg :
  ∀ ε > 0,
    ∃ (N : ℕ), ∀ n_1 ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ edist (f n_1 x) (g x)} ≤ ε
⊢ Ne (α := ℝ≥0∞) 2⁻¹ 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg :
  ∀ ε > 0,
    ∃ (N : ℕ), ∀ n_1 ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ edist (f n_1 x) (g x)} ≤ ε
⊢ ∃ (N : ℕ),
    ∀ m_1 ≥ N,
      (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ edist (f m_1 x) (g x)} ≤
        HPow.hPow (α := ℝ≥0∞) 2⁻¹ n

Tactic:
exact hfg ((2 : ℝ≥0∞)⁻¹ ^ n) (pos_iff_ne_zero.mpr <| pow_ne_zero _ <| by simp)

Premises used: Iff.mpr, pow_ne_zero, Inv.inv, HPow.hPow, OfNat.ofNat, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
rw rw₁ :
  max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1) =
    max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)
⊢ seqTendstoAeSeq hfg (n + 1) = max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)

Tactic:
rw [seqTendstoAeSeq]

Premises used: MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n k : ℕ
hn : seqTendstoAeSeq hfg n ≤ k
zero :
  ∀ (hn : seqTendstoAeSeq hfg 0 ≤ k),
    (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2⁻¹ 0 ≤ edist (f k x) (g x)} ≤
      HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2⁻¹ 0
succ :
  ∀ (n : ℕ) (hn : seqTendstoAeSeq hfg (n + 1) ≤ k),
    (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) ≤ edist (f k x) (g x)} ≤
      HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1)
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ edist (f k x) (g x)} ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n

Tactic:
cases n
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k : ℕ
hn : seqTendstoAeSeq hfg 0 ≤ k
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2⁻¹ 0 ≤ edist (f k x) (g x)} ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2⁻¹ 0

Tactic:
Classical.choose_spec (exists_nat_measure_lt_two_inv hfg 0) k hn

Premises used: Classical.choose_spec, MeasureTheory.ExistsSeqTendstoAe.exists_nat_measure_lt_two_inv, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k : ℕ
hn : seqTendstoAeSeq hfg 0 ≤ k
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2⁻¹ 0 ≤ edist (f k x) (g x)} ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2⁻¹ 0

Tactic:
exact Classical.choose_spec (exists_nat_measure_lt_two_inv hfg 0) k hn

Premises used: Classical.choose_spec, MeasureTheory.ExistsSeqTendstoAe.exists_nat_measure_lt_two_inv, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k n : ℕ
hn : seqTendstoAeSeq hfg (n + 1) ≤ k
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) ≤ edist (f k x) (g x)} ≤
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1)

Tactic:
Classical.choose_spec
      (exists_nat_measure_lt_two_inv hfg _) _ (le_trans (le_max_left _ _) hn)

Premises used: Classical.choose_spec, MeasureTheory.ExistsSeqTendstoAe.exists_nat_measure_lt_two_inv, le_max_left, le_trans
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k n : ℕ
hn : seqTendstoAeSeq hfg (n + 1) ≤ k
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) ≤ edist (f k x) (g x)} ≤
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1)

Tactic:
exact Classical.choose_spec
      (exists_nat_measure_lt_two_inv hfg _) _ (le_trans (le_max_left _ _) hn)

Premises used: Classical.choose_spec, MeasureTheory.ExistsSeqTendstoAe.exists_nat_measure_lt_two_inv, le_max_left, le_trans
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
⊢ StrictMono (seqTendstoAeSeq hfg)

Tactic:
strictMono_nat_of_lt_succ fun n => ?_

Premises used: strictMono_nat_of_lt_succ
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
refine : ∀ (n : ℕ), seqTendstoAeSeq hfg n < seqTendstoAeSeq hfg (n + 1)
⊢ StrictMono (seqTendstoAeSeq hfg)

Tactic:
refine strictMono_nat_of_lt_succ fun n => ?_

Premises used: strictMono_nat_of_lt_succ
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ seqTendstoAeSeq hfg n < max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)

Tactic:
lt_of_lt_of_le (lt_add_one <| seqTendstoAeSeq hfg n) (le_max_right _ _)

Premises used: le_max_right, lt_add_one, MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ seqTendstoAeSeq hfg n < max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)

Tactic:
exact lt_of_lt_of_le (lt_add_one <| seqTendstoAeSeq hfg n) (le_max_right _ _)

Premises used: le_max_right, lt_add_one, MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε

Tactic:
ENNReal.exists_inv_two_pow_lt hε.ne'

Premises used: ENNReal.exists_inv_two_pow_lt, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ≥0∞
hε : 0 < ε
obtain : ∀ (k : ℕ) (h_k : HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε), ∃ (k : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
⊢ ∃ (k : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε

Tactic:
obtain ⟨k, h_k⟩ : ∃ k : ℕ, (2 : ℝ≥0∞)⁻¹ ^ k < ε := ENNReal.exists_inv_two_pow_lt hε.ne'

Premises used: ENNReal.exists_inv_two_pow_lt, LT.lt.ne', OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ≥0∞
hε : 0 < ε
k : ℕ
h_k : HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
⊢ ∃ (k : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε

Tactic:
⟨k + 1, lt_of_eq_of_lt ?_ h_k⟩

Premises used: lt_of_eq_of_lt, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ≥0∞
hε : 0 < ε
k : ℕ
h_k : HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
refine : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
⊢ ∃ (k : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε

Tactic:
refine ⟨k + 1, lt_of_eq_of_lt ?_ h_k⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ≥0∞
hε : 0 < ε
k : ℕ
h_k : HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
h0 : Ne (α := ℝ≥0∞) 2 0
ht : Ne (α := ℝ≥0∞) 2 ∞
⊢ 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ k

Tactic:
rw [pow_succ', ← mul_assoc, ENNReal.mul_inv_cancel, one_mul]

Premises used: mul_assoc, ENNReal.mul_inv_cancel, pow_succ', one_mul
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ≥0∞
hε : 0 < ε
k : ℕ
h_k : HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
⊢ Ne (α := ℝ≥0∞) 2 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ≥0∞
hε : 0 < ε
k : ℕ
h_k : HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
⊢ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (k : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε

Tactic:
have h_lt_ε_real (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ k : ℕ, 2 * (2 : ℝ≥0∞)⁻¹ ^ k < ε := by
    obtain ⟨k, h_k⟩ : ∃ k : ℕ, (2 : ℝ≥0∞)⁻¹ ^ k < ε := ENNReal.exists_inv_two_pow_lt hε.ne'
    refine ⟨k + 1, lt_of_eq_of_lt ?_ h_k⟩
    rw [pow_succ', ← mul_assoc, ENNReal.mul_inv_cancel, one_mul]
    · positivity
    · simp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (k : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
h : StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
⊢ ∃ (ns : ℕ → ℕ), StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
use ns
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (k : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : (k : ℕ) → Set α := fun (k : ℕ) ↦ {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ k ≤ edist (f (ns k) x) (g x)}
⊢ ∀ (k : ℕ), (μ : (a : Set α) → ℝ≥0∞) (S k) ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ k

Tactic:
have hμS_le : ∀ k, μ (S k) ≤ (2 : ℝ≥0∞)⁻¹ ^ k :=
    fun k => ExistsSeqTendstoAe.seqTendstoAeSeq_spec hfg k (ns k) le_rfl
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (k : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : (k : ℕ) → Set α := fun (k : ℕ) ↦ {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), (μ : (a : Set α) → ℝ≥0∞) (S k) ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
⊢ let s := limsup S atTop;
  s = limsup S atTop

Tactic:
set s := Filter.atTop.limsup S with hs

Premises used: Filter.limsup, Filter.atTop