awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
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
N k : ℕ
hk_lt_ε : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : edist (f (ns n) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
h_inv_n_le_k : HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
⊢ edist (f (ns n) x) (g x) ≤ 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k

Tactic:
exact le_trans hNx.le h_inv_n_le_k

Premises used: LT.lt.le, le_trans
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
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))

Tactic:
have h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x)) := by
    refine fun x hx => EMetric.tendsto_atTop.mpr fun ε hε => ?_
    rw [hs, limsup_eq_iInf_iSup_of_nat] at hx
    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
    obtain ⟨N, hNx⟩ := hx
    obtain ⟨k, hk_lt_ε⟩ := h_lt_ε_real ε hε
    refine ⟨max N (k - 1), fun n hn_ge => lt_of_le_of_lt ?_ hk_lt_ε⟩
    specialize hNx n ((le_max_left _ _).trans hn_ge)
    have h_inv_n_le_k : (2 : ℝ≥0∞)⁻¹ ^ n ≤ 2 * (2 : ℝ≥0∞)⁻¹ ^ k := by
      nth_rw 2 [← pow_one (2 : ℝ≥0∞)]
      rw [mul_comm, ← ENNReal.inv_pow, ← ENNReal.inv_pow, ENNReal.inv_le_iff_le_mul, ← mul_assoc,
        mul_comm (_ ^ n), mul_assoc, ← ENNReal.inv_le_iff_le_mul, inv_inv, ← pow_add]
      · gcongr
        · simp
        · omega
      all_goals simp
    exact le_trans hNx.le h_inv_n_le_k
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
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∞)
h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
h :
  StrictMono ns ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Tendsto (fun (i : ℕ) ↦ f (ns i) a) atTop (𝓝 (g a))} : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
rw [ae_iff]

Premises used: MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
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∞)
h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
⊢ StrictMono ns ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Tendsto (fun (i : ℕ) ↦ f (ns i) a) atTop (𝓝 (g a))} : ℝ≥0∞)
      (0 : ℝ≥0∞)

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

Premises used: MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono, MeasureTheory.measure_mono_null, And.intro
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
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∞)
h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
h : ∀ (x : α), Membership.mem (γ := Set α) {a : α | ¬Tendsto (fun (i : ℕ) ↦ f (ns i) a) atTop (𝓝 (g a))} x → x ∈ s
⊢ StrictMono ns ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Tendsto (fun (i : ℕ) ↦ f (ns i) a) atTop (𝓝 (g a))} : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
refine ⟨ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono hfg, measure_mono_null (fun x => ?_) hμs⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
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∞)
h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
x : α
h : x ∉ s → Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
⊢ Membership.mem (γ := Set α) {a : α | ¬Tendsto (fun (i : ℕ) ↦ f (ns i) a) atTop (𝓝 (g a))} x → x ∈ s

Tactic:
rw [Set.mem_setOf_eq, ← @Classical.not_not (x ∈ s), not_imp_not]

Premises used: Classical.not_not, Set.mem_setOf_eq, not_imp_not
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
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∞)
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:
h_tendsto x

Premises used: Set.Mem, setOf, Not
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
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∞)
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
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop u

Tactic:
exists_seq_tendsto u

Premises used: Filter.exists_seq_tendsto
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
obtain :
  ∀ (ns : ℕ → ι) (h_tendsto_ns : Tendsto ns atTop u),
    ∃ (ns : ℕ → ι), Tendsto ns atTop u ∧ TendstoInMeasure μ (fun (n : ℕ) ↦ f (ns n)) atTop g
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop u ∧ TendstoInMeasure μ (fun (n : ℕ) ↦ f (ns n)) atTop g

Tactic:
obtain ⟨ns, h_tendsto_ns⟩ : ∃ ns : ℕ → ι, Tendsto ns atTop u := exists_seq_tendsto u

