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 : ℕ
rw :
  ‖HAdd.hAdd (α := E)
        (-∑ j ∈ range (p ^ t - 1),
            HSMul.hSMul (β := E) ((p ^ t).choose (j + 1)) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E))
        (∑ k ∈ range (n + 1),
          (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) •
            HSub.hSub (α := E) (β := E)
              ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑k : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
              ((f : (a : ℤ_[p]) → E) (↑k : ℤ_[p]) : E))‖ ≤
    max
      (↑((range (p ^ t - 1)).sup fun (j : ℕ) ↦
            nnnorm (E := E) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E) / (↑p : ℝ≥0)) :
        ℝ)
      (‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s)
⊢ norm (E := E) (Δ_[1]^[n + p ^ t] (⇑f : (a : ℤ_[p]) → E) 0 : E) ≤
    max
      (↑((range (p ^ t - 1)).sup fun (j : ℕ) ↦
            nnnorm (E := E) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E) / (↑p : ℝ≥0)) :
        ℝ)
      (‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s)

Tactic:
rw [bojanic_mahler_step1 _ _ (one_le_pow₀ hp.out.one_le)]

Premises used: one_le_pow₀, _private.0.bojanic_mahler_step1, Nat.Prime.one_le, Fact.out
-- 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 : ℕ
⊢ ‖HAdd.hAdd (α := E)
        (-∑ j ∈ range (p ^ t - 1),
            HSMul.hSMul (β := E) ((p ^ t).choose (j + 1)) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E))
        (∑ k ∈ range (n + 1),
          (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) •
            HSub.hSub (α := E) (β := E)
              ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑k : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
              ((f : (a : ℤ_[p]) → E) (↑k : ℤ_[p]) : E))‖ ≤
    max
      (↑((range (p ^ t - 1)).sup fun (j : ℕ) ↦
            nnnorm (E := E) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E) / (↑p : ℝ≥0)) :
        ℝ)
      (‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s)

Tactic:
(norm_add_le_max _ _).trans (max_le_max ?_ ?_)

Premises used: IsUltrametricDist.norm_add_le_max, max_le_max, LE.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
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 : ℕ
refine_1 :
  norm.{u_1} (E := E)
      (-∑ j ∈ range (p ^ t - 1),
          HSMul.hSMul (β := E) ((p ^ t).choose (j + 1)) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)) ≤
    (↑((range (p ^ t - 1)).sup fun (j : ℕ) ↦
          nnnorm (E := E) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E) / (↑p : ℝ≥0)) :
      ℝ)
refine_2 :
  norm.{u_1} (E := E)
      (∑ k ∈ range (n + 1),
        (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) •
          HSub.hSub (α := E) (β := E)
            ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑k : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
            ((f : (a : ℤ_[p]) → E) (↑k : ℤ_[p]) : E)) ≤
    ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s
⊢ ‖HAdd.hAdd (α := E)
        (-∑ j ∈ range (p ^ t - 1),
            HSMul.hSMul (β := E) ((p ^ t).choose (j + 1)) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E))
        (∑ k ∈ range (n + 1),
          (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) •
            HSub.hSub (α := E) (β := E)
              ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑k : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
              ((f : (a : ℤ_[p]) → E) (↑k : ℤ_[p]) : E))‖ ≤
    max
      (↑((range (p ^ t - 1)).sup fun (j : ℕ) ↦
            nnnorm (E := E) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E) / (↑p : ℝ≥0)) :
        ℝ)
      (‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s)

Tactic:
refine (norm_add_le_max _ _).trans (max_le_max ?_ ?_)

Premises used: IsUltrametricDist.norm_add_le_max, max_le_max, LE.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
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 : ℕ
refine_1 :
  nnnorm.{u_1} (E := E)
      (∑ j ∈ range (p ^ t - 1),
        HSMul.hSMul (β := E) ((p ^ t).choose (j + 1)) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)) ≤
    (range (p ^ t - 1)).sup fun (j : ℕ) ↦
      nnnorm (E := E) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E) / (↑p : ℝ≥0)
⊢ norm.{u_1} (E := E)
      (-∑ j ∈ range (p ^ t - 1),
          HSMul.hSMul (β := E) ((p ^ t).choose (j + 1)) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)) ≤
    (↑((range (p ^ t - 1)).sup fun (j : ℕ) ↦
          nnnorm (E := E) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E) / (↑p : ℝ≥0)) :
      ℝ)

Tactic:
rw [norm_neg, ← coe_nnnorm, coe_le_coe]

