awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
have obtain : ∀ (k : ℕ) (hk_lt_ε : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k < ε), ∃ (N : ℕ), ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
Tactic: obtain ⟨k, hk_lt_ε⟩ := h_lt_ε_real ε hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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) < ε
have refine : ∀ (n : ℕ) (hn_ge : n ≥ max N (k - 1)), edist (f (ns n) x) (g x) ≤ 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
Tactic: refine ⟨max N (k - 1), fun n hn_ge => lt_of_le_of_lt ?_ hk_lt_ε⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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) ≤ 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
have hNx₁ : edist (f (ns n) x) (g x) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Tactic: specialize hNx n ((le_max_left _ _).trans hn_ge)
Cleared hypotheses: hNx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
have nth_rw : HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
Tactic: nth_rw 2 [← pow_one (2 : ℝ≥0∞)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
have rw : HPow.hPow (α := ℝ≥0∞) 2 k ≤ HPow.hPow (α := ℝ≥0∞) 2 (n + 1)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
have h₁ : HPow.hPow (α := ℝ≥0∞) 2 n * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 = ∞ → (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ ≠ 0
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
have h₂ : (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ = ∞ → HPow.hPow (α := ℝ≥0∞) 2 n * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 ≠ 0
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
have h₃ : (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 = ∞ → HPow.hPow (α := ℝ≥0∞) 2 n ≠ 0
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
have h₄ : HPow.hPow (α := ℝ≥0∞) 2 n = ∞ → (HPow.hPow (α := ℝ≥0∞) 2 k)⁻¹ * HPow.hPow (α := ℝ≥0∞) (β := ℕ) 2 1 ≠ 0
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 + 1)
have ha : LE.le (α := ℝ≥0∞) 1 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) 2 k ≤ HPow.hPow (α := ℝ≥0∞) 2 (n + 1)
have hmn : k ≤ n + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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
⊢ edist (f (ns n) x) (g x) ≤ 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
have h_inv_n_le_k : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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∞)
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
have h_tendsto : ∀ 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
have h : StrictMono ns ∧
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Tendsto (fun (i : ℕ) ↦ f (ns i) a) atTop (𝓝 (g a))} : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [ae_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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∞)
have h : ∀ (x : α), Membership.mem (γ := Set α) {a : α | ¬Tendsto (fun (i : ℕ) ↦ f (ns i) a) atTop (𝓝 (g a))} x → x ∈ s
Tactic: refine ⟨ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono hfg, measure_mono_null (fun x => ?_) hμs⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 : α
⊢ Membership.mem (γ := Set α) {a : α | ¬Tendsto (fun (i : ℕ) ↦ f (ns i) a) atTop (𝓝 (g a))} x → x ∈ s
have h : x ∉ s → Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
Tactic: rw [Set.mem_setOf_eq, ← @Classical.not_not (x ∈ s), not_imp_not]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 ∧ TendstoInMeasure μ (fun (n : ℕ) ↦ f (ns n)) atTop g
have obtain : ∀ (ns : ℕ → ι) (h_tendsto_ns : Tendsto ns atTop u),
  ∃ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
have 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))
Tactic: obtain ⟨ms, hms1, hms2⟩ := hfg.exists_seq_tendstoInMeasure_atTop
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 : ℕ → ι), Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
have 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))
Tactic: obtain ⟨ns, hns1, hns2⟩ := hms2.exists_seq_tendsto_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 ω))
have refine : ∀
  (h1 :
    ∀ (ns : ℕ → ℕ),
      StrictMono ns →
        ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))),
  TendstoInMeasure μ f atTop g
Tactic: refine ⟨fun hfg _ hns ↦ (hfg.comp hns.tendsto_atTop).exists_seq_tendsto_ae, fun h1 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 ω))
⊢ TendstoInMeasure μ f atTop g
have rw : ∀ (ε : ℝ≥0∞),
  0 < ε →
    Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
      atTop (𝓝 0)
Tactic: rw [tendstoInMeasure_iff_tendsto_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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∞),
    0 < ε →
      Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
        atTop (𝓝 0)
have 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
Tactic: by_contra! ⟨ε, hε, h2⟩