LaurentSeries coefficient dividing

Stream: mathlib4

[Eric Paul]

I want to show that if I have a LaurentSeries and I divide by X, then all the coefficients shift down:

import Mathlib

theorem div_X_shifts_coeff {R : Type*} [Field R] (a : LaurentSeries R) :
    ∀z : ℤ, (a / (HahnSeries.single 1 1)).coeff z = a.coeff (z + 1) := by sorry

I have been struggling to make any progress here. My attempts to make things happen, like in the following, become daunting quite quickly:

import Mathlib

theorem div_X_shifts_coeff {R : Type*} [Field R] (a : LaurentSeries R) :
    ∀z : ℤ, (a / (HahnSeries.single 1 1)).coeff z = a.coeff (z + 1) := by
  intro z
  unfold_projs
  simp [DivInvMonoid.div']

I would appreciate any advice or help in working with this.

[Ruben Van de Velde]

That was pretty hard:

import Mathlib

theorem div_X_shifts_coeff {R : Type*} [Field R] (a : LaurentSeries R) (z : ℤ) (h : a.coeff (z + 1) ≠ 0):
    (a / (HahnSeries.single 1 1)).coeff z = a.coeff (z + 1) := by
  rw [div_eq_mul_inv]
  rw [@HahnSeries.mul_coeff]
  rw [← RatFunc.single_inv _ one_ne_zero, inv_one]
  simp_rw [HahnSeries.single_coeff, mul_ite, mul_zero, mul_one]

  rw [Finset.sum_ite, Finset.sum_const_zero, add_zero]
  have (x) : x ∈ Finset.filter (fun x : ℤ × ℤ => x.2 = -1) (Finset.addAntidiagonal (HahnSeries.isPWO_support a) (HahnSeries.isPWO_support ((HahnSeries.single (-1)) (1 : R))) z) → a.coeff x.1 = a.coeff (z + 1) := by
    simp
    intro h0 h1 h2 h3
    rw [← eq_sub_iff_add_eq, h1, sub_neg_eq_add] at h2
    rw [h2]
  rw [Finset.sum_congr rfl this]
  convert Finset.sum_singleton _ (⟨z+1, -1⟩ : ℤ × ℤ)
  ext x
  simp [Prod.ext_iff, h]
  intro hx
  rw [← eq_sub_iff_add_eq, hx]
  simp
  intro hx2
  rwa [hx2]

[Eric Paul]

Oh man, that is intense. Thank you so much for looking at it!
I'll inspect your proof. Hopefully I can extract ideas to make future such calculations easier.

Also, the hypothesis h : a.coeff (z + 1) ≠ 0 shouldn't be necessary right?

[Ruben Van de Velde]

I didn't check where that came from, exactly

[Eric Paul]

As far as I can tell, it's because the sum is only using things in the support of a.

Here is a slight modification so that it works without the hypothesis

import Mathlib

theorem div_X_shifts_coeff {R : Type*} [Field R] (a : LaurentSeries R) (z : ℤ) :
    (a / (HahnSeries.single 1 1)).coeff z = a.coeff (z + 1) := by
  rw [div_eq_mul_inv]
  rw [@HahnSeries.mul_coeff]
  rw [← RatFunc.single_inv _ one_ne_zero, inv_one]
  simp_rw [HahnSeries.single_coeff, mul_ite, mul_zero, mul_one]

  rw [Finset.sum_ite, Finset.sum_const_zero, add_zero]
  have (x) : x ∈ Finset.filter (fun x : ℤ × ℤ => x.2 = -1) (Finset.addAntidiagonal (HahnSeries.isPWO_support a) (HahnSeries.isPWO_support ((HahnSeries.single (-1)) (1 : R))) z) → a.coeff x.1 = a.coeff (z + 1) := by
    simp
    intro _ h1 h2 h3
    rw [← eq_sub_iff_add_eq, h1, sub_neg_eq_add] at h2
    rw [h2]
  rw [Finset.sum_congr rfl this]
  if h : a.coeff (z + 1) = 0 then
    simp [h]
  else
    convert Finset.sum_singleton _ (⟨z+1, -1⟩ : ℤ × ℤ)
    ext x
    simp [Prod.ext_iff, h]
    intro hx
    rw [← eq_sub_iff_add_eq, hx]
    simp
    intro hx2
    rwa [hx2]