-- 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 intro.intro
α : 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
x : α
ε : ℝ
hε : ε > 0
N : ℕ
hNx : ∀ i ≥ N, dist (f (ns i) x) (g x) < 2⁻¹ ^ i
k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ N ⊔ (k - 1)
⊢ dist (f (ns n) x) (g x) ≤ 2 * 2⁻¹ ^ k

Tactic:
specialize hNx n ((le_max_left _ _).trans hn_ge)

Result:
case intro.intro
α : 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
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ N ⊔ (k - 1)
hNx : dist (f (ns n) x) (g x) < 2⁻¹ ^ n
⊢ dist (f (ns n) x) (g x) ≤ 2 * 2⁻¹ ^ k

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))
x : α
⊢ x ∉ s → Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Tactic:
exact h_tendsto x

Result:
no goals

Proof state:
case intro.intro
α : 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
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ N ⊔ (k - 1)
hNx : dist (f (ns n) x) (g x) < 2⁻¹ ^ n
⊢ dist (f (ns n) x) (g x) ≤ 2 * 2⁻¹ ^ k

Tactic:
have h_inv_n_le_k : (2 : ℝ)⁻¹ ^ n ≤ 2 * (2 : ℝ)⁻¹ ^ k := by
  rw [mul_comm, ← inv_mul_le_iff₀' (zero_lt_two' ℝ)]
  conv_lhs =>
    congr
    rw [← pow_one (2 : ℝ)⁻¹]
  rw [← pow_add, add_comm]
  exact pow_le_pow_of_le_one (one_div (2 : ℝ) ▸ one_half_pos.le)
    (inv_le_one_of_one_le₀ one_le_two)
    ((le_tsub_add.trans (add_le_add_right (le_max_right _ _) 1)).trans
      (add_le_add_right hn_ge 1))

Result:
case intro.intro
α : 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
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ N ⊔ (k - 1)
hNx : dist (f (ns n) x) (g x) < 2⁻¹ ^ n
h_inv_n_le_k : 2⁻¹ ^ n ≤ 2 * 2⁻¹ ^ k
⊢ dist (f (ns n) x) (g x) ≤ 2 * 2⁻¹ ^ k