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
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
refine : Tendsto.{0, u_1} (β := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (a n) n) cofinite (𝓝 0)
⊢ HasSum (α := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (a n) n) (mahlerSeries a)

Tactic:
refine (NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero ?_).hasSum

Premises used: Summable.hasSum, NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
rw :
  ∀ (ha : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖a x‖) atTop (𝓝 0)),
    Tendsto (β := ℝ) (fun (x : ℕ) ↦ norm (E := C(ℤ_[p], E)) (mahlerTerm (a x) x)) cofinite (𝓝 0)
⊢ Tendsto.{0, u_1} (β := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (a n) n) cofinite (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero] at ha ⊢

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖a x‖) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ norm (E := C(ℤ_[p], E)) (mahlerTerm (a x) x)) cofinite (𝓝 0)

Tactic:
simpa only [norm_mahlerTerm, Nat.cofinite_eq_atTop] using ha

Premises used: PadicInt.norm_mahlerTerm, Nat.cofinite_eq_atTop
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
x : ℤ_[p]
⊢ Eq (α := E) ((mahlerSeries a : (a : ℤ_[p]) → E) x : E)
    (∑' (n : ℕ), HSMul.hSMul (α := ℤ_[p]) ((mahler n : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p]) (a n) : E)

Tactic:
simp only [mahlerSeries, ← ContinuousMap.tsum_apply (hasSum_mahlerSeries ha).summable,
    mahlerTerm_apply]

Premises used: PadicInt.mahlerTerm_apply, ContinuousMap.tsum_apply, PadicInt.mahlerSeries, HasSum.summable, PadicInt.hasSum_mahlerSeries
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
i : ℕ
⊢ m < i + (n + 1)

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
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
⊢ ∀ (i : ℕ), m.choose (i + (n + 1)) = 0

Tactic:
have h_van (i) : m.choose (i + (n + 1)) = 0 := Nat.choose_eq_zero_of_lt (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
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
h_van : ∀ (i : ℕ), m.choose (i + (n + 1)) = 0
⊢ Summable.{u_1, 0} (α := E) fun (i : ℕ) ↦ m.choose (i + (n + 1)) • a (i + (n + 1))

Tactic:
simpa only [h_van, zero_smul] using summable_zero

Premises used: zero_smul, summable_zero
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
h_van : ∀ (i : ℕ), m.choose (i + (n + 1)) = 0
⊢ Summable.{u_1, 0} (α := E) fun (i : ℕ) ↦ m.choose (i + (n + 1)) • a (i + (n + 1))

Tactic:
have aux : Summable fun i ↦ m.choose (i + (n + 1)) • a (i + (n + 1)) := by
    simpa only [h_van, zero_smul] using summable_zero
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
h_van : ∀ (i : ℕ), m.choose (i + (n + 1)) = 0
aux : Summable.{u_1, 0} (α := E) fun (i : ℕ) ↦ m.choose (i + (n + 1)) • a (i + (n + 1))
⊢ Eq (α := E) ((mahlerSeries a : (a : ℤ_[p]) → E) (↑m : ℤ_[p]) : E) (∑ i ∈ range (n + 1), m.choose i • a i : E)

Tactic:
simp only [mahlerSeries_apply ha, mahler_natCast_eq, Nat.cast_smul_eq_nsmul, add_zero,
    ← aux.sum_add_tsum_nat_add' (f := fun i ↦ m.choose i • a i), h_van, zero_smul, tsum_zero]

Premises used: PadicInt.mahlerSeries_apply, mahler_natCast_eq, tsum_zero, zero_smul, Nat.cast_smul_eq_nsmul, Summable.sum_add_tsum_nat_add', add_zero
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
simp :
  Eq.{u_1 + 1} (α := E)
    (∑ x ∈ range (n + 1),
      HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ))
        ((mahlerSeries a : (a : ℤ_[p]) → E) (HSMul.hSMul (β := ℤ_[p]) x 1) : E))
    (∑ x ∈ range (n + 1),
      HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ))
        (∑ x_1 ∈ range (n + 1), (HSMul.hSMul (β := ℕ) x 1).choose x_1 • a x_1))
⊢ Eq (α := E) (Δ_[1]^[n] (⇑(mahlerSeries a) : (a : ℤ_[p]) → E) 0 : E)
    (Δ_[1]^[n] (fun (k : ℕ) ↦ ∑ j ∈ range (n + 1), k.choose j • a j) 0 : E)

Tactic:
simp only [fwdDiff_iter_eq_sum_shift, zero_add]

