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)
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ↑(frobenius (MvPolynomial σ (ZMod p)) p) f = ↑(expand p) f
apply induction_on f
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_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)
intro a
no goals
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)
rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]
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
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)
simp only [AlgHom.map_add, RingHom.map_add]
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✝
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
intro _ _ hf hg
no goals
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✝
rw [hf, hg]
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
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)
simp only [expand_X, RingHom.map_mul, AlgHom.map_mul]
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
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
intro _ _ hf
no goals
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
rw [hf, frobenius_def]