awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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)
a :
  ‖HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p]) - (↑i : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
⊢ ‖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:
apply hst
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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)
a :
  ‖(↑i : ℤ_[p]) + HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) t - (↑i : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
a₁ : ‖HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) t‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
a₂ : norm (E := ℤ_[p]) (↑p : ℤ_[p]) ^ t ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
a₃ : HPow.hPow (α := ℝ) (↑p : ℝ)⁻¹ t ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
a₄ : (HPow.hPow (α := ℝ) (↑p : ℝ) t)⁻¹ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
a₅ : (HPow.hPow (α := ℝ) (↑p : ℝ) t)⁻¹ ≤ (HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (↑t : ℤ))⁻¹
a₆ a₇ : (HPow.hPow (α := ℝ) (↑p : ℝ) t)⁻¹ ≤ (HPow.hPow (α := ℝ) (↑p : ℝ) t)⁻¹
⊢ ‖HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p]) - (↑i : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))

Tactic:
rw [Nat.cast_pow, add_sub_cancel_left, norm_pow, norm_p, inv_pow, zpow_neg, zpow_natCast]

Premises used: zpow_natCast, norm_pow, add_sub_cancel_left, inv_pow, zpow_neg, PadicInt.norm_p, Nat.cast_pow
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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)‖
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
⊢ ‖(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

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]

Premises used: Int.cast, Nat.choose, HMul.hMul, HSub.hSub, Nat.cast, HPow.hPow, HAdd.hAdd, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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)

Tactic:
NormedAddGroup.tendsto_nhds_zero.mpr (fun ε hε ↦ ?_)

Premises used: Iff.mpr, NormedAddGroup.tendsto_nhds_zero
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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)
refine : ∀ (ε : ℝ) (hε : ε > 0), ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) < ε
⊢ Tendsto.{0, u_1} (β := E) (fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0) atTop (𝓝 0)

Tactic:
refine NormedAddGroup.tendsto_nhds_zero.mpr (fun ε hε ↦ ?_)

Premises used: Iff.mpr, NormedAddGroup.tendsto_nhds_zero
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
⊢ 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))
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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)
obtain :
  ∀ (s : ℕ) (hs : ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s < ε),
    ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) < ε
⊢ ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) < ε

Tactic:
obtain ⟨s, hs⟩ := (this.eventually_lt_const hε).exists

Premises used: Filter.Eventually.exists, Filter.Tendsto.eventually_lt_const
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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) < ε

Tactic:
.mp ?_ (.of_forall fun x hx ↦ lt_of_le_of_lt hx hs)

Premises used: lt_of_le_of_lt, Filter.Eventually.of_forall, Filter.Eventually.mp
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 < ε
refine :
  ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) ≤ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
⊢ ∀ᶠ (x : ℕ) in atTop, norm (E := E) (Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0 : E) < ε

Tactic:
refine .mp ?_ (.of_forall fun x hx ↦ lt_of_le_of_lt hx hs)
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
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
⊢ ∃ (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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
ε : ℝ
hε : ε > 0
s : ℕ
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:
simp
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
⊢ 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 _)
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
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
⊢ ∃ (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

Premises used: ContinuousMap.uniform_continuity
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
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
⊢ ∃ (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

Premises used: PadicInt.exists_pow_neg_lt
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 : ℕ
ht : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ)) < δ
x y : ℤ_[p]
hxy : ‖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:
simpa only [dist_eq_norm_sub] using (hδf (hxy.trans_lt ht)).le

