awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
⊢ ∃ (z : ℤ_[p]),
    Eq (α := ℤ_[p]) (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (0 : ℤ_[p]) ∧
      ‖z - a‖ <
          norm (E := ℤ_[p])
            (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
              ℤ_[p]) ∧
        norm (E := ℤ_[p])
              (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                  ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
                ℤ_[p]) =
            norm (E := ℤ_[p])
              (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                  ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
                ℤ_[p]) ∧
          ∀ (z' : ℤ_[p]),
            Eq (α := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
                (0 : ℤ_[p]) →
              ‖z' - a‖ <
                  norm (E := ℤ_[p])
                    (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
                      ℤ_[p]) →
                z' = z

Tactic:
exact if ha : F.aeval a = 0 then ⟨a, a_is_soln hnorm ha⟩
  else by
    exact ⟨soln_gen hnorm, eval_soln hnorm,
      soln_dist_to_a_lt_deriv hnorm ha, soln_deriv_norm hnorm, fun z => soln_unique hnorm ha z⟩

Premises used: Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
⊢ ∃ (z : ℤ_[p]),
    Eq (α := ℤ_[p]) (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (0 : ℤ_[p]) ∧
      ‖z - a‖ <
          norm (E := ℤ_[p])
            (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
              ℤ_[p]) ∧
        norm (E := ℤ_[p])
              (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                  ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
                ℤ_[p]) =
            norm (E := ℤ_[p])
              (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                  ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
                ℤ_[p]) ∧
          ∀ (z' : ℤ_[p]),
            Eq (α := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
                (0 : ℤ_[p]) →
              ‖z' - a‖ <
                  norm (E := ℤ_[p])
                    (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
                      ℤ_[p]) →
                z' = z

Tactic:
classical
  exact if ha : F.aeval a = 0 then ⟨a, a_is_soln hnorm ha⟩
  else by
    exact ⟨soln_gen hnorm, eval_soln hnorm,
      soln_dist_to_a_lt_deriv hnorm ha, soln_deriv_norm hnorm, fun z => soln_unique hnorm ha z⟩

Premises used: Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : (x : ℤ_[p]) → ℤ_[p] := fun (x : ℤ_[p]) ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
change : ‖f x‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
⊢ ‖Polynomial.eval x (ascPochhammer ℤ_[p] k)‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])

Tactic:
change ‖f x‖ ≤ ‖_‖
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : (x : ℤ_[p]) → ℤ_[p] := fun (x : ℤ_[p]) ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
⊢ Ne (α := ℤ_[p]) (↑k.factorial : ℤ_[p]) 0

Tactic:
have hC : (k.factorial : ℤ_[p]) ≠ 0 := Nat.cast_ne_zero.mpr k.factorial_ne_zero
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
⊢ ContinuousAt f x

Tactic:
have hf : ContinuousAt f x := Polynomial.continuousAt _
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
obtain :
  ∀ (δ : ℝ) (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])
⊢ ∃ (n : ℕ), ‖f x - f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])

Tactic:
obtain ⟨δ, hδp, hδ⟩ := Metric.continuousAt_iff.mp hf _ (norm_pos_iff.mpr hC)

Premises used: Iff.mpr, norm_pos_iff, Iff.mp, Metric.continuousAt_iff
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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])
obtain :
  ∀ (n : ℕ) (hn' : dist x (↑n : ℤ_[p]) < δ),
    ∃ (n : ℕ), ‖f x - f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[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

Premises used: PadicInt.denseRange_natCast, DenseRange.exists_dist_lt
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 : ℕ
hn' : dist x (↑n : ℤ_[p]) < δ
⊢ ∃ (n : ℕ), ‖f x - f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])

Tactic:
simpa only [← dist_eq_norm_sub'] using ⟨n, (hδ (dist_comm x n ▸ hn')).le⟩

Premises used: dist_eq_norm_sub'
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
obtain :
  ∀ (n : ℕ) (hn : ‖f x - f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])),
    ‖f x‖ ≤ 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⟩

Premises used: Nat.cast, Nat.factorial
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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])

Tactic:
sub_add_cancel (f x) _ ▸ (IsUltrametricDist.norm_add_le_max _ (f n)).trans (max_le hn ?_)

Premises used: Eq.rec, Nat.cast, IsUltrametricDist.norm_add_le_max, max_le, LE.le.trans, sub_add_cancel
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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])
refine : ‖f (↑n : ℤ_[p])‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
⊢ ‖f x‖ ≤ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])

Tactic:
refine sub_add_cancel (f x) _ ▸ (IsUltrametricDist.norm_add_le_max _ (f n)).trans (max_le hn ?_)
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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])
simp_rw :
  norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p]) * norm (E := ℤ_[p]) (↑(Ring.multichoose n k) : ℤ_[p]) ≤
    norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])
⊢ ‖f (↑n : ℤ_[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]

Premises used: Ring.factorial_nsmul_multichoose_eq_ascPochhammer, norm_mul, Nat.cast_mul, ascPochhammer_eval_cast, Polynomial.eval_eq_smeval, smul_eq_mul
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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])
⊢ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p]) * norm (E := ℤ_[p]) (↑(Ring.multichoose n k) : ℤ_[p]) ≤
    norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])

Tactic:
mul_le_of_le_one_right (norm_nonneg _) (norm_le_one _)

Premises used: mul_le_of_le_one_right, PadicInt.norm_le_one, norm_nonneg
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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])
⊢ norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p]) * norm (E := ℤ_[p]) (↑(Ring.multichoose n k) : ℤ_[p]) ≤
    norm (E := ℤ_[p]) (↑k.factorial : ℤ_[p])