Premises used: fwdDiff_iter_eq_sum_shift, zero_add
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ Eq.{u_1 + 1} (α := E)
    (∑ x ∈ range (n + 1),
      HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ))
        ((mahlerSeries a : (a : ℤ_[p]) → E) (HSMul.hSMul (β := ℤ_[p]) x 1) : E))
    (∑ x ∈ range (n + 1),
      HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ))
        (∑ x_1 ∈ range (n + 1), (HSMul.hSMul (β := ℕ) x 1).choose x_1 • a x_1))

Tactic:
Finset.sum_congr rfl fun j hj ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
refine :
  ∀ (j : ℕ) (hj : j ∈ range (n + 1)),
    HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ))
        ((mahlerSeries a : (a : ℤ_[p]) → E) (HSMul.hSMul (β := ℤ_[p]) j 1) : E) =
      HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ))
        (∑ x ∈ range (n + 1), (HSMul.hSMul (β := ℕ) j 1).choose x • a x)
⊢ Eq.{u_1 + 1} (α := E)
    (∑ x ∈ range (n + 1),
      HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ))
        ((mahlerSeries a : (a : ℤ_[p]) → E) (HSMul.hSMul (β := ℤ_[p]) x 1) : E))
    (∑ x ∈ range (n + 1),
      HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ))
        (∑ x_1 ∈ range (n + 1), (HSMul.hSMul (β := ℕ) x 1).choose x_1 • a x_1))

Tactic:
refine Finset.sum_congr rfl fun j hj ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n j : ℕ
hj : j ∈ range (n + 1)
rw :
  HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ))
      ((mahlerSeries a : (a : ℤ_[p]) → E) (↑j : ℤ_[p]) : E) =
    HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ))
      (∑ x ∈ range (n + 1), (HSMul.hSMul (β := ℕ) j 1).choose x • a x)
rw₁ :
  HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ))
      ((mahlerSeries a : (a : ℤ_[p]) → E) (↑j : ℤ_[p]) : E) =
    HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ))
      (∑ x ∈ range (n + 1), Nat.choose (↑j : ℕ) x • a x)
rw₂ :
  HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ)) (∑ i ∈ range (n + 1), j.choose i • a i) =
    HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ))
      (∑ x ∈ range (n + 1), Nat.choose (↑j : ℕ) x • a x)
rw₃ rw₄ :
  HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ)) (∑ i ∈ range (n + 1), j.choose i • a i) =
    HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ)) (∑ x ∈ range (n + 1), j.choose x • a x)
⊢ HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ))
      ((mahlerSeries a : (a : ℤ_[p]) → E) (HSMul.hSMul (β := ℤ_[p]) j 1) : E) =
    HSMul.hSMul (β := E) (HPow.hPow (α := ℤ) (-1) (n - j) * (↑(n.choose j) : ℤ))
      (∑ x ∈ range (n + 1), (HSMul.hSMul (β := ℕ) j 1).choose x • a x)

Tactic:
rw [nsmul_one, nsmul_one,
      mahlerSeries_apply_nat ha (Nat.lt_succ_iff.mp <| Finset.mem_range.mp hj), Nat.cast_id]