Premises used: dist_eq_norm_sub, LT.lt.le, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 : ℕ
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:
exact ⟨t, fun x y hxy ↦  by simpa only [dist_eq_norm_sub] using (hδf (hxy.trans_lt ht)).le⟩
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 < ε
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
⊢ ∀ᶠ (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⟩
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
h :
  ∀ (m : ℕ) (hm : s * p ^ t ≤ m),
    norm (E := E) (Δ_[1]^[m] (⇑f : (a : ℤ_[p]) → E) 0 : 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:
filter_upwards [eventually_ge_atTop (s * p ^ t)] with m hm

Premises used: HMul.hMul, HPow.hPow, Filter.eventually_ge_atTop
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
m : ℕ
hm : s * p ^ t ≤ m
⊢ norm (E := E) (Δ_[1]^[m] (⇑f : (a : ℤ_[p]) → E) 0 : E) ≤ ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s

Tactic:
simpa only [Nat.sub_add_cancel hm] using fwdDiff_iter_le_of_forall_le ht (m - s * p ^ t)

Premises used: HMul.hMul, HSub.hSub, PadicInt.fwdDiff_iter_le_of_forall_le, Nat.sub_add_cancel, HPow.hPow
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 : ℕ
x : ℤ_[p]
⊢ (mahlerTerm a n : (a : ℤ_[p]) → E) x = HSMul.hSMul (α := ℤ_[p]) ((mahler n : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p]) a

Tactic:
simp only [mahlerTerm, ContinuousMap.smul_apply', ContinuousMap.const_apply]

Premises used: ContinuousMap.smul_apply', ContinuousMap.const_apply, PadicInt.mahlerTerm
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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‖
a₂ : ‖a‖ ≤ norm (E := C(ℤ_[p], E)) (mahlerTerm a n)
⊢ norm (E := C(ℤ_[p], E)) (mahlerTerm a n) = ‖a‖

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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₁ : ∀ (x : ℤ_[p]), norm (E := E) ((mahlerTerm a n : (a : ℤ_[p]) → E) x : E) ≤ ‖a‖
⊢ norm (E := C(ℤ_[p], E)) (mahlerTerm a n) ≤ ‖a‖

Tactic:
rw [ContinuousMap.norm_le_of_nonempty]

Premises used: ContinuousMap.norm_le_of_nonempty
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 : ℕ
⊢ ∀ (x : ℤ_[p]), norm (E := E) ((mahlerTerm a n : (a : ℤ_[p]) → E) x : E) ≤ ‖a‖

Tactic:
fun _ ↦ (norm_smul_le _ _).trans <| mul_le_of_le_one_left (norm_nonneg _) (norm_le_one _)

Premises used: norm_smul_le, PadicInt, mahler, mul_le_of_le_one_left, ContinuousMap.const, LE.le.trans, PadicInt.norm_le_one, DFunLike.coe, norm_nonneg
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 : ℕ
⊢ ∀ (x : ℤ_[p]), norm (E := E) ((mahlerTerm a n : (a : ℤ_[p]) → E) x : E) ≤ ‖a‖

Tactic:
refine fun _ ↦ (norm_smul_le _ _).trans <| mul_le_of_le_one_left (norm_nonneg _) (norm_le_one _)

Premises used: norm_smul_le, mul_le_of_le_one_left, LE.le.trans, PadicInt.norm_le_one, norm_nonneg
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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)

Tactic:
le_trans ?_ <| (mahlerTerm a n).norm_coe_le_norm n

Premises used: ContinuousMap.norm_coe_le_norm, Nat.cast, PadicInt.mahlerTerm, le_trans
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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₁ : ‖a‖ ≤ norm (E := E) ((mahlerTerm a n : (a : ℤ_[p]) → E) (↑n : ℤ_[p]) : E)
⊢ ‖a‖ ≤ norm (E := C(ℤ_[p], E)) (mahlerTerm a n)

Tactic:
refine le_trans ?_ <| (mahlerTerm a n).norm_coe_le_norm n

Premises used: ContinuousMap.norm_coe_le_norm, Nat.cast, PadicInt.mahlerTerm, le_trans
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 := E) ((mahlerTerm a n : (a : ℤ_[p]) → E) (↑n : ℤ_[p]) : E)

Tactic:
simp [mahlerTerm_apply, mahler_natCast_eq]

Premises used: PadicInt.mahlerTerm_apply, mahler_natCast_eq
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h :
  ∀ (a : ℤ_[p]),
    Eq (α := ℤ_[p]) ((mahlerTerm 1 n : (a : ℤ_[p]) → ℤ_[p]) a : ℤ_[p]) ((mahler n : (a : ℤ_[p]) → ℤ_[p]) a : ℤ_[p])
⊢ Eq (α := C(ℤ_[p], ℤ_[p])) (mahlerTerm 1 n) (mahler n)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ_[p]
⊢ Eq (α := ℤ_[p]) ((mahlerTerm 1 n : (a : ℤ_[p]) → ℤ_[p]) a : ℤ_[p]) ((mahler n : (a : ℤ_[p]) → ℤ_[p]) a : ℤ_[p])

Tactic:
simp [mahlerTerm_apply]

Premises used: PadicInt.mahlerTerm_apply
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ norm (E := C(ℤ_[p], ℤ_[p])) (mahler k) = 1

Tactic:
simp [← mahlerTerm_one]

Premises used: PadicInt.mahlerTerm_one
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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)

Tactic:
(NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero ?_).hasSum

Premises used: PadicInt.mahlerSeries, Summable.hasSum, NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero