-- Mathlib/FieldTheory/Finite/Polynomial.lean
theorem frobenius_zmod (f : MvPolynomial σ (ZMod p)) : frobenius _ p f = expand p f

Proof state:
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) f = (expand p) f

Tactic:
apply induction_on f

Result:
case h_C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (a : ZMod p), (frobenius (MvPolynomial σ (ZMod p)) p) (C a) = (expand p) (C a)

case h_add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 + q) = (expand p) (p_1 + q)

case h_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 * X n) = (expand p) (p_1 * X n)

Proof state:
case h_add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) p_1 + (frobenius (MvPolynomial σ (ZMod p)) p) q =
          (expand p) p_1 + (expand p) q

Tactic:
intro _ _ hf hg

Result:
case h_add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ q✝ : MvPolynomial σ (ZMod p)
hf : (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝
hg : (frobenius (MvPolynomial σ (ZMod p)) p) q✝ = (expand p) q✝
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) p✝ + (frobenius (MvPolynomial σ (ZMod p)) p) q✝ =
    (expand p) p✝ + (expand p) q✝

Proof state:
case h_C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
a : ZMod p
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) (C a) = (expand p) (C a)

Tactic:
rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]

Result:
no goals

Proof state:
case h_C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (a : ZMod p), (frobenius (MvPolynomial σ (ZMod p)) p) (C a) = (expand p) (C a)

Tactic:
intro a

Result:
case h_C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
a : ZMod p
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) (C a) = (expand p) (C a)

Proof state:
case h_add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ q✝ : MvPolynomial σ (ZMod p)
hf : (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝
hg : (frobenius (MvPolynomial σ (ZMod p)) p) q✝ = (expand p) q✝
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) p✝ + (frobenius (MvPolynomial σ (ZMod p)) p) q✝ =
    (expand p) p✝ + (expand p) q✝

Tactic:
rw [hf, hg]

Result:
no goals

Proof state:
case h_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 * X n) = (expand p) (p_1 * X n)

Tactic:
simp only [expand_X, map_mul]

Result:
case h_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) p_1 * (frobenius (MvPolynomial σ (ZMod p)) p) (X n) =
        (expand p) p_1 * X n ^ p

Proof state:
case h_add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 + q) = (expand p) (p_1 + q)

Tactic:
simp only [map_add]

Result:
case h_add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) p_1 + (frobenius (MvPolynomial σ (ZMod p)) p) q =
          (expand p) p_1 + (expand p) q

Proof state:
case h_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) p_1 * (frobenius (MvPolynomial σ (ZMod p)) p) (X n) =
        (expand p) p_1 * X n ^ p

Tactic:
intro _ _ hf

Result:
case h_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
n✝ : σ
hf : (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) p✝ * (frobenius (MvPolynomial σ (ZMod p)) p) (X n✝) = (expand p) p✝ * X n✝ ^ p

Proof state:
case h_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
n✝ : σ
hf : (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) p✝ * (frobenius (MvPolynomial σ (ZMod p)) p) (X n✝) = (expand p) p✝ * X n✝ ^ p

Tactic:
rw [hf, frobenius_def]

Result:
no goals