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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

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

Premises used: ENNReal.tsum_le_tsum, ne_top_of_le_ne_top, MeasureTheory.measure_limsup_atTop_eq_zero
-- 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
refine : Ne (α := ℝ≥0∞) (∑' (a : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ a) ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

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

Premises used: ENNReal.tsum_le_tsum, ne_top_of_le_ne_top, MeasureTheory.measure_limsup_atTop_eq_zero
-- 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
⊢ Ne (α := ℝ≥0∞) (∑' (a : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ a) ∞

Tactic:
simpa only [ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, inv_inv] using ENNReal.ofNat_ne_top

Premises used: ENNReal.ofNat_ne_top, ENNReal.one_sub_inv_two, inv_inv, ENNReal.tsum_geometric
-- 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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

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
-- 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:
fun x hx => EMetric.tendsto_atTop.mpr fun ε hε => ?_

Premises used: Iff.mpr, EMetric.tendsto_atTop
-- 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∞)
refine : ∀ (x : α) (hx : x ∈ sᶜ) (ε : ℝ≥0∞) (hε : ε > 0), ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
⊢ ∀ x ∈ sᶜ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
refine fun x hx => EMetric.tendsto_atTop.mpr fun ε hε => ?_

Premises used: Iff.mpr, EMetric.tendsto_atTop
-- 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 : α
hx : x ∈ sᶜ
ε : ℝ≥0∞
hε : ε > 0
rw :
  ∀ (hx : Membership.mem (γ := Set α) (⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), S i)ᶜ x) (ε : ℝ≥0∞) (hε : ε > 0),
    ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε

Tactic:
rw [hs, limsup_eq_iInf_iSup_of_nat] at hx

Premises used: Filter.limsup_eq_iInf_iSup_of_nat
-- 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 : α
hx : Membership.mem (γ := Set α) (⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), S i)ᶜ x
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ (i : ℕ), ∀ (i_1 : ℕ) (i : i_1 ≥ i), edist (f (ns i_1) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ i_1

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

Premises used: not_le, Set.compl_iInter, Set.iInf_eq_iInter, Set.mem_iUnion, Set.iSup_eq_iUnion, Set.mem_setOf_eq, Set.mem_iInter, Set.compl_iUnion, Set.mem_compl_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∞)
x : α
ε : ℝ≥0∞
hε : ε > 0
hx : ∃ (i : ℕ), ∀ (i_1 : ℕ) (i : i_1 ≥ i), edist (f (ns i_1) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ i_1
obtain :
  ∀ (N : ℕ) (hNx : ∀ (i : ℕ) (i_1 : i ≥ N), edist (f (ns i) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ i),
    ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε

Tactic:
obtain ⟨N, hNx⟩ := hx
-- 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 : ℕ
hNx : ∀ (i : ℕ) (i_1 : i ≥ N), edist (f (ns i) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ i
obtain : ∀ (k : ℕ) (hk_lt_ε : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε), ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε

Tactic:
obtain ⟨k, hk_lt_ε⟩ := h_lt_ε_real ε hε
-- 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 : ℕ
hNx : ∀ (i : ℕ) (i_1 : i ≥ N), edist (f (ns i) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ i
k : ℕ
hk_lt_ε : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε

Tactic:
⟨max N (k - 1), fun n hn_ge => lt_of_le_of_lt ?_ hk_lt_ε⟩

Premises used: lt_of_le_of_lt, HSub.hSub, Max.max, Exists.intro, OfNat.ofNat
-- 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 : ℕ
hNx : ∀ (i : ℕ) (i_1 : i ≥ N), edist (f (ns i) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ i
k : ℕ
hk_lt_ε : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
refine : ∀ (n : ℕ) (hn_ge : n ≥ max N (k - 1)), edist (f (ns n) x) (g x) ≤ 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε

Tactic:
refine ⟨max N (k - 1), fun n hn_ge => lt_of_le_of_lt ?_ hk_lt_ε⟩
-- 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 : ℕ
hNx : ∀ (i : ℕ) (i_1 : i ≥ N), edist (f (ns i) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ i
k : ℕ
hk_lt_ε : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
⊢ edist (f (ns n) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n

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

Premises used: LE.le.trans, le_max_left
-- 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
nth_rw : HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k

Tactic:
nth_rw 2 [← pow_one (2 : ℝ≥0∞)]

Premises used: pow_one, OfNat.ofNat
-- 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
rw : HPow.hPow (α := ℝ≥0∞) 2 k ≤ HPow.hPow (α := ℝ≥0∞) 2 (n + 1)
h₁ : HPow.hPow (α := ℝ≥0∞) 2 n * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 = ∞ → (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ ≠ 0
h₂ : (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ = ∞ → HPow.hPow (α := ℝ≥0∞) 2 n * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 ≠ 0
h₃ : (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 = ∞ → HPow.hPow (α := ℝ≥0∞) 2 n ≠ 0
h₄ : HPow.hPow (α := ℝ≥0∞) 2 n = ∞ → (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 ≠ 0
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k

Tactic:
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]

Premises used: mul_assoc, ENNReal.inv_le_iff_le_mul, pow_add, HPow.hPow, inv_inv, mul_comm, ENNReal.inv_pow
-- 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
ha : LE.le (α := ℝ≥0∞) 1 2
hmn : k ≤ n + 1
⊢ HPow.hPow (α := ℝ≥0∞) 2 k ≤ HPow.hPow (α := ℝ≥0∞) 2 (n + 1)

Tactic:
gcongr
-- 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
⊢ LE.le (α := ℝ≥0∞) 1 2

Tactic:
simp
-- 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
⊢ k ≤ n + 1

Tactic:
omega
-- 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
⊢ HPow.hPow (α := ℝ≥0∞) 2 n * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 = ∞ → (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ ≠ 0

Tactic:
simp
-- 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
⊢ (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ = ∞ → HPow.hPow (α := ℝ≥0∞) 2 n * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 ≠ 0

Tactic:
simp
-- 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
⊢ (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 = ∞ → HPow.hPow (α := ℝ≥0∞) 2 n ≠ 0

Tactic:
simp
-- 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
⊢ HPow.hPow (α := ℝ≥0∞) 2 n = ∞ → (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 ≠ 0

Tactic:
simp
-- 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
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k

Tactic:
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
-- 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:
le_trans hNx.le h_inv_n_le_k

Premises used: LT.lt.le, le_trans