Theorem: contains_two_primitive_roots (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
rcases Nat.eq_zero_or_pos p with (rfl | hppos)
State after:
case inl
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hy : IsPrimitiveRoot y q
hx : IsPrimitiveRoot x 0
⊢ (lcm 0 q).totient ≤ FiniteDimensional.finrank ℚ K

case inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
rcases Nat.eq_zero_or_pos q with (rfl | hqpos)
State after:
case inr.inl
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hppos : p > 0
hy : IsPrimitiveRoot y 0
⊢ (lcm p 0).totient ≤ FiniteDimensional.finrank ℚ K

case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
let k := lcm p q
State after:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hkpos : 0 < k := Nat.pos_of_ne_zero (Nat.lcm_ne_zero hppos.ne' hqpos.ne')
State after:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
let xu := IsUnit.unit (hx.isUnit hppos)
State after:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
let yu := IsUnit.unit (hy.isUnit hqpos)
State after:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K :=  by
  rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
    IsUnit.unit_spec]
  exact (hx.pow_eq_one_iff_dvd _).2 (dvd_lcm_left _ _)
State after:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K := by
  rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
    IsUnit.unit_spec]
  exact (hy.pow_eq_one_iff_dvd _).2 (dvd_lcm_right _ _)
State after:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hxuord : orderOf (⟨xu, hxmem⟩ : rootsOfUnity ⟨k, hkpos⟩ K) = p := by
  rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
    Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
  exact hx.eq_orderOf.symm
State after:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hyuord : orderOf (⟨yu, hymem⟩ : rootsOfUnity ⟨k, hkpos⟩ K) = q := by
  rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
    Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
  exact hy.eq_orderOf.symm
State after:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
obtain ⟨g : rootsOfUnity ⟨k, hkpos⟩ K, hg⟩ :=
  IsCyclic.exists_monoid_generator (α := rootsOfUnity ⟨k, hkpos⟩ K)
State after:
case inr.inr.intro
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr.intro
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
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
obtain ⟨nx, hnx⟩ := hg ⟨xu, hxmem⟩
State after:
case inr.inr.intro.intro
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⟩
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr.intro.intro
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⟩
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
obtain ⟨ny, hny⟩ := hg ⟨yu, hymem⟩
State after:
case inr.inr.intro.intro.intro
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⟩
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr.intro.intro.intro
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⟩
H : orderOf g = k
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hroot := IsPrimitiveRoot.orderOf g
State after:
case inr.inr.intro.intro.intro
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⟩
H : orderOf g = k
hroot : IsPrimitiveRoot g (orderOf g)
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr.intro.intro.intro
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⟩
H : orderOf g = k
hroot : IsPrimitiveRoot g (orderOf g)
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
rw [H, ← IsPrimitiveRoot.coe_submonoidClass_iff, ← IsPrimitiveRoot.coe_units_iff] at hroot
State after:
case inr.inr.intro.intro.intro
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⟩
H : orderOf g = k
hroot : IsPrimitiveRoot (↑↑g) k
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr.intro.intro.intro
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⟩
H : orderOf g = k
hroot : IsPrimitiveRoot (↑↑g) k
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
conv at hroot =>
  congr
  rfl
  rw [show k = (⟨k, hkpos⟩ : ℕ+) by simp]
State after:
case inr.inr.intro.intro.intro
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⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr.intro.intro.intro
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⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
haveI := IsPrimitiveRoot.adjoin_isCyclotomicExtension ℚ hroot
State after:
case inr.inr.intro.intro.intro
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⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
this : IsCyclotomicExtension {⟨k, hkpos⟩} ℚ ↥(Algebra.adjoin ℚ {↑↑g})
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K

State before:
case inr.inr.intro.intro.intro
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⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
this : IsCyclotomicExtension {⟨k, hkpos⟩} ℚ ↥(Algebra.adjoin ℚ {↑↑g})
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
convert Submodule.finrank_le (Subalgebra.toSubmodule (Algebra.adjoin ℚ ({g.1.1} : Set K)))
State after:
case h.e'_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⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
this : IsCyclotomicExtension {⟨k, hkpos⟩} ℚ ↥(Algebra.adjoin ℚ {↑↑g})
⊢ (lcm p q).totient = FiniteDimensional.finrank ℚ ↥(Subalgebra.toSubmodule (Algebra.adjoin ℚ {↑↑g}))

