apply (card_classGroup_eq_one_iff (R := 𝓞 (CyclotomicField (⟨2, two_pos⟩ : ℕ+) ℚ))).2
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField 2 ℚ))) = 1
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsPrincipalIdealRing (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))