Tactic:
exact mul_le_of_le_one_right (norm_nonneg _) (norm_le_one _)

Premises used: mul_le_of_le_one_right, PadicInt.norm_le_one, norm_nonneg
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ 0 < norm (E := ℚ_[p]) (↑k.factorial : ℚ_[p])

Tactic:
simpa using k.factorial_ne_zero

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
rw : ‖(↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p])‖ ≤ norm (E := ℚ_[p]) (↑k.factorial : ℚ_[p])
⊢ ‖(↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])‖ ≤ 1

Tactic:
rw [norm_div, div_le_one (by simpa using k.factorial_ne_zero)]

Premises used: div_le_one, norm_div
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ ‖(↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p])‖ ≤ norm (E := ℚ_[p]) (↑k.factorial : ℚ_[p])

Tactic:
x.norm_ascPochhammer_le k

Premises used: PadicInt.norm_ascPochhammer_le
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ ‖(↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p])‖ ≤ norm (E := ℚ_[p]) (↑k.factorial : ℚ_[p])

Tactic:
exact x.norm_ascPochhammer_le k

Premises used: PadicInt.norm_ascPochhammer_le
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
rw₇ rw₈ : Polynomial.smeval (ascPochhammer ℕ 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

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]

Premises used: Subtype.coe_inj, PadicInt.coe_natCast, mul_div_cancel₀, Polynomial.ascPochhammer_smeval_cast, nsmul_eq_mul, Polynomial.eval_eq_smeval, PadicInt.coe_mul
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous (Y := ℤ_[p]) fun (x : ℤ_[p]) ↦
    Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
      ((↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) : ℚ_[p]) / (↑k.factorial : ℚ_[p])) ⋯

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous (Y := ℤ_[p]) fun (x : ℤ_[p]) ↦ Ring.multichoose (x - (↑k : ℤ_[p]) + 1) k

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
⊢ (mahler k : (a : ℤ_[p]) → ℤ_[p]) x = Ring.choose x k

Tactic:
rfl

Premises used: Ring.choose, Ring.multichoose, rfl
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
⊢ Eq (α := ℤ_[p]) ((mahler k : (a : ℤ_[p]) → ℤ_[p]) (↑n : ℤ_[p])) (↑(n.choose k) : ℤ_[p])

Tactic:
simp only [mahler_apply, Ring.choose_natCast]

Premises used: Ring.choose_natCast, mahler_apply
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 : ℕ
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‖
⊢ norm.{u_2} (E := G) (Δ_[h]^[n] (⇑f : (a : M) → G) m : G) ≤ ‖f‖

Tactic:
rw [fwdDiff_iter_eq_sum_shift]

Premises used: fwdDiff_iter_eq_sum_shift
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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‖

Tactic:
norm_sum_le_of_forall_le_of_nonneg (norm_nonneg f) fun i _ ↦ ?_

Premises used: IsUltrametricDist.norm_sum_le_of_forall_le_of_nonneg, norm_nonneg
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 : ℕ
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‖
⊢ 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:
refine norm_sum_le_of_forall_le_of_nonneg (norm_nonneg f) fun i _ ↦ ?_

Premises used: IsUltrametricDist.norm_sum_le_of_forall_le_of_nonneg, norm_nonneg
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 i : ℕ
h_1 : 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:
(norm_zsmul_le _ _).trans (f.norm_coe_le_norm _)

Premises used: ContinuousMap.norm_coe_le_norm, IsUltrametricDist.norm_zsmul_le, LE.le.trans
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 i : ℕ
h_1 : 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:
exact (norm_zsmul_le _ _).trans (f.norm_coe_le_norm _)

Premises used: ContinuousMap.norm_coe_le_norm, IsUltrametricDist.norm_zsmul_le, LE.le.trans
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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)
rw₂ rw₃ : Δ_[1]^[n + R] f 0 = Δ_[1]^[n + R] f 0
⊢ Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0

Tactic:
rw [Nat.sub_add_cancel hR, Nat.choose_self, one_smul]

Premises used: one_smul, Nat.sub_add_cancel, Nat.choose_self
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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

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]
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
⊢ n + R = n + (R - 1 + 1)

Tactic:
lia
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
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))
⊢ Δ_[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)))

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]

Premises used: Iff.mpr, Nat.choose, neg_add_eq_sub, eq_sub_iff_add_eq, fwdDiff, Nat.iterate, add_comm, one_smul, Nat.sub_add_cancel, sub_eq_iff_eq_add, HAdd.hAdd, HSMul.hSMul, add_zero, OfNat.ofNat, Finset.sum_range_succ', Finset.sum_range_succ, Nat.choose_zero_right
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 (↑R : M)

Tactic:
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

Premises used: Function.iterate_add_apply, fwdDiff, Nat.iterate, add_comm, nsmul_one, add_zero, OfNat.ofNat, Eq.symm, shift_eq_sum_fwdDiff_iter
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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 (↑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
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
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
this : ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 = Δ_[1]^[n] f (↑R : M)
⊢ ∑ 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:
simp only [this, fwdDiff_iter_eq_sum_shift (1 : M) f n, mul_comm, nsmul_one, mul_smul, add_comm,
    add_zero, smul_sub, sum_sub_distrib]

Premises used: fwdDiff_iter_eq_sum_shift, add_comm, smul_sub, Finset.sum_sub_distrib, mul_comm, nsmul_one, add_zero, OfNat.ofNat, SemigroupAction.mul_smul