State before:
case h.e'_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⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
this : IsCyclotomicExtension {⟨k, hkpos⟩} ℚ ↥(Algebra.adjoin ℚ {↑↑g})
⊢ (lcm p q).totient = FiniteDimensional.finrank ℚ ↥(Subalgebra.toSubmodule (Algebra.adjoin ℚ {↑↑g}))
Tactic:
simpa using
  (IsCyclotomicExtension.finrank (Algebra.adjoin ℚ ({g.1.1} : Set K))
      (cyclotomic.irreducible_rat (PNat.pos ⟨k, hkpos⟩))).symm
State after:
no goals

State before:
case inl
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hy : IsPrimitiveRoot y q
hx : IsPrimitiveRoot x 0
⊢ (lcm 0 q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
simp
State after:
no goals

State before:
case inr.inl
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hppos : p > 0
hy : IsPrimitiveRoot y 0
⊢ (lcm p 0).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
simp
State after:
no goals

State before:
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
⊢ xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
Tactic:
rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
  IsUnit.unit_spec]
State after:
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
⊢ x ^ k = 1

State before:
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
⊢ x ^ k = 1
Tactic:
exact (hx.pow_eq_one_iff_dvd _).2 (dvd_lcm_left _ _)
State after:
no goals

State before:
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
⊢ yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
Tactic:
rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
  IsUnit.unit_spec]
State after:
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
⊢ y ^ k = 1

State before:
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
⊢ y ^ k = 1
Tactic:
exact (hy.pow_eq_one_iff_dvd _).2 (dvd_lcm_right _ _)
State after:
no goals

State before:
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
Tactic:
rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
  Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
State after:
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

State before:
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
Tactic:
exact hx.eq_orderOf.symm
State after:
no goals

State before:
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
⊢ orderOf ⟨yu, hymem⟩ = q
Tactic:
rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
  Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
State after:
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
⊢ orderOf y = q

State before:
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
⊢ orderOf y = q
Tactic:
exact hy.eq_orderOf.symm
State after:
no goals

State before:
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 = k
Tactic:
refine' Nat.dvd_antisymm (orderOf_dvd_of_pow_eq_one _) (Nat.lcm_dvd _ _)
State after:
case refine'_1
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⟩
⊢ g ^ k = 1

case refine'_2
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⟩
⊢ p ∣ orderOf g

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⟩
⊢ q ∣ orderOf g

State before:
case refine'_1
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⟩
⊢ g ^ k = 1
Tactic:
have := (mem_rootsOfUnity _ _).1 g.2
State after:
case refine'_1
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⟩
this : ↑g ^ ↑⟨k, hkpos⟩ = 1
⊢ g ^ k = 1

State before:
case refine'_1
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⟩
this : ↑g ^ ↑⟨k, hkpos⟩ = 1
⊢ g ^ k = 1
Tactic:
simp only [PNat.mk_coe] at this
State after:
case refine'_1
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⟩
this : ↑g ^ k = 1
⊢ g ^ k = 1

State before:
case refine'_1
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⟩
this : ↑g ^ k = 1
⊢ g ^ k = 1
Tactic:
exact_mod_cast this
State after:
no goals

State before:
case refine'_2
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⟩
⊢ p ∣ orderOf g
Tactic:
rw [← hxuord, ← hnx, orderOf_pow]
State after:
case refine'_2
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 nx ∣ orderOf g

State before:
case refine'_2
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 nx ∣ orderOf g
Tactic:
exact Nat.div_dvd_of_dvd ((orderOf g).gcd_dvd_left nx)
State after:
no goals

State before:
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⟩
⊢ q ∣ orderOf g
Tactic:
rw [← hyuord, ← hny, orderOf_pow]
State after:
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

State before:
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
Tactic:
exact Nat.div_dvd_of_dvd ((orderOf g).gcd_dvd_left ny)
State after:
no goals

State before:
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⟩
H : orderOf g = k
hroot : IsPrimitiveRoot (↑↑g) k
⊢ k = ↑⟨k, hkpos⟩
Tactic:
simp
State after:
no goals