Exists irreducible factorization

theorem exists_irreducible_factorization (hq5 : q % 8 = 5) {α : ℕ} (hα : 1 ≤ α) :    ∃ p₁ p₂ : (ZMod q)[X], Irreducible p₁ ∧ Irreducible p₂ ∧ IsCoprime p₁ p₂ ∧      (X ^ (2 ^ α) + 1 : (ZMod q)[X]) = p₁ * p₂ := by  classical  have hqcop : ¬ (q ∣ 2 ^ (α + 1)) := by    intro h    have hq2 : q ∣ 2 := Nat.Prime.dvd_of_dvd_pow Fact.out h    have := Nat.le_of_dvd (by norm_num) hq2; omega  haveI : NeZero ((2 ^ (α + 1) : ℕ) : ZMod q) :=    ⟨by rw [Ne, ZMod.natCast_eq_zero_iff]; exact hqcop⟩  set f : (ZMod q)[X] := cyclotomic (2 ^ (α + 1)) (ZMod q) with hf  have hfne : f ≠ 0 := cyclotomic_ne_zero _ _  have hf_monic : f.Monic := cyclotomic.monic _ _  have hsqf : Squarefree f := squarefree_cyclotomic _ _  have hnodup := (UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hfne).mp hsqf  have hcard : Multiset.card (UniqueFactorizationMonoid.normalizedFactors f) = 2 := by    have h2 := cyclotomic_card_normalizedFactors q hq5 hα    rw [← hf] at h2    rwa [← Multiset.toFinset_card_of_nodup hnodup]  obtain ⟨a, b, hab⟩ := Multiset.card_eq_two.mp hcard  have ha_mem : a ∈ UniqueFactorizationMonoid.normalizedFactors f := by rw [hab]; simp  have hb_mem : b ∈ UniqueFactorizationMonoid.normalizedFactors f := by rw [hab]; simp  have ha_irr := UniqueFactorizationMonoid.irreducible_of_normalized_factor a ha_mem  have hb_irr := UniqueFactorizationMonoid.irreducible_of_normalized_factor b hb_mem  have ha_monic : a.Monic := by    have h := UniqueFactorizationMonoid.normalize_normalized_factor a ha_mem    rw [← h]; exact monic_normalize ha_irr.ne_zero  have hb_monic : b.Monic := by    have h := UniqueFactorizationMonoid.normalize_normalized_factor b hb_mem    rw [← h]; exact monic_normalize hb_irr.ne_zero  have hne : a ≠ b := by have := hnodup; rw [hab] at this; simpa using this  have hprod : a * b = f := by    have hassoc : Associated (a * b) f := by      have := UniqueFactorizationMonoid.prod_normalizedFactors hfne      rwa [hab, Multiset.prod_pair] at this    calc a * b = normalize (a * b) := ((ha_monic.mul hb_monic).normalize_eq_self).symm      _ = normalize f := normalize_eq_normalize_iff.mpr ⟨hassoc.dvd, hassoc.symm.dvd⟩      _ = f := hf_monic.normalize_eq_self  have hcop : IsCoprime a b := by    rw [ha_irr.coprime_iff_not_dvd]    intro hdvd    have hassoc : Associated a b := ha_irr.associated_of_dvd hb_irr hdvd    refine hne ?_    calc a = normalize a := (ha_monic.normalize_eq_self).symm      _ = normalize b := normalize_eq_normalize_iff.mpr ⟨hassoc.dvd, hassoc.symm.dvd⟩      _ = b := hb_monic.normalize_eq_self  exact ⟨a, b, ha_irr, hb_irr, hcop, by rw [Xpow_add_one_eq_cyclotomic q α, ← hf, ← hprod]⟩