-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem TendstoInMeasure.exists_seq_tendsto_ae (hfg : TendstoInMeasure μ f atTop g) :
    ∃ ns : ℕ → ℕ, StrictMono ns ∧ ∀ᵐ x ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Proof state:
case h
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 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))

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

Result:
case h
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Proof state:
case h
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
⊢ StrictMono ns ∧ μ {a | ¬Tendsto (fun i => f (ns i) a) atTop (𝓝 (g a))} = 0

Tactic:
refine ⟨ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono hfg, measure_mono_null (fun x => ?_) hμs⟩

Result:
case h
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
x : α
⊢ x ∈ {a | ¬Tendsto (fun i => f (ns i) a) atTop (𝓝 (g a))} → x ∈ s

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
⊢ μ s = 0

Tactic:
refine measure_limsup_atTop_eq_zero (ne_top_of_le_ne_top ?_ (ENNReal.tsum_le_tsum hμS_le))

Result:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
⊢ ∑' (a : ℕ), 2⁻¹ ^ a ≠ ⊤

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Tactic:
have h_lt_ε_real : ∀ (ε : ℝ) (_ : 0 < ε), ∃ k : ℕ, 2 * (2 : ℝ)⁻¹ ^ k < ε := by
  intro ε hε
  obtain ⟨k, h_k⟩ : ∃ k : ℕ, (2 : ℝ)⁻¹ ^ k < ε := exists_pow_lt_of_lt_one hε (by norm_num)
  refine ⟨k + 1, (le_of_eq ?_).trans_lt h_k⟩
  rw [pow_add]; ring

Result:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Tactic:
use ns

Result:
case h
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Proof state:
case intro
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ
hε : 0 < ε
k : ℕ
h_k : 2⁻¹ ^ k < ε
⊢ ∃ k, 2 * 2⁻¹ ^ k < ε

Tactic:
refine ⟨k + 1, (le_of_eq ?_).trans_lt h_k⟩

Result:
case intro
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ
hε : 0 < ε
k : ℕ
h_k : 2⁻¹ ^ k < ε
⊢ 2 * 2⁻¹ ^ (k + 1) = 2⁻¹ ^ k

Proof state:
case intro
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ
hε : 0 < ε
k : ℕ
h_k : 2⁻¹ ^ k < ε
⊢ 2 * 2⁻¹ ^ (k + 1) = 2⁻¹ ^ k

Tactic:
rw [pow_add]

Result:
case intro
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ
hε : 0 < ε
k : ℕ
h_k : 2⁻¹ ^ k < ε
⊢ 2 * (2⁻¹ ^ k * 2⁻¹ ^ 1) = 2⁻¹ ^ k

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Tactic:
set ns := ExistsSeqTendstoAe.seqTendstoAeSeq hfg

Result:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))