-- Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean
/-- If `M` satisfies `HasEnoughRootsOfUnity`, then the group of `n`th roots of unity
in `M` (is cyclic and) has order `n`. -/
lemma natCard_rootsOfUnity (M : Type*) [CommMonoid M] (n : ℕ) [NeZero n]
    [HasEnoughRootsOfUnity M n] :
    Nat.card (rootsOfUnity n M) = n

Proof state:
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
⊢ Nat.card ↥(rootsOfUnity n M) = n

Tactic:
obtain ⟨ζ, h⟩ := exists_primitiveRoot M n

Result:
case intro
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ Nat.card ↥(rootsOfUnity n M) = n

Proof state:
case intro.refine_1
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ Monoid.exponent ↥(rootsOfUnity n M) ∣ n

Tactic:
exact Monoid.exponent_dvd_of_forall_pow_eq_one fun g ↦ OneMemClass.coe_eq_one.mp g.prop

Result:
no goals

Proof state:
case intro.refine_2.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⟨⋯.unit, ?intro.refine_2.refine_1⟩
⊢ orderOf ⋯.unit ∣ Monoid.exponent ↥(rootsOfUnity n M)

Tactic:
rw [← Subgroup.orderOf_mk]

Result:
case intro.refine_2.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⟨⋯.unit, ?intro.refine_2.refine_1⟩
⊢ orderOf ⟨⋯.unit, ?intro.refine_2.refine_2.ha⟩ ∣ Monoid.exponent ↥(rootsOfUnity n M)

case intro.refine_2.refine_2.ha
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⟨⋯.unit, ?intro.refine_2.refine_1⟩
⊢ ⋯.unit ∈ ?m.6158

M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⟨⋯.unit, ?intro.refine_2.refine_1⟩
⊢ Subgroup Mˣ

Proof state:
case intro.refine_2.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⟨⋯.unit, ?intro.refine_2.refine_1⟩
⊢ orderOf ⟨⋯.unit, ?intro.refine_2.refine_2.ha⟩ ∣ Monoid.exponent ↥(rootsOfUnity n M)

case intro.refine_2.refine_2.ha
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⟨⋯.unit, ?intro.refine_2.refine_1⟩
⊢ ⋯.unit ∈ ?m.6158

M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⟨⋯.unit, ?intro.refine_2.refine_1⟩
⊢ Subgroup Mˣ

Tactic:
exact Monoid.order_dvd_exponent ζ'

Result:
no goals

Proof state:
case intro.refine_2.refine_1
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ ⋯.unit ^ n = 1

Tactic:
rw [← Units.eq_iff, Units.val_pow_eq_pow_val, IsUnit.unit_spec, h.pow_eq_one, Units.val_one]

Result:
no goals

Proof state:
case intro.refine_2.refine_1
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ ⋯.unit ∈ rootsOfUnity n M

Tactic:
simp only [mem_rootsOfUnity, PNat.mk_coe]

Result:
case intro.refine_2.refine_1
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ ⋯.unit ^ n = 1

Proof state:
case intro
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ Nat.card ↥(rootsOfUnity n M) = n

Tactic:
rw [← IsCyclic.exponent_eq_card]

Result:
case intro
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ Monoid.exponent ↥(rootsOfUnity n M) = n

Proof state:
case intro.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ orderOf ⋯.unit ∣ Monoid.exponent ↥(rootsOfUnity n M)

Tactic:
let ζ' : rootsOfUnity n M := ⟨(h.isUnit <| NeZero.pos n).unit, ?_⟩

Result:
case intro.refine_2.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⟨⋯.unit, ?intro.refine_2.refine_1⟩
⊢ orderOf ⋯.unit ∣ Monoid.exponent ↥(rootsOfUnity n M)

case intro.refine_2.refine_1
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ ⋯.unit ∈ rootsOfUnity n M

Proof state:
case intro
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ Monoid.exponent ↥(rootsOfUnity n M) = n

Tactic:
refine dvd_antisymm ?_ ?_

Result:
case intro.refine_1
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ Monoid.exponent ↥(rootsOfUnity n M) ∣ n

case intro.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ n ∣ Monoid.exponent ↥(rootsOfUnity n M)

Proof state:
case intro.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ orderOf ζ ∣ Monoid.exponent ↥(rootsOfUnity n M)

Tactic:
rw [← (h.isUnit <| NeZero.pos n).unit_spec, orderOf_units]

Result:
case intro.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ orderOf ⋯.unit ∣ Monoid.exponent ↥(rootsOfUnity n M)

Proof state:
case intro.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ n ∣ Monoid.exponent ↥(rootsOfUnity n M)

Tactic:
nth_rewrite 1 [h.eq_orderOf]

Result:
case intro.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ orderOf ζ ∣ Monoid.exponent ↥(rootsOfUnity n M)