Conj Fixed Subring is Field

theorem conjFixedSubring_isField (hq5 : q % 8 = 5) {α : ℕ} (hα : 1 ≤ α) :    IsField (conjFixedSubring (R := ZMod q) α) := by  haveI hntC : Nontrivial (powTwoCyclotomic (R := ZMod q) α).CyclotomicRing := by    refine ⟨0, 1, fun h => ?_⟩    rw [show (1 : (powTwoCyclotomic (R := ZMod q) α).CyclotomicRing)          = Ideal.Quotient.mk _ 1 from (map_one _).symm, eq_comm,        Ideal.Quotient.eq_zero_iff_mem, modIdeal, powTwoCyclotomic_toPoly,        Ideal.mem_span_singleton] at h    have hdeg := Polynomial.natDegree_le_of_dvd h one_ne_zero    rw [Polynomial.natDegree_one, show (X ^ (2 ^ α) + 1 : (ZMod q)[X]) = X ^ (2 ^ α) + C 1 by      rw [map_one], Polynomial.natDegree_X_pow_add_C] at hdeg    exact absurd hdeg (Nat.not_le.mpr (by positivity))  haveI : Nontrivial (Rq (powTwoCyclotomic (R := ZMod q) α)) := by    refine ⟨0, 1, fun h => ?_⟩    have h2 := congrArg (Rq.equivQuotient (powTwoCyclotomic (R := ZMod q) α)) h    rw [map_zero, map_one] at h2    exact zero_ne_one h2  haveI : Nontrivial (conjFixedSubring (R := ZMod q) α) := inferInstance  refine ⟨exists_pair_ne _, mul_comm, ?_⟩  intro a ha  set Ψ := Rq.equivQuotient (powTwoCyclotomic (R := ZMod q) α) with hΨ  have haval_fix : conjAut α (a : Rq (powTwoCyclotomic (R := ZMod q) α)) = a :=    (mem_conjFixedSubring_iff α _).mp a.property  have haval0 : (a : Rq (powTwoCyclotomic (R := ZMod q) α)) ≠ 0 :=    fun h => ha (Subtype.ext (by rw [h]; rfl))  have hbfix : galoisAutₛ α (conjExp α) (conjExp_odd α) (Ψ a) = Ψ a := by    have h1 := (galoisAut_toQuotient α (conjExp α) (conjExp_odd α)      (a : Rq (powTwoCyclotomic (R := ZMod q) α))).symm    have h2 : galoisAut (powTwoCyclotomic α) (conjExp α)        (a : Rq (powTwoCyclotomic (R := ZMod q) α)) = a := by      have h := haval_fix; rwa [conjAut, galoisRingHom_apply] at h    rw [show Ψ (a : Rq (powTwoCyclotomic (R := ZMod q) α))        = Rq.toQuotient _ a from rfl, h1, h2]  have hb0 : Ψ (a : Rq (powTwoCyclotomic (R := ZMod q) α)) ≠ 0 := by    rw [Ne, ← map_zero Ψ]; exact fun h => haval0 (Ψ.injective h)  have hunitC := galoisAutₛ_fixed_isUnit q hq5 hα hbfix hb0  have hunitRq : IsUnit (a : Rq (powTwoCyclotomic (R := ZMod q) α)) := by    have := hunitC.map Ψ.symm    rwa [Ψ.symm_apply_apply] at this  obtain ⟨u, hu⟩ := hunitRq  set c : Rq (powTwoCyclotomic (R := ZMod q) α) := ↑u⁻¹ with hcdef  have hac : (a : Rq (powTwoCyclotomic (R := ZMod q) α)) * c = 1 := by    rw [hcdef, ← hu]; exact u.mul_inv  have hcfix : conjAut α c = c := by    have h1 : conjAut α ((a : Rq (powTwoCyclotomic (R := ZMod q) α)) * c) = 1 := by      rw [hac, map_one]    rw [map_mul, haval_fix] at h1    have h2 : (a : Rq (powTwoCyclotomic (R := ZMod q) α)) * conjAut α c        = (a : Rq (powTwoCyclotomic (R := ZMod q) α)) * c := by rw [h1, hac]    rw [← hu] at h2    exact (Units.mul_right_inj u).mp h2  exact ⟨⟨c, (mem_conjFixedSubring_iff α _).mpr hcfix⟩, Subtype.ext (by    rw [MulMemClass.coe_mul, OneMemClass.coe_one]; exact hac)⟩