Premises used: Nat.cast_id, PadicInt.mahlerSeries_apply_nat, Finset.mem_range, Nat.lt_succ_iff, Iff.mp, nsmul_one
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
simp :
  Eq.{u_1 + 1} (α := E)
    (∑ x ∈ range (n + 1),
      ∑ x_1 ∈ range (n + 1),
        (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ)) • (0 + HSMul.hSMul (β := ℕ) x 1).choose x_1 • a x_1)
    (∑ x ∈ range (n + 1),
      ∑ k ∈ range (n + 1),
        (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • (0 + HSMul.hSMul (β := ℕ) k 1).choose x • a x)
⊢ Eq.{u_1 + 1} (α := E) (Δ_[1]^[n] (fun (k : ℕ) ↦ ∑ j ∈ range (n + 1), k.choose j • a j) 0 : E)
    (∑ j ∈ range (n + 1), Δ_[1]^[n] (fun (k : ℕ) ↦ k.choose j • a j) 0 : E)

Tactic:
simp only [fwdDiff_iter_eq_sum_shift, smul_sum]

Premises used: fwdDiff_iter_eq_sum_shift, Finset.smul_sum
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
rw rw₁ :
  Eq.{u_1 + 1} (α := E)
    (∑ y ∈ range (n + 1),
      ∑ x ∈ range (n + 1),
        (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ)) • (0 + HSMul.hSMul (β := ℕ) x 1).choose y • a y)
    (∑ x ∈ range (n + 1),
      ∑ k ∈ range (n + 1),
        (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • (0 + HSMul.hSMul (β := ℕ) k 1).choose x • a x)
⊢ Eq.{u_1 + 1} (α := E)
    (∑ x ∈ range (n + 1),
      ∑ x_1 ∈ range (n + 1),
        (HPow.hPow (α := ℤ) (-1) (n - x) * (↑(n.choose x) : ℤ)) • (0 + HSMul.hSMul (β := ℕ) x 1).choose x_1 • a x_1)
    (∑ x ∈ range (n + 1),
      ∑ k ∈ range (n + 1),
        (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • (0 + HSMul.hSMul (β := ℕ) k 1).choose x • a x)

Tactic:
rw [sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ Eq.{u_1 + 1} (α := E) (∑ j ∈ range (n + 1), Δ_[1]^[n] (fun (k : ℕ) ↦ k.choose j • a j) 0)
    (∑ j ∈ range (n + 1), HSMul.hSMul (α := ℤ) (Δ_[1]^[n] (fun (k : ℕ) ↦ (↑(k.choose j) : ℤ)) 0 : ℤ) (a j))

Tactic:
simp only [fwdDiff_iter_eq_sum_shift, zero_add, sum_smul, smul_assoc,
      natCast_zsmul]

Premises used: Finset.sum_smul, smul_assoc, fwdDiff_iter_eq_sum_shift, zero_add, natCast_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
inst_4 : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ j ∈ range (n + 1), HSMul.hSMul (α := ℤ) (Δ_[1]^[n] (fun (k : ℕ) ↦ (↑(k.choose j) : ℤ)) 0 : ℤ) (a j) = a n

Tactic:
simp only [fwdDiff_iter_choose_zero, ite_smul, one_smul, zero_smul, sum_ite_eq,
      Finset.mem_range, lt_add_iff_pos_right, zero_lt_one, ↓reduceIte]

Premises used: lt_add_iff_pos_right, Finset.mem_range, fwdDiff_iter_choose_zero, one_smul, zero_lt_one, zero_smul, reduceIte, ite_smul, Finset.sum_ite_eq
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
f : C(ℤ_[p], E)
⊢ HasSum.{u_1, 0} (α := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n)
    (mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0)

Tactic:
have : HasSum (fun n ↦ mahlerTerm (Δ_[1]^[n] f 0) n)
      (mahlerSeries (Δ_[1]^[·] f 0) : C(ℤ_[p], E)) :=
    hasSum_mahlerSeries (fwdDiff_tendsto_zero f)
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
f : C(ℤ_[p], E)
this :
  HasSum.{u_1, 0} (α := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n)
    (mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0)
⊢ HasSum.{u_1, 0} (α := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n)
    (mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0)

Tactic:
this
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
f : C(ℤ_[p], E)
this :
  HasSum.{u_1, 0} (α := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n)
    (mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0)
h : f = mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0
⊢ HasSum (fun (n : ℕ) ↦ mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n) f

Tactic:
convert! this using 1
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
f : C(ℤ_[p], E)
this :
  HasSum.{u_1, 0} (α := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n)
    (mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0)
⊢ f = mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0

Tactic:
ContinuousMap.coe_injective (denseRange_natCast.equalizer
    (map_continuous f) (map_continuous _) (funext fun n ↦ ?_))

Premises used: DenseRange.equalizer, PadicInt.denseRange_natCast, ContinuousMap.coe_injective, funext, ContinuousMapClass.map_continuous
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
f : C(ℤ_[p], E)
this :
  HasSum.{u_1, 0} (α := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n)
    (mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0)
h :
  ∀ (n : ℕ),
    Eq (α := E) (Function.comp (β := ℤ_[p]) (⇑f : (a : ℤ_[p]) → E) Nat.cast n)
      (Function.comp (β := ℤ_[p]) (⇑(mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0) : (a : ℤ_[p]) → E)
        Nat.cast n)
⊢ f = mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0

Tactic:
refine ContinuousMap.coe_injective (denseRange_natCast.equalizer
    (map_continuous f) (map_continuous _) (funext fun n ↦ ?_))

Premises used: DenseRange.equalizer, PadicInt.denseRange_natCast, ContinuousMap.coe_injective, funext, ContinuousMapClass.map_continuous
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
f : C(ℤ_[p], E)
this :
  HasSum.{u_1, 0} (α := C(ℤ_[p], E)) (fun (n : ℕ) ↦ mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n)
    (mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0)
n : ℕ
⊢ Eq (α := E) (Function.comp (β := ℤ_[p]) (⇑f : (a : ℤ_[p]) → E) Nat.cast n)
    (Function.comp (β := ℤ_[p]) (⇑(mahlerSeries fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0) : (a : ℤ_[p]) → E)
      Nat.cast n)

Tactic:
simpa [mahlerSeries_apply_nat (fwdDiff_tendsto_zero f) le_rfl]
    using shift_eq_sum_fwdDiff_iter 1 f n 0

Premises used: le_rfl, PadicInt.fwdDiff_tendsto_zero, PadicInt.mahlerSeries_apply_nat, OfNat.ofNat, DFunLike.coe, shift_eq_sum_fwdDiff_iter
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f g : C(ℤ_[p], E)
h :
  ∀ (x : ℕ),
    Eq (α := E)
      (({ toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑(f + g) : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
              zero_at_infty' := ⋯ } :
            (a : ℕ) → E)
          x :
        E)
      ((HAdd.hAdd (α := ℕ →C₀ E)
              { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ :
                ℕ →C₀ E }
              { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑g : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ :
                ℕ →C₀ E } :
            (a : ℕ) → E)
          x :
        E)
⊢ { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑(f + g) : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ } =
    HAdd.hAdd (α := ℕ →C₀ E)
      { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ :
        ℕ →C₀ E }
      { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑g : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ :
        ℕ →C₀ E }

Tactic:
ext x
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n : ℕ
x_1 : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f g : C(ℤ_[p], E)
x : ℕ
⊢ Eq (α := E)
    (({ toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑(f + g) : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ } :
          (a : ℕ) → E)
        x :
      E)
    ((HAdd.hAdd (α := ℕ →C₀ E)
            { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ :
              ℕ →C₀ E }
            { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑g : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ :
              ℕ →C₀ E } :
          (a : ℕ) → E)
        x :
      E)

Tactic:
simp only [ContinuousMap.coe_add, fwdDiff_iter_add, Pi.add_apply,
      ZeroAtInftyContinuousMap.coe_mk, ZeroAtInftyContinuousMap.coe_add]

Premises used: ZeroAtInftyContinuousMap.coe_mk, Pi.add_apply, fwdDiff_iter_add, ContinuousMap.coe_add, ZeroAtInftyContinuousMap.coe_add
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
r : ℤ_[p]
f : C(ℤ_[p], E)
h :
  ∀ (n : ℕ),
    Eq (α := E)
      (({ toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑(r • f) : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
              zero_at_infty' := ⋯ } :
            (a : ℕ) → E)
          n :
        E)
      ((HSMul.hSMul (α := ℤ_[p]) (β := ℕ →C₀ E) ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) r : ℤ_[p])
              { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ :
                ℕ →C₀ E } :
            (a : ℕ) → E)
          n :
        E)
⊢ { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑(r • f) : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ } =
    HSMul.hSMul (α := ℤ_[p]) (β := ℕ →C₀ E) ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) r : ℤ_[p])
      { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ :
        ℕ →C₀ E }

Tactic:
ext n
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n_1 : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
r : ℤ_[p]
f : C(ℤ_[p], E)
n : ℕ
⊢ Eq (α := E)
    (({ toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑(r • f) : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ } :
          (a : ℕ) → E)
        n :
      E)
    ((HSMul.hSMul (α := ℤ_[p]) (β := ℕ →C₀ E) ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) r : ℤ_[p])
            { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ :
              ℕ →C₀ E } :
          (a : ℕ) → E)
        n :
      E)

