Sophie Germain's theorem (FLT case I, 2p+1 prime) in Lean: ~250 lines, the useful lemmas

Layout that worked. (1) Φ(y,w) := ∑_{i<p} y^i (-w)^(p-1-i). geom_sum₂_mul y (-w) p plus Odd.neg_pow gives (y+w)Φ = y^p + w^p, closed by linear_combination. For coprimality, Φ - p(-w)^(p-1) = ∑ (y^i - (-w)^i)(-w)^(p-1-i), and each term is divisible by y + w via sub_dvd_pow_sub_pow and sub_neg_eq_add. Take a prime r ∣ gcd (Nat.exists_prime_and_dvd on gcd ≠ 1, Int.gcd_dvd_natAbs_left), and use Nat.prime_iff_prime_int + Prime.dvd_or_dvd. Then Int.eq_pow_of_mul_eq_pow_odd (Mathlib.RingTheory.Int.Basic) yields both p-th powers at once. (2) Mod q = 2p+1: ZMod.pow_card_sub_one_eq_one with q-1 = p*2 and mul_self_eq_one_iff give n^p ∈ {0, ±1}. You must subst hq first: rw [hq] fails with 'motive is not type correct' because of the Fact instance. For the 27 sign cases: all_goals first | exact h3 (by linear_combination h) | .... (3) A coprimality contradiction mod q: cast the Bézout identity s*u + t*v = 1 into ZMod q. (4) Primitive reduction: set g := Int.gcd x y, take facts like Int.gcd_div_gcd_div_gcd first, then clear_value g before obtain ⟨x', hx'⟩ : (g:ℤ) ∣ x. Otherwise rw [hx'] also rewrites the x inside gcd x y. Int.pow_dvd_pow_iff gives g ∣ z. Pairwise coprimality from x^p + y^p = z^p comes from (cxy.pow).add_mul_left_right 1 and IsCoprime.pow_iff.