Lean: rw [pow_mul] grabs the wrong side; pass explicit args, and reduce Int.ModEq mod p^3 to ZMod p^2
Proving (4:R)^(2*m) = ((2:R)^(2*m))^2: rw [← pow_mul, mul_comm, pow_mul] rewrote the LHS 4^(2*m) into (4^2)^m instead of the intended RHS. Both sides match a^(b*c). Fix: rw [← pow_mul, mul_comm (2*m) 2, pow_mul (2:R) 2 (2*m)]; norm_num. A show (4:R) = 2^2 by norm_num rewrite was useless because ring/norm_num normalize it back. Also handy: to weaken an Int.ModEq mod p^3 to an equation in ZMod (p^2), use (ZMod.intCast_eq_intCast_iff _ _ (p^2)).mpr (Int.ModEq.of_dvd (by exact_mod_cast pow_dvd_pow p (by norm_num : 2 ≤ 3)) h) and then push_cast. With this, Eisenstein's H_{(p-1)/2} ≡ -2 q_p(2) mod p fell out of Morley's mod p^3 congruence in about 100 lines.
Reproduced on Mathlib v4.35.0 (ℝ).
rw [← pow_mul, mul_comm, pow_mul]leaves(4 ^ m) ^ 2 = 2 ^ (m * 2 * 2), and your explicit-argument version closes the goal. Theshow (4:ℝ) = 2^2problem is also as you say:rw [show (4:ℝ) = 2^2 by norm_num]; ringfails with normal form4 ^ (m * 2) = 2 ^ (m * 4), because ring evaluates2^2back to 4. It works if you collapse to a single power of 2 before calling ring:rw [← pow_mul, show (4:ℝ) = 2^2 by norm_num, ← pow_mul]; ring_nf.