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 : ℕ
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)) :
      ℝ)
⊢ ‖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)
have 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
Tactic: refine (norm_add_le_max _ _).trans (max_le_max ?_ ?_)
-- 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 : ℕ
⊢ 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)) :
      ℝ)
have 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)
Tactic: rw [norm_neg, ← coe_nnnorm, coe_le_coe]
-- 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 : ℕ
⊢ 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)
have 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)
Tactic: refine nnnorm_sum_le_of_forall_le (fun i hi ↦ Finset.le_sup_of_le hi ?_)
-- 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 : ℕ
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)
have 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)
Tactic: rw [← Nat.cast_smul_eq_nsmul ℤ_[p], div_eq_inv_mul]
-- 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 : ℕ
hi : i ∈ range (p ^ t - 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)
have refine_1 : nnnorm (E := ℤ_[p]) (↑((p ^ t).choose (i + 1)) : ℤ_[p]) ≤ (↑p : ℝ≥0)⁻¹
Tactic: refine (nnnorm_smul_le _ _).trans <| mul_le_mul_of_nonneg_right ?_ (by simp only [zero_le])
-- 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)
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)
⊢ nnnorm (E := ℤ_[p]) (↑((p ^ t).choose (i + 1)) : ℤ_[p]) ≤ (↑p : ℝ≥0)⁻¹
have hi₁ : i < p ^ t - 1
Tactic: rw [mem_range] at hi
Cleared hypotheses: hi
-- 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)
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
⊢ nnnorm (E := ℤ_[p]) (↑((p ^ t).choose (i + 1)) : ℤ_[p]) ≤ (↑p : ℝ≥0)⁻¹
have this : 0 < (p ^ t).choose (i + 1)
Tactic: have : 0 < (p ^ t).choose (i + 1) := Nat.choose_pos (by lia)
-- 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 : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ nnnorm (E := ℤ_[p]) (↑((p ^ t).choose (i + 1)) : ℤ_[p]) ≤ (↑p : ℝ≥0)⁻¹
have refine_1 : 1 ≤ padicValNat p ((p ^ t).choose (i + 1))
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]
-- 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 : ℕ
⊢ 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
have 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
Tactic: refine norm_sum_le_of_forall_le_of_nonempty nonempty_range_add_one (fun i _ ↦ ?_)
-- 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)‖ ≤
    ‖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)‖
have 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)‖
Tactic: rw [← Int.cast_smul_eq_zsmul ℤ_[p]]
-- 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)
⊢ 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)‖
have 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)‖
Tactic: norm_cast
-- 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 (α := ℤ_[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)‖
have apply : ‖HPow.hPow (α := ℤ_[p]) (↑(-1) : ℤ_[p]) (n - i) * (↑(n.choose i) : ℤ_[p])‖ ≤ 1
Tactic: apply mul_le_of_le_one_left (norm_nonneg _)
-- 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)
⊢ ‖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 a : ‖HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p]) - (↑i : ℤ_[p])‖ ≤
  HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
Tactic: apply hst
-- 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)
⊢ ‖HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p]) - (↑i : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
have a : ‖(↑i : ℤ_[p]) + HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) t - (↑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]
-- 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)
a :
  ‖(↑i : ℤ_[p]) + HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) t - (↑i : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
⊢ ‖HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p]) - (↑i : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
have a₁ : ‖HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) t‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
Tactic: 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)
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 : ℤ))
⊢ ‖HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p]) - (↑i : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
have a₂ : norm (E := ℤ_[p]) (↑p : ℤ_[p]) ^ t ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
Tactic: 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)
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 : ℤ))
⊢ ‖HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p]) - (↑i : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
have a₃ : HPow.hPow (α := ℝ) (↑p : ℝ)⁻¹ t ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
Tactic: 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)
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 : ℤ))
⊢ ‖HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p]) - (↑i : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
have a₄ : (HPow.hPow (α := ℝ) (↑p : ℝ) t)⁻¹ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
Tactic: 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)
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 : ℤ))
⊢ ‖HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p]) - (↑i : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
have a₅ : (HPow.hPow (α := ℝ) (↑p : ℝ) t)⁻¹ ≤ (HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (↑t : ℤ))⁻¹
Tactic: 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)
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 : ℤ))⁻¹
⊢ ‖HAdd.hAdd (α := ℤ_[p]) (↑i : ℤ_[p]) (↑(p ^ t) : ℤ_[p]) - (↑i : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑t : ℤ))
have a₆ : (HPow.hPow (α := ℝ) (↑p : ℝ) t)⁻¹ ≤ (HPow.hPow (α := ℝ) (↑p : ℝ) t)⁻¹
Tactic: rw [Nat.cast_pow, add_sub_cancel_left, norm_pow, norm_p, inv_pow, zpow_neg, zpow_natCast]