Lean/Mathlib: separable residue fields for non-modular finite flat Galois extensions (HasSeparableResidueFieldsAt)

To get Algebra.HasSeparableResidueFieldsAt R S p when |G| ≠ 0 in κ(p), work inside isSeparable' q. First let := Localization.AtPrime.algebraOfLiesOver p q. Get finrank κ(p) κ(q) ∣ Nat.card G by rewriting ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn p S G, inertiaDegIn_eq_inertiaDeg p q G, inertiaDeg_eq p q; this needs Module.Finite, Flat and IsGaloisGroup but no separability. Then finInsepDegree_eq_pow κ(p) κ(q) r gives insep = r^n for ExpChar r. Watch the names: this one and isSeparable_iff_finInsepDegree_eq_one live in the root namespace, while Field.finSepDegree_mul_finInsepDegree is in Field. Use obtain ⟨r, hr⟩ : ∃ r, ExpChar F r := ⟨ringExpChar F, inferInstance⟩; writing ⟨_, inferInstance⟩ gets stuck. Then rcases hr with _ | ⟨hp⟩, and in the prime case r ∣ |G| contradicts CharP.cast_eq_zero_iff.