awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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ᶜ
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
have ht₁ : (μ : (a : Set α) → ℝ≥0∞) t ≤ (↑δ : ℝ≥0∞)
Tactic: rw [ENNReal.ofReal_coe_nnreal] at ht
Cleared hypotheses: ht, hunif
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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ᶜ
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
have hunif₁ : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, edist (g x) (f n x) < ε
Tactic: rw [EMetric.tendstoUniformlyOn_iff] at hunif
Cleared hypotheses: hunif
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
have 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∞)
Tactic: obtain ⟨N, hN⟩ := eventually_atTop.1 (hunif ε hε)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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∞)
have neg : ∀ (n : ℕ) (hn : n ≥ N), (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
Tactic: refine ⟨N, fun n hn => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
have neg : {x : α | ε ≤ edist (f n x) (g x)} ⊆ t
Tactic: suffices { x : α | ε ≤ edist (f n x) (g x) } ⊆ t from (measure_mono this).trans ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 : α | ε ≤ edist (f n x) (g x)} ⊆ t
have neg : tᶜ ⊆ {x : α | ε ≤ edist (f n x) (g x)}ᶜ
Tactic: rw [← Set.compl_subset_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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ᶜ
⊢ Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)}ᶜ x
have neg : edist (g x) (f n x) < ε
Tactic: rw [Set.mem_compl_iff, Set.notMem_setOf_iff, edist_comm, not_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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))
⊢ TendstoInMeasure μ f atTop g
have hg : AEStronglyMeasurable g μ
Tactic: have hg : AEStronglyMeasurable g μ := aestronglyMeasurable_of_tendsto_ae _ hf hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
have refine : TendstoInMeasure μ (fun (i : ℕ) ↦ AEStronglyMeasurable.mk (f i) sorry) atTop (AEStronglyMeasurable.mk g hg)
Tactic: refine TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)
have refine : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) sorry x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))
Tactic: refine tendstoInMeasure_of_tendsto_ae_of_measurable_edist
    (fun n ↦ ((hf n).stronglyMeasurable_mk.edist hg.stronglyMeasurable_mk).measurable) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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 : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))
have hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) sorry 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))
have h : ∀ (x : α) (hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) sorry 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) sorry x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))
Tactic: filter_upwards [hf_eq_ae, hg.ae_eq_mk, hfg] with x hxf hxg hxfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ ∃ (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
have hfg₁ : 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) _)
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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)
⊢ ∃ (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
have hfg₁ : ∀ ε > 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
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 + 1) = max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)
have rw : max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1) =
  max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)
Tactic: rw [seqTendstoAeSeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ edist (f k x) (g x)} ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
have 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
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ edist (f k x) (g x)} ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
have 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)
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)
have refine : ∀ (n : ℕ), seqTendstoAeSeq hfg n < seqTendstoAeSeq hfg (n + 1)
Tactic: refine strictMono_nat_of_lt_succ fun n => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 < ε
have obtain : ∀ (k : ℕ) (h_k : 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'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 < ε
have refine : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
Tactic: refine ⟨k + 1, lt_of_eq_of_lt ?_ h_k⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 < ε
⊢ 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
have h0 : Ne (α := ℝ≥0∞) 2 0
Tactic: rw [pow_succ', ← mul_assoc, ENNReal.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
have ht : Ne (α := ℝ≥0∞) 2 ∞
Tactic: rw [pow_succ', ← mul_assoc, ENNReal.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
⊢ ∃ (ns : ℕ → ℕ), StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
have h_lt_ε_real : ∀ (ε : ℝ≥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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ ∃ (ns : ℕ → ℕ), StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
have h : StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
Tactic: use ns
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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)}
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
have hμS_le : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
have hs : let s := limsup S atTop;
s = limsup S atTop
Tactic: set s := Filter.atTop.limsup S with hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
s : Set α := limsup S atTop
hs : s = limsup S atTop
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : Ne (α := ℝ≥0∞) (∑' (a : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ a) ∞
Tactic: refine measure_limsup_atTop_eq_zero (ne_top_of_le_ne_top ?_ (ENNReal.tsum_le_tsum hμS_le))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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
s : Set α := limsup S atTop
hs : s = limsup S atTop
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
have hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hμs : μ s = 0 := by
    refine measure_limsup_atTop_eq_zero (ne_top_of_le_ne_top ?_ (ENNReal.tsum_le_tsum hμS_le))
    simpa only [ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, inv_inv] using ENNReal.ofNat_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ x ∈ sᶜ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
have refine : ∀ (x : α) (hx : x ∈ sᶜ) (ε : ℝ≥0∞) (hε : ε > 0), ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
Tactic: refine fun x hx => EMetric.tendsto_atTop.mpr fun ε hε => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ sᶜ
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
have rw : ∀ (hx : Membership.mem (γ := Set α) (⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), S i)ᶜ x) (ε : ℝ≥0∞) (hε : ε > 0),
  ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
Tactic: rw [hs, limsup_eq_iInf_iSup_of_nat] at hx
Cleared hypotheses: hx, ε, hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) (⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), S i)ᶜ x
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
have hx₁ : ∃ (i : ℕ), ∀ (i_1 : ℕ) (i : i_1 ≥ i), edist (f (ns i_1) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ i_1
Tactic: simp only [S, Set.iSup_eq_iUnion, Set.iInf_eq_iInter, Set.compl_iInter, Set.compl_iUnion,
      Set.mem_iUnion, Set.mem_iInter, Set.mem_compl_iff, Set.mem_setOf_eq, not_le] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
ε : ℝ≥0∞
hε : ε > 0
hx : ∃ (i : ℕ), ∀ (i_1 : ℕ) (i : i_1 ≥ i), edist (f (ns i_1) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ i_1
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
have obtain : ∀ (N : ℕ) (hNx : ∀ (i : ℕ) (i_1 : i ≥ N), edist (f (ns i) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ i),
  ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
Tactic: obtain ⟨N, hNx⟩ := hx
Cleared hypotheses: hx