awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : (x : ℤ_[p]) → ℤ_[p] := fun (x : ℤ_[p]) ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : Ne (α := ℤ_[p]) (↑k.factorial : ℤ_[p]) 0
hf : ContinuousAt f x
δ : ℝ
hδp : δ > 0
hδ : ∀ ⦃x_1 : ℤ_[p]⦄, dist x_1 x < δ → dist (f x_1) (f x) < norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
⊢ ∃ (n : ℕ), ‖f x - f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
have obtain : ∀ (n : ℕ) (hn' : dist x (↑n : ℤ_[p]) < δ), ∃ (n : ℕ), ‖f x - f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
Tactic: obtain ⟨n, hn'⟩ := PadicInt.denseRange_natCast.exists_dist_lt x hδp
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : (x : ℤ_[p]) → ℤ_[p] := fun (x : ℤ_[p]) ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : Ne (α := ℤ_[p]) (↑k.factorial : ℤ_[p]) 0
hf : ContinuousAt f x
⊢ ‖f x‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
have obtain : ∀ (n : ℕ) (hn : ‖f x - f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])),
  ‖f x‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
Tactic: obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖f x - f n‖ ≤ ‖(k.factorial : ℤ_[p])‖ := by
    obtain ⟨δ, hδp, hδ⟩ := Metric.continuousAt_iff.mp hf _ (norm_pos_iff.mpr hC)
    obtain ⟨n, hn'⟩ := PadicInt.denseRange_natCast.exists_dist_lt x hδp
    simpa only [← dist_eq_norm_sub'] using ⟨n, (hδ (dist_comm x n ▸ hn')).le⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : (x : ℤ_[p]) → ℤ_[p] := fun (x : ℤ_[p]) ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : Ne (α := ℤ_[p]) (↑k.factorial : ℤ_[p]) 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
⊢ ‖f x‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
have refine : ‖f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
Tactic: refine sub_add_cancel (f x) _ ▸ (IsUltrametricDist.norm_add_le_max _ (f n)).trans (max_le hn ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : (x : ℤ_[p]) → ℤ_[p] := fun (x : ℤ_[p]) ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : Ne (α := ℤ_[p]) (↑k.factorial : ℤ_[p]) 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
⊢ ‖f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
have simp_rw : norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p]) * norm (E := ℤ_[p]) (↑(Ring.multichoose n k) : ℤ_[p]) ≤
  norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
Tactic: simp_rw [f, ← ascPochhammer_eval_cast, Polynomial.eval_eq_smeval,
    ← Ring.factorial_nsmul_multichoose_eq_ascPochhammer, smul_eq_mul, Nat.cast_mul, norm_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ ‖(↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])‖ ≤ 1
have rw : ‖(↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p])‖ ≤ norm (E := ℚ_[p]) (↑k.factorial : ℚ_[p])
Tactic: rw [norm_div, div_le_one (by simpa using k.factorial_ne_zero)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ HSMul.hSMul (β := ℤ_[p]) k.factorial
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
        ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) =
    Polynomial.smeval (ascPochhammer ℕ k) x
