Calculations using `SModEq`

Stream: new members

[Robert Spencer]

Apologies if this is a stupid question - I'm still quite a hack-and-slash lean coder.

If I am working in some module modulo a submodule and want to rewrite some terms modulo that submodule. For example:

variable {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p : Submodule R M} (n : ℕ)

-- This works fine. `simp` is able to `rw [h]` under the summation
theorem EqTest (a : M) (g : Fin n → M) (h : ∀ i, g i = a) :
  n • a = ∑ i, (g i) := by
    simp[h]

-- This does not. `h` is no longer a straight equality, but rather an equality of `Quotient.mk`s
theorem SModEqTest (a : M) (g : Fin n → M) (h : ∀ i, g i ≡ a [SMOD p]) :
  n • a ≡ ∑ i, (g i) [SMOD p] := by
    simp[h]

I think I understand why this is tricky to simplify - you have to go into the summand, then realise that the sum of images in the quotient is the image of sums etc etc.

I'd hoped that simp with h (and possibly SModEq.sum) would be able to work this out, but am at a little bit of a loss as to how to proceed. I could be quite explicit, such as

-- Works
theorem SModEqTest (a : M) (g : Fin n → M) (h : ∀ i ∈ Finset.univ, g i ≡ a [SMOD p]) :
  n • a ≡ ∑ i, (g i) [SMOD p] := by
    apply SModEq.trans _ (SModEq.sum h).symm
    simp
    rfl

but my actual use case has summations with factors and more complex terms that would require some rewriting/puling out of sums that I don't want to manually do.

Is there a simpler way to deal with this? Should I be working in Quotient.mks?

[Ruben Van de Velde]

grw maybe, but I don't know if that works under sums. But you realized correctly that there is a subtlety here to needs to be dealt with somewhere

[Robert Spencer]

Hmm, grw wasn't happy

As an aside, I've found rewriting under sums to be a particular pain in my current project. Sometimes simp manages, but sometimes I find myself in very long conv blocks to get to the term I need. My lack familiarity with lean tactics means I end up just doing very explicit rw, apply and simp all over the place. What is the "better practice" when dealing with many (nested) sums?