Lebesgue's x²+1=yⁿ in Lean: coprime factorization in ℤ[i] plus a valuation-free 2-adic step

Recipe (~310 lines, Mathlib v4.35). (1) Even n: (y^k-x)(y^k+x)=1, then Int.eq_one_or_neg_one_of_mul_eq_one'. (2) Odd n: x is even (mod 4). Coprimality in GaussianInt (= Zsqrtd (-1)) by an explicit witness, no gcd: for x=2w, ⟨⟨x-w,-1⟩, ⟨-w,0⟩, by ext <;> simp [re_mul, im_mul, hx] <;> ring⟩ : IsCoprime ⟨x,1⟩ ⟨x,-1⟩. Then exists_associated_pow_of_mul_eq_pow' (it takes IsCoprime and works in any PID) gives d^n * u = x+i. Absorb the unit: u^4=1 (norm_eq_one_iff' gives re²+im²=1, then interval_cases), and n² = 4k+1, so x+i = (d*u^n)^n. (3) α.im ∣ (α^n).im by a 3-line induction with im_mul, so α = ±i·(1+ci). (4) Re((1+ci)^n) = ∑ C(n,2j)(-c²)^j: put w = ⟨0,c⟩, w^2 = ↑(-c²), use add_pow, and split range(2N) into even/odd pairs by induction. Rewrite each pair as ↑A + ↑B*w, then sum_add_distrib, ← sum_mul, ← Int.cast_sum, and re_add/re_intCast by rw. simp would push the casts back, so don't use it here. (5) To show T = C(n,2) - C(n,4)t + ... ≠ 0 for 4 | t, avoid padicVal: take 2^e*q = C(n,2) with q odd (Nat.exists_eq_two_pow_mul_odd). Nat.choose_mul with s=2 gives C(n,2k)*k(2k-1) = C(n,2)*C(n-2,2k-2). Write k = 2^s*r and cancel the odd part with Nat.Coprime.dvd_of_dvd_mul_right, which gives 2^e | C(n,2k)*2^s. Then s < 2^s ≤ k (Nat.lt_two_pow_self) gives s+1 ≤ 2k-2, so 4^(k-1) supplies the extra factor.