Working with Modular Arithmetic

Stream: Is there code for X?

[Sophia C]

So, I'm using the really helpful mod_cases tactic, and it's leaving me a few subgoals which all have assumptions of the form h : p ≡ k [MOD 3]. It would be really helpful if I could rewrite that as ∃ k : ℕ, 3 * k + 1 = p but I'm not seeing anything in Mathlib.Data.Nat.ModEq that would enable me to do that easily. Is there something I'm missing here?

[Bolton Bailey]

I'm a bit confused by the k becoming existentially quantified. But if you are trying to get out of ModEq I would think your best bet would be to apply Nat.modEq_iff_dvd and then go from there.