awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x
⊢ (Summable (α := ℝ≥0) fun (k : ℕ) ↦ HPow.hPow (α := ℝ≥0) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have h : ∀ (x : ℕ),
  HPow.hPow (α := ℝ≥0) 2 x =
    HSub.hSub (α := ℝ≥0) (↑(HPow.hPow (α := ℕ) 2 (x + 1)) : ℝ≥0) (↑(HPow.hPow (α := ℕ) 2 x) : ℝ≥0)
Tactic: convert!
    summable_schlomilch_iff hf (pow_pos zero_lt_two) (pow_right_strictMono₀ _root_.one_lt_two)
      two_ne_zero h_succ_diff
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) * f (u k)) ↔ Summable f
have lift : ∀ (f : (i : ℕ) → ℝ≥0)
  (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → LE.le (α := ℝ) ((fun (i : ℕ) ↦ (↑(f i) : ℝ)) n) ((fun (i : ℕ) ↦ (↑(f i) : ℝ)) m)),
  (Summable (α := ℝ) fun (k : ℕ) ↦
      HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) * (fun (i : ℕ) ↦ (↑(f i) : ℝ)) (u k)) ↔
    Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)
Tactic: lift f to ℕ → ℝ≥0 using h_nonneg
Cleared hypotheses: f, h_nonneg, hf
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : (i : ℕ) → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → LE.le (α := ℝ) ((fun (i : ℕ) ↦ (↑(f i) : ℝ)) n) ((fun (i : ℕ) ↦ (↑(f i) : ℝ)) m)
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦
      HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) * (fun (i : ℕ) ↦ (↑(f i) : ℝ)) (u k)) ↔
    Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)
have hf₁ : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
Tactic: simp only [NNReal.coe_le_coe] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : (i : ℕ) → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
k : ℕ
⊢ HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) = (↑(HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0)) : ℝ)
have this : LE.le (α := ℝ≥0) (↑(u k) : ℝ≥0) (↑(u k.succ) : ℝ≥0)
Tactic: have := Nat.cast_le (α := ℝ≥0).mpr <| (hu_strict k.lt_succ_self).le
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : (i : ℕ) → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) * (↑(f (u k)) : ℝ)) ↔
    Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)
have this : ∀ (k : ℕ),
  HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) = (↑(HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0)) : ℝ)
Tactic: have (k : ℕ) : (u (k + 1) - (u k : ℝ)) = ((u (k + 1) : ℝ≥0) - (u k : ℝ≥0) : ℝ≥0) := by
    have := Nat.cast_le (α := ℝ≥0).mpr <| (hu_strict k.lt_succ_self).le
    simp [NNReal.coe_sub this]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : (i : ℕ) → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
this :
  ∀ (k : ℕ),
    HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) =
      (↑(HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0)) : ℝ)
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) * (↑(f (u k)) : ℝ)) ↔
    Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)
have simp_rw : (Summable (α := ℝ) fun (k : ℕ) ↦ (↑(HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0)) : ℝ) * (↑(f (u k)) : ℝ)) ↔
  Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have h_succ_diff : SuccDiffBounded 2 fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x
