case zero
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
⊢ map (frobenius R p ^ Nat.zero) (↑(expand R (p ^ Nat.zero)) f) = f ^ p ^ Nat.zero

case succ
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n✝ : ℕ
n_ih : map (frobenius R p ^ n✝) (↑(expand R (p ^ n✝)) f) = f ^ p ^ n✝
⊢ map (frobenius R p ^ Nat.succ n✝) (↑(expand R (p ^ Nat.succ n✝)) f) = f ^ p ^ Nat.succ n✝
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n : ℕ
⊢ map (frobenius R p ^ n) (↑(expand R (p ^ n)) f) = f ^ p ^ n
induction' n with _ n_ih
case succ
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n✝ : ℕ
n_ih : map (frobenius R p ^ n✝) (↑(expand R (p ^ n✝)) f) = f ^ p ^ n✝
⊢ f ^ p ^ Nat.succ n✝ = map (frobenius R p ^ Nat.succ n✝) (↑(expand R (p ^ Nat.succ n✝)) f)
case succ
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n✝ : ℕ
n_ih : map (frobenius R p ^ n✝) (↑(expand R (p ^ n✝)) f) = f ^ p ^ n✝
⊢ map (frobenius R p ^ Nat.succ n✝) (↑(expand R (p ^ Nat.succ n✝)) f) = f ^ p ^ Nat.succ n✝
symm
no goals
case succ
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n✝ : ℕ
n_ih : map (frobenius R p ^ n✝) (↑(expand R (p ^ n✝)) f) = f ^ p ^ n✝
⊢ f ^ p ^ Nat.succ n✝ = map (frobenius R p ^ Nat.succ n✝) (↑(expand R (p ^ Nat.succ n✝)) f)
rw [pow_succ', pow_mul, ← n_ih, ← expand_char, pow_succ, RingHom.mul_def, ← map_map, mul_comm,
  expand_mul, ← map_expand]
no goals
case zero
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
⊢ map (frobenius R p ^ Nat.zero) (↑(expand R (p ^ Nat.zero)) f) = f ^ p ^ Nat.zero
simp [RingHom.one_def]