awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst :
  ∀ (x y : ℤ_[p]),
    ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
      ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
        ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
n i : ℕ
h : i ∈ range (n + 1)
⊢ ‖(HPow.hPow (α := ℤ) (-1) (n - i) * (↑(n.choose i) : ℤ)) •
        HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
          ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖ ≤
    ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
have calc : ‖(HPow.hPow (α := ℤ) (-1) (n - i) * (↑(n.choose i) : ℤ)) •
      HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
        ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖ ≤
  ‖HPow.hPow (α := ℤ_[p]) (↑(-1) : ℤ_[p]) (n - i) * (↑(n.choose i) : ℤ_[p])‖ *
    ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
        ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖
Tactic: calc ‖((-1 : ℤ) ^ (n - i) * n.choose i) • (f (i + ↑(p ^ t)) - f i)‖
    _ ≤ ‖((-1 : ℤ) ^ (n - i) * n.choose i : ℤ_[p])‖ * ‖(f (i + ↑(p ^ t)) - f i)‖ := by
      rw [← Int.cast_smul_eq_zsmul ℤ_[p]]
      exact (norm_smul_le ..).trans (by norm_cast)
    _ ≤ ‖f (i + ↑(p ^ t)) - f i‖ := by
      apply mul_le_of_le_one_left (norm_nonneg _)
      simpa only [← coe_intCast] using norm_le_one _
    _ ≤ ‖f‖ / p ^ s := by
      apply hst
      rw [Nat.cast_pow, add_sub_cancel_left, norm_pow, norm_p, inv_pow, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst :
  ∀ (x y : ℤ_[p]),
    ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
      ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
        ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
n i : ℕ
h : i ∈ range (n + 1)
calc :
  ‖(HPow.hPow (α := ℤ) (-1) (n - i) * (↑(n.choose i) : ℤ)) •
        HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
          ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖ ≤
    ‖HPow.hPow (α := ℤ_[p]) (↑(-1) : ℤ_[p]) (n - i) * (↑(n.choose i) : ℤ_[p])‖ *
      ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
          ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖
⊢ ‖(HPow.hPow (α := ℤ) (-1) (n - i) * (↑(n.choose i) : ℤ)) •
        HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
          ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖ ≤
    ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
have calc₁ : ‖HPow.hPow (α := ℤ_[p]) (↑(-1) : ℤ_[p]) (n - i) * (↑(n.choose i) : ℤ_[p])‖ *
    ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
        ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖ ≤
  ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
      ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖
Tactic: calc ‖((-1 : ℤ) ^ (n - i) * n.choose i) • (f (i + ↑(p ^ t)) - f i)‖
    _ ≤ ‖((-1 : ℤ) ^ (n - i) * n.choose i : ℤ_[p])‖ * ‖(f (i + ↑(p ^ t)) - f i)‖ := by
      rw [← Int.cast_smul_eq_zsmul ℤ_[p]]
      exact (norm_smul_le ..).trans (by norm_cast)
    _ ≤ ‖f (i + ↑(p ^ t)) - f i‖ := by
      apply mul_le_of_le_one_left (norm_nonneg _)
      simpa only [← coe_intCast] using norm_le_one _
    _ ≤ ‖f‖ / p ^ s := by
      apply hst
      rw [Nat.cast_pow, add_sub_cancel_left, norm_pow, norm_p, inv_pow, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst :
  ∀ (x y : ℤ_[p]),
    ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
      ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
        ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
n i : ℕ
h : i ∈ range (n + 1)
calc :
  ‖(HPow.hPow (α := ℤ) (-1) (n - i) * (↑(n.choose i) : ℤ)) •
        HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
          ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖ ≤
    ‖HPow.hPow (α := ℤ_[p]) (↑(-1) : ℤ_[p]) (n - i) * (↑(n.choose i) : ℤ_[p])‖ *
      ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
          ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖
calc₁ :
  ‖HPow.hPow (α := ℤ_[p]) (↑(-1) : ℤ_[p]) (n - i) * (↑(n.choose i) : ℤ_[p])‖ *
      ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
          ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖ ≤
    ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
        ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖
⊢ ‖(HPow.hPow (α := ℤ) (-1) (n - i) * (↑(n.choose i) : ℤ)) •
        HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
          ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖ ≤
    ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
have calc₂ : ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
      ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖ ≤
  ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
Tactic: calc ‖((-1 : ℤ) ^ (n - i) * n.choose i) • (f (i + ↑(p ^ t)) - f i)‖
    _ ≤ ‖((-1 : ℤ) ^ (n - i) * n.choose i : ℤ_[p])‖ * ‖(f (i + ↑(p ^ t)) - f i)‖ := by
      rw [← Int.cast_smul_eq_zsmul ℤ_[p]]
      exact (norm_smul_le ..).trans (by norm_cast)
    _ ≤ ‖f (i + ↑(p ^ t)) - f i‖ := by
      apply mul_le_of_le_one_left (norm_nonneg _)
      simpa only [← coe_intCast] using norm_le_one _
    _ ≤ ‖f‖ / p ^ s := by
      apply hst
      rw [Nat.cast_pow, add_sub_cancel_left, norm_pow, norm_p, inv_pow, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
⊢ Tendsto.{0, u_1} (β := E) (fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0) atTop (𝓝 0)
have refine : ∀ (ε : ℝ) (hε : ε > 0), ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) < ε
Tactic: refine NormedAddGroup.tendsto_nhds_zero.mpr (fun ε hε ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) < ε
have this : Tendsto (β := ℝ) (fun (s : ℕ) ↦ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0)
Tactic: have : Tendsto (fun s ↦ ‖f‖ / p ^ s) _ _ := tendsto_const_nhds.div_atTop
    (tendsto_pow_atTop_atTop_of_one_lt (mod_cast hp.out.one_lt))
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (β := ℝ) (fun (s : ℕ) ↦ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0)
⊢ ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) < ε
have obtain : ∀ (s : ℕ) (hs : ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε),
  ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) < ε