Tactic: have h_succ_diff : SuccDiffBounded 2 (2 ^ ·) := by
    intro n
    simp [pow_succ, mul_two, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have h : ∀ (x : ℕ),
  HPow.hPow (α := ℝ) 2 x = HSub.hSub (α := ℝ) (↑(HPow.hPow (α := ℕ) 2 (x + 1)) : ℝ) (↑(HPow.hPow (α := ℕ) 2 x) : ℝ)
Tactic: convert!
    summable_schlomilch_iff_of_nonneg h_nonneg h_mono (pow_pos zero_lt_two)
      (pow_right_strictMono₀ one_lt_two) two_ne_zero h_succ_diff
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
f : ℕ → ℝ
h_nonneg : 0 ≤ᶠ[Filter.atTop] f
h_mono : ∀ᶠ (k : ℕ) in Filter.atTop, f (k + 1) ≤ f k
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have h_nonneg₁ : ∃ (a : ℕ), ∀ b ≥ a, 0 b ≤ f b
Tactic: rw [Filter.EventuallyLE, Filter.eventually_atTop] at h_nonneg
Cleared hypotheses: h_nonneg, h_mono
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
f : ℕ → ℝ
h_nonneg : ∃ (a : ℕ), ∀ b ≥ a, 0 b ≤ f b
h_mono : ∀ᶠ (k : ℕ) in Filter.atTop, f (k + 1) ≤ f k
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have h_mono₁ : ∃ (a : ℕ), ∀ b ≥ a, f (b + 1) ≤ f b
Tactic: rw [Filter.eventually_atTop] at h_mono
Cleared hypotheses: h_mono
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
h_nonneg : ∃ (a : ℕ), ∀ b ≥ a, 0 b ≤ f b
h_mono : ∃ (a : ℕ), ∀ b ≥ a, f (b + 1) ≤ f b
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have rcases : ∀ (n : ℕ) (hn : ∀ b ≥ n, 0 b ≤ f b),
  (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
Tactic: rcases h_nonneg with ⟨n, hn⟩
Cleared hypotheses: h_nonneg
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
h_mono : ∃ (a : ℕ), ∀ b ≥ a, f (b + 1) ≤ f b
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have rcases : ∀ (m : ℕ) (hm : ∀ b ≥ m, f (b + 1) ≤ f b),
  (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
Tactic: rcases h_mono with ⟨m, hm⟩
Cleared hypotheses: h_mono
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have h : (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔
  Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))
Tactic: convert! summable_condensed_iff_of_nonneg (f := fun k ↦ f (max k (n + m))) _ _ using 1
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h :
  (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔
    Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have h₁ : Summable f ↔ Summable (α := ℝ) fun (k : ℕ) ↦ f (max k (n + m))
Tactic: convert! summable_condensed_iff_of_nonneg (f := fun k ↦ f (max k (n + m))) _ _ using 1
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h :
  (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔
    Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))
h₁ : Summable f ↔ Summable (α := ℝ) fun (k : ℕ) ↦ f (max k (n + m))
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have convert_1 : ∀ (n_1 : ℕ), LE.le (α := ℝ) 0 ((fun (k : ℕ) ↦ f (max k (n + m))) n_1)
Tactic: convert! summable_condensed_iff_of_nonneg (f := fun k ↦ f (max k (n + m))) _ _ using 1
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h :
  (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔
    Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))
h₁ : Summable f ↔ Summable (α := ℝ) fun (k : ℕ) ↦ f (max k (n + m))
convert_1 : ∀ (n_1 : ℕ), LE.le (α := ℝ) 0 ((fun (k : ℕ) ↦ f (max k (n + m))) n_1)
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have convert_2 : ∀ ⦃m_1 n_1 : ℕ⦄,
  0 < m_1 → m_1 ≤ n_1 → LE.le (α := ℝ) ((fun (k : ℕ) ↦ f (max k (n + m))) n_1) ((fun (k : ℕ) ↦ f (max k (n + m))) m_1)
Tactic: convert! summable_condensed_iff_of_nonneg (f := fun k ↦ f (max k (n + m))) _ _ using 1
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔
    Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))
have h : Filter.EventuallyEq (β := ℝ) Filter.atTop (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k))
  fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))
Tactic: rw [summable_congr_atTop]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
⊢ Filter.EventuallyEq (β := ℝ) Filter.atTop (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k))
    fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))
have h_pow : Filter.Tendsto (β := ℕ) (fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n) Filter.atTop Filter.atTop
Tactic: have h_pow := tendsto_pow_atTop_atTop_of_one_lt (r := 2) (by simp)
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h_pow : Filter.Tendsto (β := ℕ) (fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n) Filter.atTop Filter.atTop
⊢ Filter.EventuallyEq (β := ℝ) Filter.atTop (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k))
    fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))
