-- 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:
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'
⊢ ¬∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))

Tactic:
by_contra 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 ω))
⊢ 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
⊢ TendstoInMeasure μ f atTop g ↔
    ∀ (ns : ℕ → ℕ),
      StrictMono ns → ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))

Tactic:
refine ⟨fun hfg _ hns ↦ (hfg.comp hns.tendsto_atTop).exists_seq_tendsto_ae,
  not_imp_not.mp (fun 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 : ¬TendstoInMeasure μ f atTop g
⊢ ¬∀ (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)
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

Tactic:
exact ⟨δ, ns, hδ, hns, fun n ↦ Set.not_mem_Iio.1 (Set.not_mem_subset h5 (h6 n))⟩

Result:
no goals

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,
    StrictMono ns ∧
      ∀ (ns' : ℕ → ℕ), StrictMono ns' → ¬∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))

Tactic:
refine ⟨ns, hns, fun ns' _ ↦ ?_⟩

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'
⊢ ¬∀ᵐ (ω : α) ∂μ, 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 ω))
h7 : ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => (μ {x | ε ≤ dist (f (ns (ns' i)) x) (g x)}).toNNReal) atTop (𝓝 0)
⊢ False

Tactic:
exact lt_irrefl _ (lt_of_le_of_lt (ge_of_tendsto' (h7 ε hε) (fun n ↦ h3 _)) hδ)

Result:
no goals

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:
obtain ⟨ε, hε, h2⟩ := h1

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)
⊢ ∃ ns,
    StrictMono ns ∧
      ∀ (ns' : ℕ → ℕ), StrictMono ns' → ¬∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f (ns (ns' i)) ω) atTop (𝓝 (g ω))

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)
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

Tactic:
obtain ⟨δ, hδ, h5⟩ := NNReal.nhds_zero_basis.mem_iff.1 hs

Result:
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