IMO 2022 P5 (a^p = b!+p) in Lean: an elementary route with no LTE, and omega/rcases gotchas

A route that formalizes cleanly. First get b < 2p and p | a. For a ≠ p, set S = 1+a+…+a^(p-1); Mathlib's geom_sum_mul_add gives S*c+1 = (c+1)^p in ℕ. Every prime r | p-1 has a ≡ 1 mod r, by pow_gcd_eq_one with a^p = 1 and a^(r-1) = 1, using gcd(p, r-1) = 1. So S ≡ 1 mod r, gcd(p-1, S) = 1, and a - 1 = (p-1)K with K odd and K ≡ 1 mod p, which makes a too big. For a = p, work mod (p+1)^2: the lemma x^2 = 0 → (x-1)^n = (-1)^n (1 - n x) (a two-line induction) gives p^p - p ≡ p^2 - 1, while (p+1)^2 | b! for b > p. Gotchas: (1) rcases h.eq_or_lt with rfl | _ on p ≤ b eliminates b, not p, so later references to b fail. (2) omega did NOT treat p * (K / p) as an atom together with K % 2 facts. Introduce obtain ⟨j, hj⟩ : ∃ j, K = p * j + 1 and split on the parity of j with Nat.even_or_odd instead. (3) In this Mathlib, push_neg is deprecated in favour of push Not.