-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
/-- If `G` is cyclic of order `n` and `G'` contains a primitive `n`th root of unity,
then for each `a : G` with `a ≠ 1` there is a homomorphism `φ : G →* G'` such that `φ a ≠ 1`. -/
lemma IsCyclic.exists_apply_ne_one {G G' : Type*} [CommGroup G] [IsCyclic G] [Finite G]
    [CommGroup G'] (hG' : ∃ ζ : G', IsPrimitiveRoot ζ (Nat.card G)) ⦃a : G⦄ (ha : a ≠ 1) :
    ∃ φ : G →* G', φ a ≠ 1

Proof state:
case h
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
⊢ φ a ≠ 1

Tactic:
contrapose! ha

Result:
case h
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
ha : φ a = 1
⊢ a = 1

Proof state:
case h.intro.intro
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
l : ℕ
ha : φ g ^ (Nat.card G * l) = 1
hk : g ^ (Nat.card G * l) = a
⊢ a = 1

Tactic:
rw [← hk, pow_mul, Nat.card_eq_fintype_card, pow_card_eq_one, one_pow]

Result:
no goals

Proof state:
case intro.intro
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
⊢ ∃ φ, φ a ≠ 1

Tactic:
use φ

Result:
case h
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
⊢ φ a ≠ 1

Proof state:
case h
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
ha : φ a = 1
⊢ a = 1

Tactic:
specialize hg a

Result:
case h
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg✝ : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg✝ hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
ha : φ a = 1
hg : a ∈ Subgroup.zpowers g
⊢ a = 1

Proof state:
case h.intro
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
k : ℕ
ha : φ g ^ k = 1
hk : g ^ k = a
⊢ a = 1

Tactic:
obtain ⟨l, rfl⟩ := (hφg.pow_eq_one_iff_dvd k).mp ha

Result:
case h.intro.intro
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
l : ℕ
ha : φ g ^ (Nat.card G * l) = 1
hk : g ^ (Nat.card G * l) = a
⊢ a = 1

Proof state:
case intro
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
⊢ ∃ φ, φ a ≠ 1

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)

Result:
case intro.intro
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ ∃ φ, φ a ≠ 1