have h : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ n + m ≤ HPow.hPow (α := ℕ) 2 x) x} x →
        Membership.mem (γ := Set ℕ)
          {x : ℕ |
            (fun (x : ℕ) ↦
                Eq (α := ℝ) ((fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) x)
                  ((fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))) x))
              x}
          x}
    a
Tactic: filter_upwards [h_pow.eventually_ge_atTop (n + m)] with _ hk using by simp [max_eq_left hk]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h_pow : Filter.Tendsto (β := ℕ) (fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n) Filter.atTop Filter.atTop
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ n + m ≤ HPow.hPow (α := ℕ) 2 x) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  Eq (α := ℝ) ((fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) x)
                    ((fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))) x))
                x}
            x}
      a
⊢ Filter.EventuallyEq (β := ℝ) Filter.atTop (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k))
    fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))
have h₁ : ∀ (a : ℕ),
  n + m ≤ HPow.hPow (α := ℕ) 2 a →
    HPow.hPow (α := ℝ) 2 a * f (HPow.hPow (α := ℕ) 2 a) =
      HPow.hPow (α := ℝ) 2 a * f (max (HPow.hPow (α := ℕ) 2 a) (n + m))
Tactic: filter_upwards [h_pow.eventually_ge_atTop (n + m)] with _ hk using by simp [max_eq_left hk]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
⊢ Summable f ↔ Summable (α := ℝ) fun (k : ℕ) ↦ f (max k (n + m))
have h : f =ᶠ[Filter.atTop] fun (k : ℕ) ↦ f (max k (n + m))
Tactic: rw [summable_congr_atTop]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
⊢ f =ᶠ[Filter.atTop] fun (k : ℕ) ↦ f (max k (n + m))
have h : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ n + m ≤ x) x} x →
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ f x = (fun (k : ℕ) ↦ f (max k (n + m))) x) x} x}
    a
Tactic: filter_upwards [Filter.eventually_ge_atTop (n + m)] with _ hk using by simp [max_eq_left hk]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ n + m ≤ x) x} x →
          Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ f x = (fun (k : ℕ) ↦ f (max k (n + m))) x) x} x}
      a
