Counterpart of rw for modeq

Stream: Is there code for X?

[Stuart Presnell]

If I have a modeq like hcd : c ≡ d [MOD m] and an expression like h : c * a ≡ d * b [MOD m] with the same modulus, is there a tactic like rw that will let me replace c with d (or vice versa) in h?

[Alex J. Best]

Not really, its often better to use zmod rather than modeq for this reason, as then its an actual type where rw works. tactic#cc can also be useful though when you have some equivalence relation like this and complicated chains of equivalences

[Kyle Miller]

When I was plugging my students' number theory homework into Lean, unfortunately it was a lot of manual docs#int.modeq.mul and docs#int.modeq.add

(In principle, it seems like it should be possible to have a tactic that zmodifies everything, does the rewrite, then unzmodifies everything again.)

[Heather Macbeth]

I have a WIP tactic for modular arithmetic problems, which is basically apply_rules for a curated set of modular arithmetic facts.