-- Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean
theorem FiniteField.Matrix.charpoly_pow_card {K : Type*} [Field K] [Fintype K] (M : Matrix n n K) :
    (M ^ Fintype.card K).charpoly = M.charpoly

Proof state:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ matPolyEquiv ((expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix) =
    matPolyEquiv (M.charmatrix ^ Fintype.card K)

Tactic:
rw [map_pow, matPolyEquiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow]

Result:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ matPolyEquiv ((expand K (p ^ k)).mapMatrix (M ^ p ^ k).charmatrix) = X ^ p ^ k - C (M ^ p ^ k)

case inl.intro.intro.mk.intro.a.h
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Commute X (C M)

Proof state:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix = M.charmatrix ^ Fintype.card K

Tactic:
refine matPolyEquiv.injective ?_

Result:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ matPolyEquiv ((expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix) =
    matPolyEquiv (M.charmatrix ^ Fintype.card K)

Proof state:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ matPolyEquiv ((expand K (p ^ k)).mapMatrix (M ^ p ^ k).charmatrix) = X ^ p ^ k - C (M ^ p ^ k)

Tactic:
exact (id (matPolyEquiv_eq_X_pow_sub_C (p ^ k) M) :)

Result:
no goals

Proof state:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = M.charpoly ^ Fintype.card K

Tactic:
rw [← FiniteField.expand_card]

Result:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (expand K (Fintype.card K)) (M ^ Fintype.card K).charpoly = M.charpoly ^ Fintype.card K

Proof state:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ detMonoidHom ((expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix) =
    detMonoidHom (M.charmatrix ^ Fintype.card K)

Tactic:
apply congr_arg det

Result:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix = M.charmatrix ^ Fintype.card K

Proof state:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (expand K (Fintype.card K)) (M ^ Fintype.card K).charpoly = M.charpoly ^ Fintype.card K

Tactic:
unfold charpoly

Result:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (expand K (Fintype.card K)) (M ^ Fintype.card K).charmatrix.det = M.charmatrix.det ^ Fintype.card K

Proof state:
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ ↑⟨k, kpos⟩
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
haveI : Fact p.Prime := ⟨hp⟩

Result:
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ ↑⟨k, kpos⟩
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Proof state:
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
cases (isEmpty_or_nonempty n).symm

Result:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

case inr
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Proof state:
case inl.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
this : CharP K p := hp
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
rcases FiniteField.card K p with ⟨⟨k, kpos⟩, ⟨hp, hk⟩⟩

Result:
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ ↑⟨k, kpos⟩
⊢ (M ^ Fintype.card K).charpoly = M.charpoly