⊢ f =ᶠ[Filter.atTop] fun (k : ℕ) ↦ f (max k (n + m))
have h₁ : ∀ (a : ℕ), n + m ≤ a → f a = f (max a (n + m))
Tactic: filter_upwards [Filter.eventually_ge_atTop (n + m)] with _ hk using by simp [max_eq_left hk]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
have inl : ∀ (hp : 0 ≤ p), (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
Tactic: rcases le_or_gt 0 p with hp | hp
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
inl : ∀ (hp : 0 ≤ p), (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
have inr : ∀ (hp : p < 0), (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
Tactic: rcases le_or_gt 0 p with hp | hp
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
hp : 0 ≤ p
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
have inl : (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * (HPow.hPow (α := ℝ) (↑(HPow.hPow (α := ℕ) 2 k) : ℝ) p)⁻¹) ↔
  1 < p
Tactic: rw [← summable_condensed_iff_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
hp : 0 ≤ p
inl :
  (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * (HPow.hPow (α := ℝ) (↑(HPow.hPow (α := ℕ) 2 k) : ℝ) p)⁻¹) ↔
    1 < p
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
have inl₁ : ∀ (n : ℕ), 0 ≤ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
Tactic: rw [← summable_condensed_iff_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
hp : 0 ≤ p
inl :
  (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * (HPow.hPow (α := ℝ) (↑(HPow.hPow (α := ℕ) 2 k) : ℝ) p)⁻¹) ↔
    1 < p
inl₁ : ∀ (n : ℕ), 0 ≤ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
have inl₂ : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹ ≤ (HPow.hPow (α := ℝ) (↑m : ℝ) p)⁻¹
Tactic: rw [← summable_condensed_iff_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
hp : 0 ≤ p
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * (HPow.hPow (α := ℝ) (↑(HPow.hPow (α := ℕ) 2 k) : ℝ) p)⁻¹) ↔
    1 < p
have inl : ‖2 * (HPow.hPow (α := ℝ) 2 p)⁻¹‖ < 1 ↔ 1 < p
Tactic: simp_rw [Nat.cast_pow, Nat.cast_two, ← rpow_natCast, ← rpow_mul zero_lt_two.le, mul_comm _ p,
        rpow_mul zero_lt_two.le, rpow_natCast, ← inv_pow, ← mul_pow,
        summable_geometric_iff_norm_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
hp : 0 ≤ p
⊢ ‖2 * (HPow.hPow (α := ℝ) 2 p)⁻¹‖ < 1 ↔ 1 < p
have inl : ‖HPow.hPow (α := ℝ) (β := ℝ) 2 1 * (HPow.hPow (α := ℝ) 2 p)⁻¹‖ < 1 ↔ 1 < p
Tactic: nth_rw 1 [← rpow_one 2]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
hp : 0 ≤ p
⊢ ‖HPow.hPow (α := ℝ) (β := ℝ) 2 1 * (HPow.hPow (α := ℝ) 2 p)⁻¹‖ < 1 ↔ 1 < p
have inl : Eq (α := ℝ) 2 0 ∧ 1 - p ≠ 0 ∨ LT.lt (α := ℝ) 1 2 ∧ 1 - p < 0 ∨ LT.lt (α := ℝ) 2 1 ∧ 0 < 1 - p ↔ 1 < p
Tactic: rw [← division_def, ← rpow_sub zero_lt_two, norm_eq_abs,
        abs_of_pos (rpow_pos_of_pos zero_lt_two _), rpow_lt_one_iff zero_lt_two.le]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
hp : 0 ≤ p
m n : ℕ
hm : 0 < m
hmn : m ≤ n
⊢ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹ ≤ (HPow.hPow (α := ℝ) (↑m : ℝ) p)⁻¹
have inl : 0 < HPow.hPow (α := ℝ) (↑m : ℝ) p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
hp : 0 ≤ p
m n : ℕ
hm : 0 < m
hmn : m ≤ n
inl : 0 < HPow.hPow (α := ℝ) (↑m : ℝ) p
⊢ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹ ≤ (HPow.hPow (α := ℝ) (↑m : ℝ) p)⁻¹
have inl₁ : LE.le (α := ℝ) 0 (↑m : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
p : ℝ
hp : p < 0
this : ¬Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
have this₁ : ¬1 < p
Tactic: have : ¬1 < p := fun hp₁ => hp.not_ge (zero_le_one.trans hp₁.le)
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
hp : p < 0
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
have inr : ¬Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
Tactic: suffices ¬Summable (fun n => ((n : ℝ) ^ p)⁻¹ : ℕ → ℝ) by
      have : ¬1 < p := fun hp₁ => hp.not_ge (zero_le_one.trans hp₁.le)
      simpa only [this, iff_false]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
hp : p < 0
h : Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
⊢ False
have inr : ∀ (k : ℕ) (hk₁ : (HPow.hPow (α := ℝ) (↑k : ℝ) p)⁻¹ < 1) (hk₀ : k ≠ 0), False
Tactic: obtain ⟨k : ℕ, hk₁ : ((k : ℝ) ^ p)⁻¹ < 1, hk₀ : k ≠ 0⟩ :=
      ((h.tendsto_cofinite_zero.eventually (gt_mem_nhds zero_lt_one)).and
          (eventually_cofinite_ne 0)).exists
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
hp : p < 0
h : Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
k : ℕ
hk₁ : (HPow.hPow (α := ℝ) (↑k : ℝ) p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ False
have inr : k = 0
Tactic: apply hk₀
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
p : ℝ
hp : p < 0
h : Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
k : ℕ
hk₁ : (HPow.hPow (α := ℝ) (↑k : ℝ) p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ k = 0
have hk₂ : LT.lt (α := ℝ) 0 (↑k : ℝ)
Tactic: rw [← pos_iff_ne_zero, ← @Nat.cast_pos ℝ] at hk₀
Cleared hypotheses: hk₀
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℝ
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) p) ↔ p < -1
have rcases : ∀ (p : ℝ), (Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-p)) ↔ -p < -1
Tactic: rcases neg_surjective p with ⟨p, rfl⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℕ
⊢ (Summable (α := ℝ) fun (n : ℤ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) ↔ 1 < p
have refine : ∀ (h : 1 < p) (n : ℕ),
  1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (↑(-(↑n : ℤ)) : ℝ) p
Tactic: refine ⟨fun h ↦ summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective),
    fun h ↦ .of_nat_of_neg (summable_one_div_nat_pow.mpr h)
      (((summable_one_div_nat_pow.mpr h).mul_left <| 1 / (-1 : ℝ) ^ p).congr fun n ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (↑(-(↑n : ℤ)) : ℝ) p
have rw : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (-(↑(↑n : ℤ) : ℝ)) p
Tactic: rw [Int.cast_neg, Int.cast_natCast, neg_eq_neg_one_mul (n : ℝ), mul_pow, mul_one_div, div_div]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℕ
h : 1 < p
n : ℕ
rw : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (-(↑(↑n : ℤ) : ℝ)) p
⊢ 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (↑(-(↑n : ℤ)) : ℝ) p
have rw₁ : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (-(↑n : ℝ)) p
Tactic: rw [Int.cast_neg, Int.cast_natCast, neg_eq_neg_one_mul (n : ℝ), mul_pow, mul_one_div, div_div]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℕ
h : 1 < p
n : ℕ
rw : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (-(↑(↑n : ℤ) : ℝ)) p
rw₁ : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (-(↑n : ℝ)) p
⊢ 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (↑(-(↑n : ℤ)) : ℝ) p
have rw₂ : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HMul.hMul (α := ℝ) (-1) (↑n : ℝ) ^ p
Tactic: rw [Int.cast_neg, Int.cast_natCast, neg_eq_neg_one_mul (n : ℝ), mul_pow, mul_one_div, div_div]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℕ
h : 1 < p
n : ℕ
rw : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (-(↑(↑n : ℤ) : ℝ)) p
rw₁ : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (-(↑n : ℝ)) p
rw₂ : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HMul.hMul (α := ℝ) (-1) (↑n : ℝ) ^ p
⊢ 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (↑(-(↑n : ℤ)) : ℝ) p
have rw₃ : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) =
  1 / (HPow.hPow (α := ℝ) (-1) p * HPow.hPow (α := ℝ) (↑n : ℝ) p)
Tactic: rw [Int.cast_neg, Int.cast_natCast, neg_eq_neg_one_mul (n : ℝ), mul_pow, mul_one_div, div_div]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℕ
h : 1 < p
n : ℕ
rw : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (-(↑(↑n : ℤ) : ℝ)) p
rw₁ : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (-(↑n : ℝ)) p
rw₂ : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HMul.hMul (α := ℝ) (-1) (↑n : ℝ) ^ p
rw₃ :
  1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) =
    1 / (HPow.hPow (α := ℝ) (-1) p * HPow.hPow (α := ℝ) (↑n : ℝ) p)
⊢ 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (↑(-(↑n : ℤ)) : ℝ) p
have rw₄ : 1 / HPow.hPow (α := ℝ) (-1) p / HPow.hPow (α := ℝ) (↑n : ℝ) p =
  1 / (HPow.hPow (α := ℝ) (-1) p * HPow.hPow (α := ℝ) (↑n : ℝ) p)
Tactic: rw [Int.cast_neg, Int.cast_natCast, neg_eq_neg_one_mul (n : ℝ), mul_pow, mul_one_div, div_div]