no goals
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ map f (T R 0) = T S 0
simp only [T_zero, Polynomial.map_one]
no goals
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ map f (T R 1) = T S 1
simp only [T_one, map_X]
no goals
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ map f (T R (n + 2)) = T S (n + 2)
simp only [T_add_two, Polynomial.map_mul, Polynomial.map_sub, map_X, Polynomial.map_add,
  Polynomial.map_one, Polynomial.map_ofNat, map_T f (n + 1), map_T f n]