Fixed Subring Equiv Galois Field

theorem fixedSubringEquivGaloisField (hq5 : q % 8 = 5) {α κ : ℕ} (hα : 1 ≤ α)    (hk : 2 * 2 ^ κ ∣ 2 ^ α) :    Nonempty (fixedSubring (R := ZMod q) α (2 ^ κ) ≃+* GaloisField q (2 ^ κ)) := by  have hq2 : ¬ (q ∣ 2) := fun h => by have := Nat.le_of_dvd (by norm_num) h; omega  have h2 : (2 : ZMod q) ≠ 0 := by    have h2' : ((2 : ℕ) : ZMod q) ≠ 0 := by rw [Ne, ZMod.natCast_eq_zero_iff]; exact hq2    simpa using h2'  letI : Field (fixedSubring (R := ZMod q) α (2 ^ κ)) := (fixedSubring_isField q hq5 hα).toField  haveI : Fintype (GaloisField q (2 ^ κ)) := Fintype.ofFinite _  have hcardK : Fintype.card (fixedSubring (R := ZMod q) α (2 ^ κ)) = q ^ 2 ^ κ := by    rw [card_fixedSubring_eq q α κ h2 hk, ZMod.card q]  have hcardG : Fintype.card (GaloisField q (2 ^ κ)) = q ^ 2 ^ κ := by    rw [← Nat.card_eq_fintype_card, GaloisField.card q (2 ^ κ) (by positivity)]  exact ⟨FiniteField.ringEquivOfCardEq (hcardK.trans hcardG.symm)⟩