rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
  Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
⊢ orderOf ⟨xu, hxmem⟩ = p
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
⊢ orderOf x = p