-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem exists_seq_tendstoInMeasure_atTop_iff [IsFiniteMeasure μ]
    {f : ℕ → α → E} (hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) {g : α → E} :
    TendstoInMeasure μ f atTop g ↔
      ∀ ns : ℕ → ℕ, StrictMono ns → ∃ ns' : ℕ → ℕ, StrictMono ns' ∧
        ∀ᵐ (ω : α) ∂μ, Tendsto (fun i ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
ε : ℝ
hε : 0 < ε
h2 : ¬Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
⊢ ∃ δ ns, 0 < δ ∧ StrictMono ns ∧ ∀ (n : ℕ), δ ≤ (μ {x | ε ≤ dist (f (ns n) x) (g x)}).toNNReal

Tactic:
obtain ⟨s, hs, h4⟩ := not_tendsto_iff_exists_frequently_nmem.1 h2

Result:
case intro.intro
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
ε : ℝ
hε : 0 < ε
h2 : ¬Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
s : Set ℝ≥0
hs : s ∈ 𝓝 0
h4 : ∃ᶠ (x : ℕ) in atTop, (μ {x_1 | ε ≤ dist (f x x_1) (g x_1)}).toNNReal ∉ s
⊢ ∃ δ ns, 0 < δ ∧ StrictMono ns ∧ ∀ (n : ℕ), δ ≤ (μ {x | ε ≤ dist (f (ns n) x) (g x)}).toNNReal

Proof state:
case intro.intro
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
ε : ℝ
hε : 0 < ε
h2 : ¬Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
⊢ ∃ ns,
    StrictMono ns ∧
      ∀ (ns' : ℕ → ℕ), StrictMono ns' → ¬∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))

Tactic:
obtain ⟨δ, ns, hδ, hns, h3⟩ : ∃ (δ : ℝ≥0) (ns : ℕ → ℕ), 0 < δ ∧ StrictMono ns ∧
    ∀ n, δ ≤ (μ {x | ε ≤ dist (f (ns n) x) (g x)}).toNNReal := by
  obtain ⟨s, hs, h4⟩ := not_tendsto_iff_exists_frequently_nmem.1 h2
  obtain ⟨δ, hδ, h5⟩ := NNReal.nhds_zero_basis.mem_iff.1 hs
  obtain ⟨ns, hns, h6⟩ := extraction_of_frequently_atTop h4
  exact ⟨δ, ns, hδ, hns, fun n ↦ Set.not_mem_Iio.1 (Set.not_mem_subset h5 (h6 n))⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
ε : ℝ
hε : 0 < ε
h2 : ¬Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
δ : ℝ≥0
ns : ℕ → ℕ
hδ : 0 < δ
hns : StrictMono ns
h3 : ∀ (n : ℕ), δ ≤ (μ {x | ε ≤ dist (f (ns n) x) (g x)}).toNNReal
⊢ ∃ ns,
    StrictMono ns ∧
      ∀ (ns' : ℕ → ℕ), StrictMono ns' → ¬∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
ε : ℝ
hε : 0 < ε
h2 : ¬Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
δ : ℝ≥0
ns : ℕ → ℕ
hδ : 0 < δ
hns : StrictMono ns
h3 : ∀ (n : ℕ), δ ≤ (μ {x | ε ≤ dist (f (ns n) x) (g x)}).toNNReal
ns' : ℕ → ℕ
x✝ : StrictMono ns'
h6 : ∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))
⊢ False

Tactic:
have h7 := tendstoInMeasure_iff_tendsto_toNNReal.mp <|
  tendstoInMeasure_of_tendsto_ae (fun n ↦ hf _) h6

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
ε : ℝ
hε : 0 < ε
h2 : ¬Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
δ : ℝ≥0
ns : ℕ → ℕ
hδ : 0 < δ
hns : StrictMono ns
h3 : ∀ (n : ℕ), δ ≤ (μ {x | ε ≤ dist (f (ns n) x) (g x)}).toNNReal
ns' : ℕ → ℕ
x✝ : StrictMono ns'
h6 : ∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))
h7 : ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => (μ {x | ε ≤ dist (f (ns (ns' i)) x) (g x)}).toNNReal) atTop (𝓝 0)
⊢ False

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 : ¬TendstoInMeasure μ f atTop g
⊢ ¬∀ (ns : ℕ → ℕ),
      StrictMono ns → ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))

Tactic:
rw [tendstoInMeasure_iff_tendsto_toNNReal] at h1

Result:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 : ¬∀ (ε : ℝ), 0 < ε → Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
⊢ ¬∀ (ns : ℕ → ℕ),
      StrictMono ns → ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
ε : ℝ
hε : 0 < ε
h2 : ¬Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
s : Set ℝ≥0
hs : s ∈ 𝓝 0
h4 : ∃ᶠ (x : ℕ) in atTop, (μ {x_1 | ε ≤ dist (f x x_1) (g x_1)}).toNNReal ∉ s
δ : ℝ≥0
hδ : 0 < δ
h5 : Set.Iio δ ⊆ s
⊢ ∃ δ ns, 0 < δ ∧ StrictMono ns ∧ ∀ (n : ℕ), δ ≤ (μ {x | ε ≤ dist (f (ns n) x) (g x)}).toNNReal

Tactic:
obtain ⟨ns, hns, h6⟩ := extraction_of_frequently_atTop h4

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
ε : ℝ
hε : 0 < ε
h2 : ¬Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
s : Set ℝ≥0
hs : s ∈ 𝓝 0
h4 : ∃ᶠ (x : ℕ) in atTop, (μ {x_1 | ε ≤ dist (f x x_1) (g x_1)}).toNNReal ∉ s
δ : ℝ≥0
hδ : 0 < δ
h5 : Set.Iio δ ⊆ s
ns : ℕ → ℕ
hns : StrictMono ns
h6 : ∀ (n : ℕ), (μ {x | ε ≤ dist (f (ns n) x) (g x)}).toNNReal ∉ s
⊢ ∃ δ ns, 0 < δ ∧ StrictMono ns ∧ ∀ (n : ℕ), δ ≤ (μ {x | ε ≤ dist (f (ns n) x) (g x)}).toNNReal

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 : ¬∀ (ε : ℝ), 0 < ε → Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
⊢ ¬∀ (ns : ℕ → ℕ),
      StrictMono ns → ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))

Tactic:
push_neg at *

Result:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 : ∃ ε, 0 < ε ∧ ¬Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
⊢ ∃ ns,
    StrictMono ns ∧
      ∀ (ns' : ℕ → ℕ), StrictMono ns' → ¬∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))