Premises used: coe_nnnorm, norm_neg, NNReal.coe_le_coe
-- 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 : ℕ
⊢ nnnorm.{u_1} (E := E)
      (∑ j ∈ range (p ^ t - 1),
        HSMul.hSMul (β := E) ((p ^ t).choose (j + 1)) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)) ≤
    (range (p ^ t - 1)).sup fun (j : ℕ) ↦
      nnnorm (E := E) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E) / (↑p : ℝ≥0)

Tactic:
nnnorm_sum_le_of_forall_le (fun i hi ↦ Finset.le_sup_of_le hi ?_)

Premises used: IsUltrametricDist.nnnorm_sum_le_of_forall_le, Finset.le_sup_of_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)
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 : ℕ
refine_1 :
  ∀ (i : ℕ) (hi : i ∈ range (p ^ t - 1)),
    ‖HSMul.hSMul (β := E) ((p ^ t).choose (i + 1)) (Δ_[1]^[n + (i + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)‖₊ ≤
      nnnorm (E := E) (Δ_[1]^[n + (i + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E) / (↑p : ℝ≥0)
⊢ nnnorm.{u_1} (E := E)
      (∑ j ∈ range (p ^ t - 1),
        HSMul.hSMul (β := E) ((p ^ t).choose (j + 1)) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)) ≤
    (range (p ^ t - 1)).sup fun (j : ℕ) ↦
      nnnorm (E := E) (Δ_[1]^[n + (j + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E) / (↑p : ℝ≥0)

Tactic:
refine nnnorm_sum_le_of_forall_le (fun i hi ↦ Finset.le_sup_of_le hi ?_)

Premises used: IsUltrametricDist.nnnorm_sum_le_of_forall_le, Finset.le_sup_of_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)
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 : ℕ
hi : i ∈ range (p ^ t - 1)
refine_1 :
  ‖HSMul.hSMul (α := ℤ_[p]) (β := E) (↑((p ^ t).choose (i + 1)) : ℤ_[p])
        (Δ_[1]^[n + (i + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)‖₊ ≤
    (↑p : ℝ≥0)⁻¹ * nnnorm (E := E) (Δ_[1]^[n + (i + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)
⊢ ‖HSMul.hSMul (β := E) ((p ^ t).choose (i + 1)) (Δ_[1]^[n + (i + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)‖₊ ≤
    nnnorm (E := E) (Δ_[1]^[n + (i + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E) / (↑p : ℝ≥0)

Tactic:
rw [← Nat.cast_smul_eq_nsmul ℤ_[p], div_eq_inv_mul]

Premises used: PadicInt, Nat.cast_smul_eq_nsmul, div_eq_inv_mul
-- 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 : ℕ
hi : i ∈ range (p ^ t - 1)
⊢ 0 ≤ nnnorm (E := E) (Δ_[1]^[n + (i + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)

Tactic:
simp only [zero_le]

Premises used: zero_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)
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 : ℕ
hi : i ∈ range (p ^ t - 1)
refine_1 : nnnorm (E := ℤ_[p]) (↑((p ^ t).choose (i + 1)) : ℤ_[p]) ≤ (↑p : ℝ≥0)⁻¹
⊢ ‖HSMul.hSMul (α := ℤ_[p]) (β := E) (↑((p ^ t).choose (i + 1)) : ℤ_[p])
        (Δ_[1]^[n + (i + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)‖₊ ≤
    (↑p : ℝ≥0)⁻¹ * nnnorm (E := E) (Δ_[1]^[n + (i + 1)] (⇑f : (a : ℤ_[p]) → E) 0 : E)

Tactic:
refine (nnnorm_smul_le _ _).trans <| mul_le_mul_of_nonneg_right ?_ (by simp only [zero_le])

Premises used: mul_le_mul_of_nonneg_right, nnnorm_smul_le, LE.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
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 : ℕ
hi : i ∈ range (p ^ t - 1)
⊢ i < p ^ t - 1

Tactic:
rw [mem_range] at hi

Premises used: Finset.mem_range
-- 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 : ℕ
hi : i < p ^ t - 1
⊢ i + 1 ≤ p ^ t

Tactic:
lia
-- 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 : ℕ
hi : i < p ^ t - 1
⊢ 0 < (p ^ t).choose (i + 1)

Tactic:
have : 0 < (p ^ t).choose (i + 1) := Nat.choose_pos (by lia)
-- 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 : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
refine_1 : 1 ≤ padicValNat p ((p ^ t).choose (i + 1))
⊢ nnnorm (E := ℤ_[p]) (↑((p ^ t).choose (i + 1)) : ℤ_[p]) ≤ (↑p : ℝ≥0)⁻¹

Tactic:
rw [← zpow_neg_one, ← coe_le_coe, coe_nnnorm, PadicInt.norm_eq_zpow_neg_valuation
      (mod_cast this.ne'), coe_zpow, NNReal.coe_natCast,
      zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt), neg_le_neg_iff,
      ← PadicInt.valuation_coe, PadicInt.coe_natCast, Padic.valuation_natCast, Nat.one_le_cast]

Premises used: zpow_neg_one, PadicInt.norm_eq_zpow_neg_valuation, Nat.one_le_cast, zpow_le_zpow_iff_right₀, PadicInt.coe_natCast, NNReal.coe_natCast, coe_nnnorm, PadicInt.valuation_coe, Padic.valuation_natCast, NNReal.coe_zpow, NNReal.coe_le_coe, neg_le_neg_iff
-- 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 : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ i + 1 ≠ 0

Tactic:
lia
-- 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 : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ i + 1 ≠ p ^ t

Tactic:
lia
-- 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 : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ 1 ≤ padicValNat p ((p ^ t).choose (i + 1))

Tactic:
exact one_le_padicValNat_of_dvd this.ne' <| hp.out.dvd_choose_pow (by lia) (by lia)

Premises used: Nat.Prime.dvd_choose_pow, one_le_padicValNat_of_dvd, LT.lt.ne', Fact.out
-- 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 : ℕ
⊢ norm.{u_1} (E := E)
      (∑ k ∈ range (n + 1),
        (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) •
          HSub.hSub (α := E) (β := E)
            ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑k : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
            ((f : (a : ℤ_[p]) → E) (↑k : ℤ_[p]) : E)) ≤
    ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s

Tactic:
norm_sum_le_of_forall_le_of_nonempty nonempty_range_add_one (fun i _ ↦ ?_)

Premises used: Finset.nonempty_range_add_one, IsUltrametricDist.norm_sum_le_of_forall_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
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 : ℕ
refine_2 :
  ∀ 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
⊢ norm.{u_1} (E := E)
      (∑ k ∈ range (n + 1),
        (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) •
          HSub.hSub (α := E) (β := E)
            ((f : (a : ℤ_[p]) → E) (HAdd.hAdd (α := ℤ_[p]) (↑k : ℤ_[p]) (↑(p ^ t) : ℤ_[p])) : E)
            ((f : (a : ℤ_[p]) → E) (↑k : ℤ_[p]) : E)) ≤
    ‖f‖ / HPow.hPow (α := ℝ) (↑p : ℝ) s

Tactic:
refine norm_sum_le_of_forall_le_of_nonempty nonempty_range_add_one (fun i _ ↦ ?_)

Premises used: Finset.nonempty_range_add_one, IsUltrametricDist.norm_sum_le_of_forall_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
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)
rw :
  ‖HSMul.hSMul (α := ℤ_[p]) (↑(HPow.hPow (α := ℤ) (-1) (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 (α := ℤ_[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)‖ ≤
    ‖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:
rw [← Int.cast_smul_eq_zsmul ℤ_[p]]

Premises used: PadicInt, Int.cast_smul_eq_zsmul
-- 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)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  norm (E := ℤ_[p]) (↑(Int.negSucc 0 ^ (n - i) * (↑(n.choose i) : ℤ)) : ℤ_[p]) *
      ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (↑(i + p ^ t) : ℤ_[p]) : E)
          ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖ ≤
    norm (E := ℤ_[p]) (↑(Int.negSucc 0 ^ (n - i) * (↑(n.choose i) : ℤ)) : ℤ_[p]) *
      ‖HSub.hSub (α := E) (β := E) ((f : (a : ℤ_[p]) → E) (↑(i + p ^ t) : ℤ_[p]) : E)
          ((f : (a : ℤ_[p]) → E) (↑i : ℤ_[p]) : E)‖
⊢ norm (E := ℤ_[p]) (↑(HPow.hPow (α := ℤ) (-1) (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 (α := ℤ_[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:
norm_cast
-- 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)
⊢ ‖HSMul.hSMul (α := ℤ_[p]) (↑(HPow.hPow (α := ℤ) (-1) (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 (α := ℤ_[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:
exact (norm_smul_le ..).trans (by norm_cast)

Premises used: norm_smul_le, LE.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
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)
apply : ‖HPow.hPow (α := ℤ_[p]) (↑(-1) : ℤ_[p]) (n - i) * (↑(n.choose i) : ℤ_[p])‖ ≤ 1
⊢ ‖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:
apply mul_le_of_le_one_left (norm_nonneg _)

Premises used: mul_le_of_le_one_left, 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
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 (α := ℤ_[p]) (↑(-1) : ℤ_[p]) (n - i) * (↑(n.choose i) : ℤ_[p])‖ ≤ 1

Tactic:
simpa only [← coe_intCast] using norm_le_one _

Premises used: PadicInt.norm_le_one, PadicInt.coe_intCast