-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem card_primitiveRoots {ζ : R} {k : ℕ} (h : IsPrimitiveRoot ζ k) :
    #(primitiveRoots k R) = φ k

Proof state:
case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ b ∈ primitiveRoots k R, ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = b

Tactic:
intro ξ hξ

Result:
case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
hξ : ξ ∈ primitiveRoots k R
⊢ ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Proof state:
case neg.refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ a₁ < k, k.Coprime a₁ → ∀ a₂ < k, k.Coprime a₂ → ζ ^ a₁ = ζ ^ a₂ → a₁ = a₂

Tactic:
rintro i hi - j hj - H

Result:
case neg.refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
i : ℕ
hi : i < k
j : ℕ
hj : j < k
H : ζ ^ i = ζ ^ j
⊢ i = j

Proof state:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ #(primitiveRoots k R) = φ k

Tactic:
have : NeZero k := ⟨h0⟩

Result:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ #(primitiveRoots k R) = φ k

Proof state:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : k = 0
⊢ #(primitiveRoots k R) = φ k

Tactic:
simp [h0]

Result:
no goals

Proof state:
case neg.refine_3.intro.intro.intro
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
i : ℕ
hin : i < k
hi : i.Coprime k
H : ζ ^ i = ξ
⊢ ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Tactic:
exact ⟨i, ⟨hin, hi.symm⟩, H⟩

Result:
no goals

Proof state:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ #(primitiveRoots k R) = φ k

Tactic:
symm

Result:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ φ k = #(primitiveRoots k R)

Proof state:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
⊢ #(primitiveRoots k R) = φ k

Tactic:
by_cases h0 : k = 0

Result:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : k = 0
⊢ #(primitiveRoots k R) = φ k

case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ #(primitiveRoots k R) = φ k

Proof state:
case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
hξ : ξ ∈ primitiveRoots k R
⊢ ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Tactic:
rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0), h.isPrimitiveRoot_iff] at hξ

Result:
case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
hξ : ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
⊢ ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Proof state:
case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ b ∈ primitiveRoots k R, ∃ a, ∃ (ha : a ∈ filter (fun a => k.Coprime a) (range k)), (fun i x => ζ ^ i) a ha = b

Tactic:
simp only [exists_prop, mem_filter, mem_range, mem_univ]

Result:
case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ b ∈ primitiveRoots k R, ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = b

Proof state:
case neg.refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
i : ℕ
hi : i < k
j : ℕ
hj : j < k
H : ζ ^ i = ζ ^ j
⊢ i = j

Tactic:
exact h.pow_inj hi hj H

Result:
no goals

Proof state:
case neg.refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ (a : ℕ) (ha : a ∈ filter (fun a => k.Coprime a) (range k)), (fun i x => ζ ^ i) a ha ∈ primitiveRoots k R

Tactic:
simp only [and_imp, mem_filter, mem_range, mem_univ]

Result:
case neg.refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ a < k, k.Coprime a → ζ ^ a ∈ primitiveRoots k R

Proof state:
case neg.refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ a < k, k.Coprime a → ζ ^ a ∈ primitiveRoots k R

Tactic:
rintro i - hi

Result:
case neg.refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
i : ℕ
hi : k.Coprime i
⊢ ζ ^ i ∈ primitiveRoots k R

Proof state:
case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
hξ : ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
⊢ ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Tactic:
rcases hξ with ⟨i, hin, hi, H⟩

Result:
case neg.refine_3.intro.intro.intro
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
i : ℕ
hin : i < k
hi : i.Coprime k
H : ζ ^ i = ξ
⊢ ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Proof state:
case neg.refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
i : ℕ
hi : k.Coprime i
⊢ ζ ^ i ∈ primitiveRoots k R

Tactic:
rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0)]

Result:
case neg.refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
i : ℕ
hi : k.Coprime i
⊢ IsPrimitiveRoot (ζ ^ i) k

Proof state:
case neg.refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
i : ℕ
hi : k.Coprime i
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
exact h.pow_of_coprime i hi.symm

Result:
no goals

Proof state:
case neg.refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ filter (fun a => k.Coprime a) (range k)) (a₂ : ℕ)
    (ha₂ : a₂ ∈ filter (fun a => k.Coprime a) (range k)),
    (fun i x => ζ ^ i) a₁ ha₁ = (fun i x => ζ ^ i) a₂ ha₂ → a₁ = a₂

Tactic:
simp only [and_imp, mem_filter, mem_range, mem_univ]

Result:
case neg.refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ a₁ < k, k.Coprime a₁ → ∀ a₂ < k, k.Coprime a₂ → ζ ^ a₁ = ζ ^ a₂ → a₁ = a₂

Proof state:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ φ k = #(primitiveRoots k R)

Tactic:
refine Finset.card_bij (fun i _ ↦ ζ ^ i) ?_ ?_ ?_

Result:
case neg.refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ (a : ℕ) (ha : a ∈ filter (fun a => k.Coprime a) (range k)), (fun i x => ζ ^ i) a ha ∈ primitiveRoots k R

case neg.refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ filter (fun a => k.Coprime a) (range k)) (a₂ : ℕ)
    (ha₂ : a₂ ∈ filter (fun a => k.Coprime a) (range k)),
    (fun i x => ζ ^ i) a₁ ha₁ = (fun i x => ζ ^ i) a₂ ha₂ → a₁ = a₂

case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ b ∈ primitiveRoots k R, ∃ a, ∃ (ha : a ∈ filter (fun a => k.Coprime a) (range k)), (fun i x => ζ ^ i) a ha = b