have rw : (↑(HSMul.hSMul (β := ℤ_[p]) k.factorial
        (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
          ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) sorry)) :
    ℚ_[p]) =
  (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
Tactic: rw [← Subtype.coe_inj, nsmul_eq_mul, PadicInt.coe_mul,
    PadicInt.coe_natCast, mul_div_cancel₀ _ (mod_cast k.factorial_ne_zero), Subtype.coe_inj,
    Polynomial.eval_eq_smeval, Polynomial.ascPochhammer_smeval_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
rw :
  (↑(HSMul.hSMul (β := ℤ_[p]) k.factorial
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
⊢ HSMul.hSMul (β := ℤ_[p]) k.factorial
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
        ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) =
    Polynomial.smeval (ascPochhammer ℕ k) x
have rw₁ : (↑(HMul.hMul (α := ℤ_[p]) (↑k.factorial : ℤ_[p])
        (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
          ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) sorry)) :
    ℚ_[p]) =
  (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
Tactic: rw [← Subtype.coe_inj, nsmul_eq_mul, PadicInt.coe_mul,
    PadicInt.coe_natCast, mul_div_cancel₀ _ (mod_cast k.factorial_ne_zero), Subtype.coe_inj,
    Polynomial.eval_eq_smeval, Polynomial.ascPochhammer_smeval_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
rw :
  (↑(HSMul.hSMul (β := ℤ_[p]) k.factorial
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₁ :
  (↑(HMul.hMul (α := ℤ_[p]) (↑k.factorial : ℤ_[p])
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
⊢ HSMul.hSMul (β := ℤ_[p]) k.factorial
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
        ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) =
    Polynomial.smeval (ascPochhammer ℕ k) x
have rw₂ : (↑(↑k.factorial : ℤ_[p]) : ℚ_[p]) *
    (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
          ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) sorry) :
      ℚ_[p]) =
  (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
Tactic: rw [← Subtype.coe_inj, nsmul_eq_mul, PadicInt.coe_mul,
    PadicInt.coe_natCast, mul_div_cancel₀ _ (mod_cast k.factorial_ne_zero), Subtype.coe_inj,
    Polynomial.eval_eq_smeval, Polynomial.ascPochhammer_smeval_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
rw :
  (↑(HSMul.hSMul (β := ℤ_[p]) k.factorial
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₁ :
  (↑(HMul.hMul (α := ℤ_[p]) (↑k.factorial : ℤ_[p])
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₂ :
  (↑(↑k.factorial : ℤ_[p]) : ℚ_[p]) *
      (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) :
        ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
⊢ HSMul.hSMul (β := ℤ_[p]) k.factorial
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
        ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) =
    Polynomial.smeval (ascPochhammer ℕ k) x
have rw₃ : (↑k.factorial : ℚ_[p]) *
    (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
          ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) sorry) :
      ℚ_[p]) =
  (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
Tactic: rw [← Subtype.coe_inj, nsmul_eq_mul, PadicInt.coe_mul,
    PadicInt.coe_natCast, mul_div_cancel₀ _ (mod_cast k.factorial_ne_zero), Subtype.coe_inj,
    Polynomial.eval_eq_smeval, Polynomial.ascPochhammer_smeval_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
rw :
  (↑(HSMul.hSMul (β := ℤ_[p]) k.factorial
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₁ :
  (↑(HMul.hMul (α := ℤ_[p]) (↑k.factorial : ℤ_[p])
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₂ :
  (↑(↑k.factorial : ℤ_[p]) : ℚ_[p]) *
      (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) :
        ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₃ :
  (↑k.factorial : ℚ_[p]) *
      (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) :
        ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
⊢ HSMul.hSMul (β := ℤ_[p]) k.factorial
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
        ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) =
    Polynomial.smeval (ascPochhammer ℕ k) x
have rw₄ : (↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) = (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
Tactic: rw [← Subtype.coe_inj, nsmul_eq_mul, PadicInt.coe_mul,
    PadicInt.coe_natCast, mul_div_cancel₀ _ (mod_cast k.factorial_ne_zero), Subtype.coe_inj,
    Polynomial.eval_eq_smeval, Polynomial.ascPochhammer_smeval_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
rw :
  (↑(HSMul.hSMul (β := ℤ_[p]) k.factorial
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₁ :
  (↑(HMul.hMul (α := ℤ_[p]) (↑k.factorial : ℤ_[p])
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₂ :
  (↑(↑k.factorial : ℤ_[p]) : ℚ_[p]) *
      (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) :
        ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₃ :
  (↑k.factorial : ℚ_[p]) *
      (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) :
        ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₄ : (↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) = (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
⊢ HSMul.hSMul (β := ℤ_[p]) k.factorial
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
        ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) =
    Polynomial.smeval (ascPochhammer ℕ k) x
have rw₅ : Polynomial.eval x (ascPochhammer ℤ_[p] k) = Polynomial.smeval (ascPochhammer ℕ k) x
Tactic: rw [← Subtype.coe_inj, nsmul_eq_mul, PadicInt.coe_mul,
    PadicInt.coe_natCast, mul_div_cancel₀ _ (mod_cast k.factorial_ne_zero), Subtype.coe_inj,
    Polynomial.eval_eq_smeval, Polynomial.ascPochhammer_smeval_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
rw :
  (↑(HSMul.hSMul (β := ℤ_[p]) k.factorial
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₁ :
  (↑(HMul.hMul (α := ℤ_[p]) (↑k.factorial : ℤ_[p])
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₂ :
  (↑(↑k.factorial : ℤ_[p]) : ℚ_[p]) *
      (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) :
        ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₃ :
  (↑k.factorial : ℚ_[p]) *
      (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) :
        ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₄ : (↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) = (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₅ : Polynomial.eval x (ascPochhammer ℤ_[p] k) = Polynomial.smeval (ascPochhammer ℕ k) x
⊢ HSMul.hSMul (β := ℤ_[p]) k.factorial
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
        ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) =
    Polynomial.smeval (ascPochhammer ℕ k) x
have rw₆ : Polynomial.smeval (R := ℤ_[p]) (ascPochhammer ℤ_[p] k) x = Polynomial.smeval (ascPochhammer ℕ k) x
Tactic: rw [← Subtype.coe_inj, nsmul_eq_mul, PadicInt.coe_mul,
    PadicInt.coe_natCast, mul_div_cancel₀ _ (mod_cast k.factorial_ne_zero), Subtype.coe_inj,
    Polynomial.eval_eq_smeval, Polynomial.ascPochhammer_smeval_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
rw :
  (↑(HSMul.hSMul (β := ℤ_[p]) k.factorial
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₁ :
  (↑(HMul.hMul (α := ℤ_[p]) (↑k.factorial : ℤ_[p])
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯)) :
      ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₂ :
  (↑(↑k.factorial : ℤ_[p]) : ℚ_[p]) *
      (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) :
        ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₃ :
  (↑k.factorial : ℚ_[p]) *
      (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
            ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) :
        ℚ_[p]) =
    (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₄ : (↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) = (↑(Polynomial.smeval (ascPochhammer ℕ k) x) : ℚ_[p])
rw₅ : Polynomial.eval x (ascPochhammer ℤ_[p] k) = Polynomial.smeval (ascPochhammer ℕ k) x
rw₆ : Polynomial.smeval (R := ℤ_[p]) (ascPochhammer ℤ_[p] k) x = Polynomial.smeval (ascPochhammer ℕ k) x
⊢ HSMul.hSMul (β := ℤ_[p]) k.factorial
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
        ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯) =
    Polynomial.smeval (ascPochhammer ℕ k) x
have rw₇ : Polynomial.smeval (ascPochhammer ℕ k) x = Polynomial.smeval (ascPochhammer ℕ k) x
Tactic: rw [← Subtype.coe_inj, nsmul_eq_mul, PadicInt.coe_mul,
    PadicInt.coe_natCast, mul_div_cancel₀ _ (mod_cast k.factorial_ne_zero), Subtype.coe_inj,
    Polynomial.eval_eq_smeval, Polynomial.ascPochhammer_smeval_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
M : Type u_1
G : Type u_2
inst : TopologicalSpace M
inst_1 : CompactSpace M
inst_2 : AddCommMonoid M
inst_3 : SeminormedAddCommGroup G
inst_4 : IsUltrametricDist G
h : M
f : C(M, G)
m : M
n : ℕ
⊢ norm.{u_2} (E := G) (Δ_[h]^[n] (⇑f : (a : M) → G) m : G) ≤ ‖f‖
have rw : norm.{u_2} (E := G)
    (∑ k ∈ range (n + 1),
      HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ))
        ((f : (a : M) → G) (m + k • h) : G)) ≤
  ‖f‖
Tactic: rw [fwdDiff_iter_eq_sum_shift]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
M : Type u_1
G : Type u_2
inst : TopologicalSpace M
inst_1 : CompactSpace M
inst_2 : AddCommMonoid M
inst_3 : SeminormedAddCommGroup G
inst_4 : IsUltrametricDist G
h : M
f : C(M, G)
m : M
n : ℕ
⊢ norm.{u_2} (E := G)
      (∑ k ∈ range (n + 1),
        HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ))
          ((f : (a : M) → G) (m + k • h) : G)) ≤
    ‖f‖
have refine : ∀ i ∈ range (n + 1),
  ‖HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) (n - i) * (↑(n.choose i) : ℤ)) ((f : (a : M) → G) (m + i • h) : G)‖ ≤
    ‖f‖
Tactic: refine norm_sum_le_of_forall_le_of_nonneg (norm_nonneg f) fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoidWithOne M
inst_1 : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
⊢ Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
have rw : Δ_[1]^[n + R] f 0 = R.choose R • Δ_[1]^[n + R] f 0
Tactic: rw [Nat.sub_add_cancel hR, Nat.choose_self, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoidWithOne M
inst_1 : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
rw : Δ_[1]^[n + R] f 0 = R.choose R • Δ_[1]^[n + R] f 0
⊢ Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
have rw₁ : Δ_[1]^[n + R] f 0 = HSMul.hSMul (α := ℕ) 1 (Δ_[1]^[n + R] f 0)
Tactic: rw [Nat.sub_add_cancel hR, Nat.choose_self, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoidWithOne M
inst_1 : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
rw : Δ_[1]^[n + R] f 0 = R.choose R • Δ_[1]^[n + R] f 0
rw₁ : Δ_[1]^[n + R] f 0 = HSMul.hSMul (α := ℕ) 1 (Δ_[1]^[n + R] f 0)
⊢ Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
have rw₂ : Δ_[1]^[n + R] f 0 = Δ_[1]^[n + R] f 0
Tactic: rw [Nat.sub_add_cancel hR, Nat.choose_self, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (hypothesis)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoidWithOne M
inst_1 : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
⊢ Δ_[1]^[n + R] f 0 =
    HAdd.hAdd (α := G) (-∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0)
      (∑ k ∈ range (n + 1),
        (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) •
          (f (HAdd.hAdd (α := M) (↑k : M) (↑R : M)) - f (↑k : M)))
have aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
Tactic: have aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0 := by
    rw [Nat.sub_add_cancel hR, Nat.choose_self, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoidWithOne M
inst_1 : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ Δ_[1]^[n + R] f 0 =
    HAdd.hAdd (α := G) (-∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0)
      (∑ k ∈ range (n + 1),
        (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) •
          (f (HAdd.hAdd (α := M) (↑k : M) (↑R : M)) - f (↑k : M)))
have rw : ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 - Δ_[1]^[n] f 0 =
  ∑ k ∈ range (n + 1),
    (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • (f (HAdd.hAdd (α := M) (↑k : M) (↑R : M)) - f (↑k : M))
Tactic: rw [neg_add_eq_sub, eq_sub_iff_add_eq, add_comm, aux, (by lia : n + R = (n + ((R - 1) + 1))),
    ← sum_range_succ, Nat.sub_add_cancel hR,
    ← sub_eq_iff_eq_add.mpr (sum_range_succ' (fun x ↦ R.choose x • Δ_[1]^[n + x] f 0) R), add_zero,
    Nat.choose_zero_right, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.MahlerBasis (hypothesis)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoidWithOne M
inst_1 : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 - Δ_[1]^[n] f 0 =
    ∑ k ∈ range (n + 1),
      (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • (f (HAdd.hAdd (α := M) (↑k : M) (↑R : M)) - f (↑k : M))
have this : ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 = Δ_[1]^[n] f (↑R : M)
Tactic: have : ∑ k ∈ Finset.range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 = Δ_[1]^[n] f R := by
    simpa only [← Function.iterate_add_apply, add_comm, nsmul_one, add_zero] using
      (shift_eq_sum_fwdDiff_iter 1 (Δ_[1]^[n] f) R 0).symm
-- 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 (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)
have 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)
Tactic: rw [bojanic_mahler_step1 _ _ (one_le_pow₀ hp.out.one_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)
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)
have 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)) :
    ℝ)
Tactic: refine (norm_add_le_max _ _).trans (max_le_max ?_ ?_)