Theorem: Polynomial.coeff_baseChange_apply (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : S[X]
p : ℕ
⊢ ((baseChange φ) f).coeff p = φ (f.coeff p)
Tactic:
rw [baseChange, AlgHom.coe_mk, coe_eval₂RingHom]
State after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : S[X]
p : ℕ
⊢ (eval₂ (C.comp ↑φ) X f).coeff p = φ (f.coeff p)

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : S[X]
p : ℕ
⊢ (eval₂ (C.comp ↑φ) X f).coeff p = φ (f.coeff p)
Tactic:
induction f using Polynomial.induction_on with
| h_C r =>
  simp only [eval₂_C, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, coeff_C,
    apply_ite φ, map_zero]
| h_add f g hf hg => simp only [eval₂_add, coeff_add, hf, hg, map_add]
| h_monomial n r _ =>
  simp only [eval₂_mul, eval₂_C, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
    eval₂_X_pow, coeff_C_mul, _root_.map_mul, coeff_X_pow, apply_ite φ, _root_.map_one, map_zero]
State after:
no goals

State before:
case h_C
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p : ℕ
r : S
⊢ (eval₂ (C.comp ↑φ) X (C r)).coeff p = φ ((C r).coeff p)
Tactic:
simp only [eval₂_C, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, coeff_C,
  apply_ite φ, map_zero]
State after:
no goals

State before:
case h_add
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p : ℕ
f g : S[X]
hf : (eval₂ (C.comp ↑φ) X f).coeff p = φ (f.coeff p)
hg : (eval₂ (C.comp ↑φ) X g).coeff p = φ (g.coeff p)
⊢ (eval₂ (C.comp ↑φ) X (f + g)).coeff p = φ ((f + g).coeff p)
Tactic:
simp only [eval₂_add, coeff_add, hf, hg, map_add]
State after:
no goals

State before:
case h_monomial
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p n : ℕ
r : S
a✝ : (eval₂ (C.comp ↑φ) X (C r * X ^ n)).coeff p = φ ((C r * X ^ n).coeff p)
⊢ (eval₂ (C.comp ↑φ) X (C r * X ^ (n + 1))).coeff p = φ ((C r * X ^ (n + 1)).coeff p)
Tactic:
simp only [eval₂_mul, eval₂_C, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
  eval₂_X_pow, coeff_C_mul, _root_.map_mul, coeff_X_pow, apply_ite φ, _root_.map_one, map_zero]
State after:
no goals