Tactic:
simp only [ContinuousMap.coe_smul, RingHom.id_apply, ZeroAtInftyContinuousMap.coe_mk,
      ZeroAtInftyContinuousMap.coe_smul, Pi.smul_apply, fwdDiff_iter_const_smul]

Premises used: ZeroAtInftyContinuousMap.coe_smul, ZeroAtInftyContinuousMap.coe_mk, RingHom.id_apply, ContinuousMap.coe_smul, fwdDiff_iter_const_smul, Pi.smul_apply
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
simp :
  norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ : ℕ →C₀ E },
              map_add' := ⋯, map_smul' := ⋯ : LinearMap (R := ℤ_[p]) (RingHom.id ℤ_[p]) C(ℤ_[p], E) (ℕ →C₀ E) } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          f)) =
    ‖f‖
⊢ norm (E := ℕ →C₀ E)
      (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ : ℕ →C₀ E },
              map_add' := ⋯, map_smul' := ⋯, invFun := fun (a : ℕ →C₀ E) ↦ mahlerSeries (⇑a : (a : ℕ) → E),
              left_inv := ⋯, right_inv := ⋯ : C(ℤ_[p], E) ≃ₗ[ℤ_[p]] ℕ →C₀ E } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          f :
        ℕ →C₀ E) =
    ‖f‖

Tactic:
simp only [LinearEquiv.coe_mk, ← ZeroAtInftyContinuousMap.norm_toBCF_eq_norm]

Premises used: LinearEquiv.coe_mk, ZeroAtInftyContinuousMap.norm_toBCF_eq_norm