exact Nat.div_dvd_of_dvd ((orderOf g).gcd_dvd_left ny)
case refine'_3
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
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
⊢ orderOf g / (orderOf g).gcd ny ∣ orderOf g
no goals