case refine'_1
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f a b : R[X]
ha : map (frobenius R p) (↑(expand R p) a) = a ^ p
hb : map (frobenius R p) (↑(expand R p) b) = b ^ p
⊢ map (frobenius R p) (↑(expand R p) (a + b)) = (a + b) ^ p

case refine'_2
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 : ℕ
a : R
⊢ map (frobenius R p) (↑(expand R p) (↑(monomial n) a)) = ↑(monomial n) a ^ p
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) (↑(expand R p) f) = f ^ p
refine' f.induction_on' (fun a b ha hb => _) fun n a => _
no goals
case refine'_1
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f a b : R[X]
ha : map (frobenius R p) (↑(expand R p) a) = a ^ p
hb : map (frobenius R p) (↑(expand R p) b) = b ^ p
⊢ map (frobenius R p) (↑(expand R p) (a + b)) = (a + b) ^ p
rw [AlgHom.map_add, Polynomial.map_add, ha, hb, add_pow_char]
case refine'_2
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 : ℕ
a : R
⊢ ↑C (a ^ p) * X ^ (n * p) = ↑C (a ^ p) * (X ^ n) ^ p
case refine'_2
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 : ℕ
a : R
⊢ map (frobenius R p) (↑(expand R p) (↑(monomial n) a)) = ↑(monomial n) a ^ p
rw [expand_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
  mul_pow, ← C.map_pow, frobenius_def]
no goals
case refine'_2
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 : ℕ
a : R
⊢ ↑C (a ^ p) * X ^ (n * p) = ↑C (a ^ p) * (X ^ n) ^ p
ring