-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem coeff_frobenius_charP (x : 𝕎 R) (n : ℕ) : coeff (frobenius x) n = x.coeff n ^ p

Proof state:
case calc_3
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k => x.coeff k) (X n ^ p) = x.coeff n ^ p

Tactic:
rw [map_pow, aeval_X]

Result:
no goals

Proof state:
case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k => x.coeff k) (frobeniusPoly p n) =
    (eval₂Hom ((algebraMap (ZMod p) R).comp (Int.castRingHom (ZMod p))) fun k => x.coeff k) (frobeniusPoly p n)

Tactic:
apply eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval x.coeff) (frobeniusPoly p n) = x.coeff n ^ p

Tactic:
calc
  aeval (fun k => x.coeff k) (frobeniusPoly p n) =
      aeval (fun k => x.coeff k)
        (MvPolynomial.map (Int.castRingHom (ZMod p)) (frobeniusPoly p n)) := ?_
  _ = aeval (fun k => x.coeff k) (X n ^ p : MvPolynomial ℕ (ZMod p)) := ?_
  _ = x.coeff n ^ p := ?_

Result:
case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k => x.coeff k) (frobeniusPoly p n) =
    (aeval fun k => x.coeff k) ((MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))

case calc_2
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k => x.coeff k) ((MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n)) =
    (aeval fun k => x.coeff k) (X n ^ p)

case calc_3
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k => x.coeff k) (X n ^ p) = x.coeff n ^ p

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ (aeval x.coeff) (frobeniusPoly p n) = x.coeff n ^ p

Tactic:
letI : Algebra (ZMod p) R := ZMod.algebra _ _

Result:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval x.coeff) (frobeniusPoly p n) = x.coeff n ^ p

Proof state:
case calc_2
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k => x.coeff k) ((MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n)) =
    (aeval fun k => x.coeff k) (X n ^ p)

Tactic:
rw [frobeniusPoly_zmod]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ (frobenius x).coeff n = x.coeff n ^ p

Tactic:
rw [coeff_frobenius]

Result:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ (aeval x.coeff) (frobeniusPoly p n) = x.coeff n ^ p

Proof state:
case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k => x.coeff k) (frobeniusPoly p n) =
    (aeval fun k => x.coeff k) ((MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))

Tactic:
conv_rhs => rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]

Result:
case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k => x.coeff k) (frobeniusPoly p n) =
    (eval₂Hom ((algebraMap (ZMod p) R).comp (Int.castRingHom (ZMod p))) fun k => x.coeff k) (frobeniusPoly p n)