-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem dvd_of_isCyclotomicExtension [IsCyclotomicExtension {n} ℚ K] {ζ : K}
    {l : ℕ} (hζ : IsPrimitiveRoot ζ l) (hl : l ≠ 0) : l ∣ 2 * n

Proof state:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
key : φ (l.lcm ↑n) ≤ Module.finrank ℚ K
⊢ l ∣ 2 * ↑n

Tactic:
rw [IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat n.2)] at key

Result:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
key : φ (l.lcm ↑n) ≤ φ ↑n
⊢ l ∣ 2 * ↑n

Proof state:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
key : φ (l.lcm ↑n) ≤ φ ↑n
⊢ l ∣ 2 * ↑n

Tactic:
rcases _root_.dvd_lcm_right l n with ⟨r, hr⟩

Result:
case intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
key : φ (l.lcm ↑n) ≤ φ ↑n
r : ℕ
hr : GCDMonoid.lcm l ↑n = ↑n * r
⊢ l ∣ 2 * ↑n

Proof state:
case intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
r : ℕ
hr : GCDMonoid.lcm l ↑n = ↑n * r
ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)
key : φ r ≤ 1
⊢ l ∣ 2 * ↑n

Tactic:
have rpos : 0 < r := by
  refine Nat.pos_of_ne_zero (fun h ↦ ?_)
  simp only [h, mul_zero, _root_.lcm_eq_zero_iff, PNat.ne_zero, or_false] at hr
  exact hl.1 hr

Result:
case intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
r : ℕ
hr : GCDMonoid.lcm l ↑n = ↑n * r
ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)
key : φ r ≤ 1
rpos : 0 < r
⊢ l ∣ 2 * ↑n

Proof state:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
⊢ l ∣ 2 * ↑n

Tactic:
have key := IsPrimitiveRoot.lcm_totient_le_finrank hζ hroot
  (cyclotomic.irreducible_rat <| Nat.lcm_pos (Nat.pos_of_ne_zero hl.1) n.2)

Result:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
key : φ (l.lcm ↑n) ≤ Module.finrank ℚ K
⊢ l ∣ 2 * ↑n

Proof state:
case intro.inl
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
r : ℕ
hr : GCDMonoid.lcm l ↑n = ↑n
ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * ↑n

Tactic:
rw [← hr]

Result:
case intro.inl
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
r : ℕ
hr : GCDMonoid.lcm l ↑n = ↑n
ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * GCDMonoid.lcm l ↑n

Proof state:
case intro.inl
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
r : ℕ
hr : GCDMonoid.lcm l ↑n = ↑n * r
ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * ↑n

Tactic:
rw [key, mul_one] at hr

Result:
case intro.inl
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
r : ℕ
hr : GCDMonoid.lcm l ↑n = ↑n
ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * ↑n

Proof state:
case intro.inr
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
r : ℕ
hr : GCDMonoid.lcm l ↑n = ↑n * r
ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)
rpos : 0 < r
key : r = 2
⊢ l ∣ 2 * ↑n

Tactic:
rw [key, mul_comm] at hr

Result:
case intro.inr
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n
r : ℕ
hr : GCDMonoid.lcm l ↑n = 2 * ↑n
ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)
rpos : 0 < r
key : r = 2
⊢ l ∣ 2 * ↑n