Premises used: Filter.exists_seq_tendsto
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ns : ℕ → ι
h_tendsto_ns : Tendsto ns atTop u
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop u ∧ TendstoInMeasure μ (fun (n : ℕ) ↦ f (ns n)) atTop g

Tactic:
⟨ns, h_tendsto_ns, fun ε hε => (hfg ε hε).comp h_tendsto_ns⟩

Premises used: And.intro, Exists.intro, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ns : ℕ → ι
h_tendsto_ns : Tendsto ns atTop u
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop u ∧ TendstoInMeasure μ (fun (n : ℕ) ↦ f (ns n)) atTop g

Tactic:
exact ⟨ns, h_tendsto_ns, fun ε hε => (hfg ε hε).comp h_tendsto_ns⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
obtain :
  ∀ (ms : ℕ → ι) (hms1 : Tendsto ms atTop u) (hms2 : TendstoInMeasure μ (fun (n : ℕ) ↦ f (ms n)) atTop g),
    ∃ (ns : ℕ → ι), Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
obtain ⟨ms, hms1, hms2⟩ := hfg.exists_seq_tendstoInMeasure_atTop

Premises used: MeasureTheory.TendstoInMeasure.exists_seq_tendstoInMeasure_atTop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ms : ℕ → ι
hms1 : Tendsto ms atTop u
hms2 : TendstoInMeasure μ (fun (n : ℕ) ↦ f (ms n)) atTop g
obtain :
  ∀ (ns : ℕ → ℕ) (hns1 : StrictMono ns) (hns2 : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ms (ns i)) x) atTop (𝓝 (g x))),
    ∃ (ns : ℕ → ι), Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
obtain ⟨ns, hns1, hns2⟩ := hms2.exists_seq_tendsto_ae

Premises used: MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ms : ℕ → ι
hms1 : Tendsto ms atTop u
hms2 : TendstoInMeasure μ (fun (n : ℕ) ↦ f (ms n)) atTop g
ns : ℕ → ℕ
hns1 : StrictMono ns
hns2 : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ms (ns i)) x) atTop (𝓝 (g x))
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
⟨ms ∘ ns, hms1.comp hns1.tendsto_atTop, hns2⟩

Premises used: Function.comp, StrictMono.tendsto_atTop, And.intro, Exists.intro, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ms : ℕ → ι
hms1 : Tendsto ms atTop u
hms2 : TendstoInMeasure μ (fun (n : ℕ) ↦ f (ms n)) atTop g
ns : ℕ → ℕ
hns1 : StrictMono ns
hns2 : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ms (ns i)) x) atTop (𝓝 (g x))
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
exact ⟨ms ∘ ns, hms1.comp hns1.tendsto_atTop, hns2⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : 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:
⟨fun hfg _ hns ↦ (hfg.comp hns.tendsto_atTop).exists_seq_tendsto_ae, fun h1 ↦ ?_⟩

Premises used: StrictMono.tendsto_atTop, MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae, Iff.intro, MeasureTheory.TendstoInMeasure.comp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
refine :
  ∀
    (h1 :
      ∀ (ns : ℕ → ℕ),
        StrictMono ns →
          ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))),
    TendstoInMeasure μ f atTop g
⊢ 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, fun h1 ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
rw :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
        atTop (𝓝 0)
⊢ TendstoInMeasure μ f atTop g

Tactic:
rw [tendstoInMeasure_iff_tendsto_toNNReal]

Premises used: MeasureTheory.tendstoInMeasure_iff_tendsto_toNNReal
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
by_contra! :
  ∀ (ε : ℝ≥0∞) (hε : 0 < ε)
    (h2 :
      ¬Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
          atTop (𝓝 0)),
    False
⊢ ∀ (ε : ℝ≥0∞),
    0 < ε →
      Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
        atTop (𝓝 0)

Tactic:
by_contra! ⟨ε, hε, h2⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 :
  ¬Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
      atTop (𝓝 0)
