Fermat's x⁴ − y⁴ = z² descent in Lean: two uses of coprime_classification', and a trap with gcd + set

Mathlib has not_fermat_42 (x⁴+y⁴=z²) but not the difference. A descent of about 260 lines: strong induction on x.natAbs with 0 < x. First prove a helper ih' that accepts any-sign smaller x' (apply ih to |x'|, using |x'|^4 = x'^4 via pow_mul and sq_abs). Non-coprime case: set g := (Int.gcd x y : ℤ). The obtained Int.gcd_dvd_left facts still mention ↑(x.gcd y), so rw [← hg_def] at hx' hy' and then clear_value g. Otherwise rewriting hx' also rewrites the x inside gcd x y, and ring fails with an odd-looking goal. Then (Int.pow_dvd_pow_iff two_ne_zero).mp gives g² ∣ z. Parity: ∀ k l c : ZMod 4, (2*k)^4 - (2*l+1)^4 ≠ c^2 := by decide. Coprimality of y² and z: (hcop.symm.pow).add_mul_left_right (-(y^2)) gives IsCoprime (y²) (z*z) after convert, then .of_mul_right_left. For y even, apply PythagoreanTriple.coprime_classification' to (z, y², x²) and then again to (n, m, x) or (m, n, x) by parity. That gives (y/2)² = rs(r²−s²). Split it with Int.sq_of_isCoprime three times (IsCoprime r (r²−s²) from hrs.pow_right.neg_right.add_mul_left_right r). Both signs of r²−s² = ±c² descend. Rational corollary (1 is not congruent): with D := a.den*b.den*c.den*q.den : ℕ, each r with r.den ∣ D has D*r = ↑(r.num*k) via rw [hk]; push_cast; rw [← Rat.mul_den_eq_num]; ring.