Principal is maximal iff irred

lemma principal_is_maximal_iff_irred {F : Type} [Field F] (f : F[X]) :    (principalIdeal f).IsMaximal ↔ Irreducible f := by    constructor <;> intro h;    · -- If the ideal generated by f is maximal, then f is non-zero.      have h_nonzero : f ≠ 0 := by        intro hf;        subst hf        rw [principalIdeal] at h        rw [Ideal.isMaximal_iff] at h        have hmax := h.2 (Ideal.span ({Polynomial.X} : Set F[X])) Polynomial.X        have hXmem : (Polynomial.X : F[X]) ∈ Ideal.span ({Polynomial.X} : Set F[X]) :=          Ideal.mem_span_singleton_self _        have hXnotmem : (Polynomial.X : F[X]) ∉ Ideal.span ({0} : Set F[X]) := by          simp        have htop : (1 : F[X]) ∈ Ideal.span ({Polynomial.X} : Set F[X]) := by          apply hmax          · simp          · exact hXnotmem          · exact hXmem        exact absurd (Polynomial.X_dvd_iff.mp (by simpa [Ideal.mem_span_singleton] using htop))          (by norm_num);      -- If the ideal generated by f is maximal, then f is prime.      have h_prime : Prime f := by        rw [ ← Ideal.span_singleton_prime h_nonzero ];        exact h.isPrime;      exact h_prime.irreducible;    · rw [ Ideal.isMaximal_iff ];      constructor;      · exact fun h' => h.not_isUnit <| isUnit_of_dvd_one <| Ideal.mem_span_singleton.mp h';      · intro J x hJ hx hxJ        have h_coprime : IsCoprime f x := by          exact h.coprime_iff_not_dvd.mpr fun h' => hx <| Ideal.mem_span_singleton.mpr h';        rcases h_coprime with ⟨ a, b, h ⟩;        exact h.symm ▸          J.add_mem            (J.mul_mem_left a (hJ (Ideal.subset_span (Set.mem_singleton f))))            (J.mul_mem_left b hxJ)