obtain :
  ∀ (s : Set ℝ≥0) (hs : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) s)
    (h4 : ∃ᶠ (x : ℕ) in atTop, ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) ∉ s),
    ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
      0 < δ ∧
        StrictMono ns ∧
          ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
⊢ ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
    0 < δ ∧
      StrictMono ns ∧ ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})

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

Premises used: Filter.not_tendsto_iff_exists_frequently_notMem, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 :
  ¬Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
      atTop (𝓝 0)
s : Set ℝ≥0
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) s
h4 : ∃ᶠ (x : ℕ) in atTop, ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) ∉ s
obtain :
  ∀ (δ : ℝ≥0) (hδ : 0 < δ) (h5 : Set.Iio δ ⊆ s),
    ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
      0 < δ ∧
        StrictMono ns ∧
          ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
⊢ ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
    0 < δ ∧
      StrictMono ns ∧ ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})

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

Premises used: Filter.HasBasis.mem_iff, Iff.mp, NNReal.nhds_zero_basis
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 :
  ¬Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
      atTop (𝓝 0)
s : Set ℝ≥0
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) s
h4 : ∃ᶠ (x : ℕ) in atTop, ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) ∉ s
δ : ℝ≥0
hδ : 0 < δ
h5 : Set.Iio δ ⊆ s
obtain :
  ∀ (ns : ℕ → ℕ) (hns : StrictMono ns)
    (h6 : ∀ (n : ℕ), ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)}) ∉ s),
    ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
      0 < δ ∧
        StrictMono ns ∧
          ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
⊢ ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
    0 < δ ∧
      StrictMono ns ∧ ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})

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

Premises used: Filter.extraction_of_frequently_atTop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 :
  ¬Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
      atTop (𝓝 0)
s : Set ℝ≥0
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) s
h4 : ∃ᶠ (x : ℕ) in atTop, ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) ∉ s
δ : ℝ≥0
hδ : 0 < δ
h5 : Set.Iio δ ⊆ s
ns : ℕ → ℕ
hns : StrictMono ns
h6 : ∀ (n : ℕ), ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)}) ∉ s
⊢ ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
    0 < δ ∧
      StrictMono ns ∧ ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})

Tactic:
⟨δ, ns, hδ, hns, fun n ↦ Set.notMem_Iio.1 (Set.notMem_subset h5 (h6 n))⟩

Premises used: And.intro, Exists.intro, Iff.mp, Set.notMem_Iio, Set.notMem_subset
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 :
  ¬Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
      atTop (𝓝 0)
s : Set ℝ≥0
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) s
h4 : ∃ᶠ (x : ℕ) in atTop, ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) ∉ s
δ : ℝ≥0
hδ : 0 < δ
h5 : Set.Iio δ ⊆ s
ns : ℕ → ℕ
hns : StrictMono ns
h6 : ∀ (n : ℕ), ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)}) ∉ s
⊢ ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
    0 < δ ∧
      StrictMono ns ∧ ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})

Tactic:
exact ⟨δ, ns, hδ, hns, fun n ↦ Set.notMem_Iio.1 (Set.notMem_subset h5 (h6 n))⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 :
  ¬Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
      atTop (𝓝 0)
obtain :
  ∀ (δ : ℝ≥0) (ns : ℕ → ℕ) (hδ : 0 < δ) (hns : StrictMono ns)
    (h3 : ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})), False
⊢ False

Tactic:
obtain ⟨δ, ns, hδ, hns, h3⟩ : ∃ (δ : ℝ≥0) (ns : ℕ → ℕ), 0 < δ ∧ StrictMono ns ∧
      ∀ n, δ ≤ (μ {x | ε ≤ edist (f (ns n) x) (g x)}).toNNReal := by
    obtain ⟨s, hs, h4⟩ := not_tendsto_iff_exists_frequently_notMem.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.notMem_Iio.1 (Set.notMem_subset h5 (h6 n))⟩