Galois Autₛ fixed is Unit

theorem galoisAutₛ_fixed_isUnit (hq5 : q % 8 = 5) {α : ℕ} (hα : 1 ≤ α)    {b : (powTwoCyclotomic (R := ZMod q) α).CyclotomicRing}    (hbfix : galoisAutₛ α (conjExp α) (conjExp_odd α) b = b) (hb0 : b ≠ 0) :    IsUnit b := by  classical  obtain ⟨p₁, p₂, hp₁, hp₂, hcop, hf⟩ := exists_irreducible_factorization q hq5 hα  have hswap12 : Associated p₁.reverse p₂ := no_selfReciprocal_factor q hq5 hα hp₁ hp₂ hf  have hswap21 : Associated p₂.reverse p₁ :=    no_selfReciprocal_factor q hq5 hα hp₂ hp₁ (by rw [hf]; ring)  set mk := Ideal.Quotient.mk (powTwoCyclotomic (R := ZMod q) α).modIdeal with hmkdef  have hmk_zero : ∀ z : (ZMod q)[X], mk z = 0 ↔ (X ^ (2 ^ α) + 1 : (ZMod q)[X]) ∣ z := fun z => by    rw [hmkdef, Ideal.Quotient.eq_zero_iff_mem, modIdeal, powTwoCyclotomic_toPoly,      Ideal.mem_span_singleton]  -- `mk X` is a unit (`(mk X)^{2^{α+1}} = 1`)  have hmkX_unit : IsUnit (mk X) :=    IsUnit.of_mul_eq_one ((mk X) ^ (conjExp α)) (by      rw [mul_comm, ← pow_succ, conjExp, Nat.sub_add_cancel Nat.one_le_two_pow, ← map_pow,        mk_X_pow_conductor_eq_one α])  obtain ⟨g, rfl⟩ := Ideal.Quotient.mk_surjective b  by_contra hbnu  have hncop : ¬ IsCoprime g (X ^ (2 ^ α) + 1 : (ZMod q)[X]) := by    rintro ⟨u, v, huv⟩    refine hbnu (IsUnit.of_mul_eq_one (mk u) ?_)    have := congrArg mk huv    rwa [map_add, map_mul, map_mul, (hmk_zero _).mpr (dvd_refl _), mul_zero, add_zero, map_one,      mul_comm] at this  -- the key step: a factor `p` of `g` forces its "reverse partner" `p'` to divide `g` too  have keystep : ∀ (p p' : (ZMod q)[X]), Associated p.reverse p' →      p' ∣ (X ^ (2 ^ α) + 1 : (ZMod q)[X]) → p ∣ g → p' ∣ g := by    intro p p' hpp' hp'f hpg    have hd1 : mk p' ∣ mk p.reverse := map_dvd mk hpp'.symm.dvd    rw [mk_reverse_eq_galoisAutₛ_mul q α p] at hd1    have hd2 : mk p' ∣ galoisAutₛ α (conjExp α) (conjExp_odd α) (mk p) :=      ((hmkX_unit.pow p.natDegree).dvd_mul_right).mp hd1    have hd3 : galoisAutₛ α (conjExp α) (conjExp_odd α) (mk p) ∣ mk g := by      obtain ⟨h, hh⟩ := hpg      refine ⟨galoisAutₛ α (conjExp α) (conjExp_odd α) (mk h), ?_⟩      rw [← map_mul, ← hbfix, hh, map_mul]    obtain ⟨c, hc⟩ := hd2.trans hd3    obtain ⟨c', rfl⟩ := Ideal.Quotient.mk_surjective c    have hz : (X ^ (2 ^ α) + 1 : (ZMod q)[X]) ∣ (g - p' * c') := by      rw [← hmk_zero, map_sub, map_mul, ← hc, sub_self]    have : p' ∣ (g - p' * c') := hp'f.trans hz    simpa using dvd_add this (Dvd.intro c' rfl)  rw [hf, IsCoprime.mul_right_iff, not_and_or] at hncop  have hfg : (X ^ (2 ^ α) + 1 : (ZMod q)[X]) ∣ g := by    rw [hf]    rcases hncop with h1 | h2    · have hp1g : p₁ ∣ g := by        by_contra hnd        exact h1 (isCoprime_comm.mp ((hp₁.coprime_iff_not_dvd).mpr hnd))      exact hcop.mul_dvd hp1g (keystep p₁ p₂ hswap12 (hf ▸ dvd_mul_left p₂ p₁) hp1g)    · have hp2g : p₂ ∣ g := by        by_contra hnd        exact h2 (isCoprime_comm.mp ((hp₂.coprime_iff_not_dvd).mpr hnd))      exact hcop.mul_dvd (keystep p₂ p₁ hswap21 (hf ▸ dvd_mul_right p₁ p₂) hp2g) hp2g  exact hb0 ((hmk_zero g).mpr hfg)