Tactic: obtain ⟨s, hs⟩ := (this.eventually_lt_const hε).exists
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (β := ℝ) (fun (s : ℕ) ↦ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε
⊢ ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) < ε
have refine : ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) ≤ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
Tactic: refine .mp ?_ (.of_forall fun x hx ↦ lt_of_le_of_lt hx hs)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (β := ℝ) (fun (s : ℕ) ↦ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε
⊢ ∃ (t : ℕ),
    ∀ (x y : ℤ_[p]),
      ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
        ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
          ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
have inl : ∀ (this : Tendsto (β := ℝ) (fun (s : ℕ) ↦ norm.{u_1} (E := C(ℤ_[p], E)) 0 / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0))
  (hs : norm.{u_1} (E := C(ℤ_[p], E)) 0 / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε),
  ∃ (t : ℕ),
    ∀ (x y : ℤ_[p]),
      ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
        ‖HSub.hSub (α := E) (β := E) ((0 : (a : ℤ_[p]) → E) x : E) ((0 : (a : ℤ_[p]) → E) y : E)‖ ≤
          norm.{u_1} (E := C(ℤ_[p], E)) 0 / HPow.hPow (α := ℝ) (↑p : ℝ) s
Tactic: rcases eq_or_ne f 0 with rfl | hf
Cleared hypotheses: f, this, hs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (β := ℝ) (fun (s : ℕ) ↦ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε
inl :
  ∀
    (this :
      Tendsto (β := ℝ) (fun (s : ℕ) ↦ norm.{u_1} (E := C(ℤ_[p], E)) 0 / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0))
    (hs : norm.{u_1} (E := C(ℤ_[p], E)) 0 / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε),
    ∃ (t : ℕ),
      ∀ (x y : ℤ_[p]),
        ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
          ‖HSub.hSub (α := E) (β := E) ((0 : (a : ℤ_[p]) → E) x : E) ((0 : (a : ℤ_[p]) → E) y : E)‖ ≤
            norm.{u_1} (E := C(ℤ_[p], E)) 0 / HPow.hPow (α := ℝ) (↑p : ℝ) s
⊢ ∃ (t : ℕ),
    ∀ (x y : ℤ_[p]),
      ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
        ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
          ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
have inr : ∀ (hf : f ≠ 0),
  ∃ (t : ℕ),
    ∀ (x y : ℤ_[p]),
      ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
        ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
          ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
Tactic: rcases eq_or_ne f 0 with rfl | hf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (β := ℝ) (fun (s : ℕ) ↦ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε
hf : f ≠ 0
⊢ ∃ (t : ℕ),
    ∀ (x y : ℤ_[p]),
      ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
        ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
          ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
have this₁ : 0 < ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
Tactic: have : 0 < ‖f‖ / p ^ s := div_pos (norm_pos_iff.mpr hf) (mod_cast pow_pos hp.out.pos _)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this_1 : Tendsto (β := ℝ) (fun (s : ℕ) ↦ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
⊢ ∃ (t : ℕ),
    ∀ (x y : ℤ_[p]),
      ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
        ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
          ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
have inr : ∀ (δ : ℝ) (hδpos : δ > 0)
  (hδf :
    ∀ {x y : ℤ_[p]},
      dist x y < δ →
        dist (α := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E) <
          ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s),
  ∃ (t : ℕ),
    ∀ (x y : ℤ_[p]),
      ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
        ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
          ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
Tactic: obtain ⟨δ, hδpos, hδf⟩ := f.uniform_continuity _ this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this_1 : Tendsto (β := ℝ) (fun (s : ℕ) ↦ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
δ : ℝ
hδpos : δ > 0
hδf :
  ∀ {x y : ℤ_[p]},
    dist x y < δ →
      dist (α := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E) < ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
⊢ ∃ (t : ℕ),
    ∀ (x y : ℤ_[p]),
      ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
        ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
          ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
have inr : ∀ (t : ℕ) (ht : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) < δ),
  ∃ (t : ℕ),
    ∀ (x y : ℤ_[p]),
      ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
        ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
          ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
Tactic: obtain ⟨t, ht⟩ := PadicInt.exists_pow_neg_lt p hδpos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (β := ℝ) (fun (s : ℕ) ↦ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε
⊢ ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) ≤ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
have obtain : ∀ (t : ℕ)
  (ht :
    ∀ (x y : ℤ_[p]),
      ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
        ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
          ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s),
  ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) ≤ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
Tactic: obtain ⟨t, ht⟩ : ∃ t : ℕ, ∀ x y, ‖x - y‖ ≤ p ^ (-t : ℤ) → ‖f x - f y‖ ≤ ‖f‖ / p ^ s := by
    rcases eq_or_ne f 0 with rfl | hf
    · -- silly case : f = 0
      simp
    have : 0 < ‖f‖ / p ^ s := div_pos (norm_pos_iff.mpr hf) (mod_cast pow_pos hp.out.pos _)
    obtain ⟨δ, hδpos, hδf⟩ := f.uniform_continuity _ this
    obtain ⟨t, ht⟩ := PadicInt.exists_pow_neg_lt p hδpos
    exact ⟨t, fun x y hxy ↦  by simpa only [dist_eq_norm_sub] using (hδf (hxy.trans_lt ht)).le⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (β := ℝ) (fun (s : ℕ) ↦ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε
t : ℕ
ht :
  ∀ (x y : ℤ_[p]),
    ‖x - y‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) →
      ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) x : E) ((f : (a : ℤ_[p]) → E) y : E)‖ ≤
        ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
⊢ ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) ≤ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
have h : ∀ (m : ℕ) (hm : s * p ^ t ≤ m),
  norm (E := E) (Δ_[1]^[m] (⇑f : (a : ℤ_[p]) → E) 0 : E) ≤ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
