-- Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
theorem is_roots_of_minpoly [DecidableEq K] :
    primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Proof state:
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Tactic:
by_cases hn : n = 0

Result:
case pos
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : n = 0
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Proof state:
case a
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots ↔ (map (Int.castRingHom K) (minpoly ℤ μ)).IsRoot (μ ^ m)

Tactic:
rw [← mem_roots]

Result:
case a
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ map (Int.castRingHom K) (minpoly ℤ μ) ≠ 0

Proof state:
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
x : K
hx : x ∈ primitiveRoots n K
⊢ x ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Tactic:
obtain ⟨m, _, hcop, rfl⟩ := (isPrimitiveRoot_iff h).1 ((mem_primitiveRoots hpos).1 hx)

Result:
case neg.intro.intro.intro
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Proof state:
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Tactic:
intro x hx

Result:
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
x : K
hx : x ∈ primitiveRoots n K
⊢ x ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Proof state:
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Tactic:
have : NeZero n := ⟨hn⟩

Result:
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Proof state:
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Tactic:
have hpos := Nat.pos_of_ne_zero hn

Result:
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Proof state:
case pos
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : n = 0
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Tactic:
simp_all

Result:
no goals

Proof state:
case neg.intro.intro.intro
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Tactic:
simp only [Multiset.mem_toFinset, mem_roots]

Result:
case neg.intro.intro.intro
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots

Proof state:
case neg.intro.intro.intro
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots

Tactic:
convert pow_isRoot_minpoly h hcop using 0

Result:
case a
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots ↔ (map (Int.castRingHom K) (minpoly ℤ μ)).IsRoot (μ ^ m)

Proof state:
case a
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ map (Int.castRingHom K) (minpoly ℤ μ) ≠ 0

Tactic:
exact map_monic_ne_zero <| minpoly.monic <| isIntegral h hpos

Result:
no goals