-- 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:
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
hG' : ∃ ζ, IsPrimitiveRoot ζ (Nat.card G)
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
⊢ ∃ φ, φ a ≠ 1

Tactic:
obtain ⟨ζ, hζ⟩ := hG'

Result:
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

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
⊢ ∃ φ, φ a ≠ 1

Tactic:
have hζg : orderOf ζ ∣ orderOf g := by
  rw [← hζ.eq_orderOf, orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]

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
hζg : orderOf ζ ∣ orderOf 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)
ha : φ a = 1
k : ℕ
hk : g ^ k = a
⊢ a = 1

Tactic:
rw [← hk, map_pow] at ha

Result:
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

Proof state:
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
⊢ orderOf ζ ∣ orderOf g

Tactic:
rw [← hζ.eq_orderOf, orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]

Result:
no goals

Proof state:
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
⊢ IsPrimitiveRoot (φ g) (Nat.card G)

Tactic:
rwa [monoidHomOfForallMemZpowers_apply_gen hg hζg]

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
⊢ ∃ φ, φ a ≠ 1

Tactic:
have hφg : IsPrimitiveRoot (φ g) (Nat.card G) := by
  rwa [monoidHomOfForallMemZpowers_apply_gen hg hζ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
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
⊢ ∃ φ, φ a ≠ 1

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

Tactic:
let inst : Fintype G := Fintype.ofFinite _

Result:
G : Type u_7
G' : Type u_8
inst✝³ : CommGroup G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
hG' : ∃ ζ, IsPrimitiveRoot ζ (Nat.card G)
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite 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
hg : a ∈ Subgroup.zpowers g
⊢ a = 1

Tactic:
rw [← mem_powers_iff_mem_zpowers, Submonoid.mem_powers_iff] at hg

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 : ∃ n, g ^ n = a
⊢ a = 1

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
⊢ ∃ φ, φ a ≠ 1

Tactic:
let φ := monoidHomOfForallMemZpowers hg hζ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
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζ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
hg : ∃ n, g ^ n = a
⊢ a = 1

Tactic:
obtain ⟨k, hk⟩ := hg

Result:
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)
ha : φ a = 1
k : ℕ
hk : g ^ k = a
⊢ a = 1