-- Mathlib/NumberTheory/NumberField/Units/Basic.lean
theorem rootsOfUnity_eq_one [NumberField K] {k : ℕ+} (hc : Nat.Coprime k (torsionOrder K))
    {ζ : (𝓞 K)ˣ} : ζ ∈ rootsOfUnity k (𝓞 K) ↔ ζ = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
⊢ ζ ∈ rootsOfUnity (↑k) (𝓞 K) ↔ ζ = 1

Tactic:
rw [mem_rootsOfUnity]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
⊢ ζ ^ ↑k = 1 ↔ ζ = 1

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ ↑k

Tactic:
exact orderOf_dvd_of_pow_eq_one h

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ ζ ∈ torsion K

Tactic:
rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ = 1
⊢ ζ ^ ↑k = 1

Tactic:
rw [h, one_pow]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ ζ = 1

Tactic:
refine orderOf_eq_one_iff.mp (Nat.eq_one_of_dvd_coprimes hc ?_ ?_)

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ ↑k

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ ↑(torsionOrder K)

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
hζ : ζ ∈ torsion K
⊢ orderOf ζ ∣ ↑(torsionOrder K)

Tactic:
rw [orderOf_submonoid (⟨ζ, hζ⟩ : torsion K)]

Result:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
hζ : ζ ∈ torsion K
⊢ orderOf ⟨ζ, hζ⟩ ∣ ↑(torsionOrder K)

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
hζ : ζ ∈ torsion K
⊢ orderOf ⟨ζ, hζ⟩ ∣ ↑(torsionOrder K)

Tactic:
exact orderOf_dvd_card

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
⊢ ζ ^ ↑k = 1 ↔ ζ = 1

Tactic:
refine ⟨fun h => ?_, fun h => by rw [h, one_pow]⟩

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ ζ = 1

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ ↑(torsionOrder K)

Tactic:
have hζ : ζ ∈ torsion K := by
  rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
  exact ⟨k, k.prop, h⟩

Result:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
hζ : ζ ∈ torsion K
⊢ orderOf ζ ∣ ↑(torsionOrder K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
k : ℕ+
hc : (↑k).Coprime ↑(torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1

Tactic:
exact ⟨k, k.prop, h⟩

Result:
no goals