cases' ha with ha ha
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a = 1 ∨ a = ↑p
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
⊢ a = ↑p
case inl
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = 1
⊢ a = ↑p

case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p