Tactic: filter_upwards [eventually_ge_atTop (s * p ^ t)] with m hm
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a : E
n : ℕ
⊢ norm (E := C(ℤ_[p], E)) (mahlerTerm a n) = ‖a‖
have a₁ : norm (E := C(ℤ_[p], E)) (mahlerTerm a n) ≤ ‖a‖
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a : E
n : ℕ
a₁ : norm (E := C(ℤ_[p], E)) (mahlerTerm a n) ≤ ‖a‖
⊢ norm (E := C(ℤ_[p], E)) (mahlerTerm a n) = ‖a‖
have a₂ : ‖a‖ ≤ norm (E := C(ℤ_[p], E)) (mahlerTerm a n)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a : E
n : ℕ
⊢ norm (E := C(ℤ_[p], E)) (mahlerTerm a n) ≤ ‖a‖
have a₁ : ∀ (x : ℤ_[p]), norm (E := E) ((mahlerTerm a n : (a : ℤ_[p]) → E) x : E) ≤ ‖a‖
Tactic: rw [ContinuousMap.norm_le_of_nonempty]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a : E
n : ℕ
⊢ ‖a‖ ≤ norm (E := C(ℤ_[p], E)) (mahlerTerm a n)
have a₁ : ‖a‖ ≤ norm (E := E) ((mahlerTerm a n : (a : ℤ_[p]) → E) (↑n : ℤ_[p]) : E)
Tactic: refine le_trans ?_ <| (mahlerTerm a n).norm_coe_le_norm n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := C(ℤ_[p], ℤ_[p])) (mahlerTerm 1 n) (mahler n)
have h : ∀ (a : ℤ_[p]),
  Eq (α := ℤ_[p]) ((mahlerTerm 1 n : (a : ℤ_[p]) → ℤ_[p]) a : ℤ_[p]) ((mahler n : (a : ℤ_[p]) → ℤ_[p]) a : ℤ_[p])
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
⊢ HasSum (α := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (a n) n) (mahlerSeries a)
have refine : Tendsto.{0, u_1} (β := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (a n) n) cofinite (𝓝 0)
Tactic: refine (NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero ?_).hasSum
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
⊢ Tendsto.{0, u_1} (β := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (a n) n) cofinite (𝓝 0)
have rw : ∀ (ha : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖a x‖) atTop (𝓝 0)),
  Tendsto (β := ℝ) (fun (x : ℕ) ↦ norm (E := C(ℤ_[p], E)) (mahlerTerm (a x) x)) cofinite (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
⊢ Eq (α := E) ((mahlerSeries a : (a : ℤ_[p]) → E) (↑m : ℤ_[p]) : E) (∑ i ∈ range (n + 1), m.choose i • a i : E)
have h_van : ∀ (i : ℕ), m.choose (i + (n + 1)) = 0
Tactic: have h_van (i) : m.choose (i + (n + 1)) = 0 := Nat.choose_eq_zero_of_lt (by lia)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
h_van : ∀ (i : ℕ), m.choose (i + (n + 1)) = 0
⊢ Eq (α := E) ((mahlerSeries a : (a : ℤ_[p]) → E) (↑m : ℤ_[p]) : E) (∑ i ∈ range (n + 1), m.choose i • a i : E)
have aux : Summable.{u_1, 0} (α := E) fun (i : ℕ) ↦ m.choose (i + (n + 1)) • a (i + (n + 1))
Tactic: have aux : Summable fun i ↦ m.choose (i + (n + 1)) • a (i + (n + 1)) := by
    simpa only [h_van, zero_smul] using summable_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ Eq (α := E) (Δ_[1]^[n] (⇑(mahlerSeries a) : (a : ℤ_[p]) → E) 0 : E)
    (Δ_[1]^[n] (fun (k : ℕ) ↦ ∑ j ∈ range (n + 1), k.choose j • a j) 0 : E)
have simp : Eq.{u_1 + 1} (α := E)
  (∑ x ∈ range (n + 1),
    HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ))
      ((mahlerSeries a : (a : ℤ_[p]) → E) (HSMul.hSMul (β := ℤ_[p]) x 1) : E))
  (∑ x ∈ range (n + 1),
    HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ))
      (∑ x_1 ∈ range (n + 1), (HSMul.hSMul (β := ℕ) x 1).choose x_1 • a x_1))
Tactic: simp only [fwdDiff_iter_eq_sum_shift, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ Eq.{u_1 + 1} (α := E)
    (∑ x ∈ range (n + 1),
      HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ))
        ((mahlerSeries a : (a : ℤ_[p]) → E) (HSMul.hSMul (β := ℤ_[p]) x 1) : E))
    (∑ x ∈ range (n + 1),
      HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ))
        (∑ x_1 ∈ range (n + 1), (HSMul.hSMul (β := ℕ) x 1).choose x_1 • a x_1))
have refine : ∀ (j : ℕ) (hj : j ∈ range (n + 1)),
  HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ))
      ((mahlerSeries a : (a : ℤ_[p]) → E) (HSMul.hSMul (β := ℤ_[p]) j 1) : E) =
    HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ))
      (∑ x ∈ range (n + 1), (HSMul.hSMul (β := ℕ) j 1).choose x • a x)
Tactic: refine Finset.sum_congr rfl fun j hj ↦ ?_