feat(ring_theory/power_series): teach simp to simplify more coercions…

… of polynomials to power series (#11287)

So that simp can prove that the polynomial `5 * X^2 + X + 1` coerced to a power series is the same thing with the power series generator `X`. Likewise for `mv_power_series`.

src/ring_theory/power_series/basic.lean

@@ -780,6 +780,14 @@ by simp only [coeff_coe, mv_power_series.coeff_mul, coeff_mul]
   ((C a : mv_polynomial σ R) : mv_power_series σ R) = mv_power_series.C σ R a :=
 coe_monomial _ _
 
+@[simp, norm_cast] lemma coe_bit0 :
+  ((bit0 φ : mv_polynomial σ R) : mv_power_series σ R) = bit0 (φ : mv_power_series σ R) :=
+coe_add _ _
+
+@[simp, norm_cast] lemma coe_bit1 :
+  ((bit1 φ : mv_polynomial σ R) : mv_power_series σ R) = bit1 (φ : mv_power_series σ R) :=
+by rw [bit1, bit1, coe_add, coe_one, coe_bit0]
+
 @[simp, norm_cast] lemma coe_X (s : σ) :
   ((X s : mv_polynomial σ R) : mv_power_series σ R) = mv_power_series.X s :=
 coe_monomial _ _
@@ -811,6 +819,10 @@ def coe_to_mv_power_series.ring_hom : mv_polynomial σ R →+* mv_power_series 
   map_add' := coe_add,
   map_mul' := coe_mul }
 
+@[simp, norm_cast] lemma coe_pow (n : ℕ) :
+  ((φ ^ n : mv_polynomial σ R) : mv_power_series σ R) = (φ : mv_power_series σ R) ^ n :=
+coe_to_mv_power_series.ring_hom.map_pow _ _
+
 variables (φ ψ)
 
 @[simp] lemma coe_to_mv_power_series.ring_hom_apply : coe_to_mv_power_series.ring_hom φ = φ := rfl
@@ -1811,6 +1823,14 @@ begin
   rwa power_series.monomial_zero_eq_C_apply at this,
 end
 
+@[simp, norm_cast] lemma coe_bit0 :
+  ((bit0 φ : polynomial R) : power_series R) = bit0 (φ : power_series R) :=
+coe_add φ φ
+
+@[simp, norm_cast] lemma coe_bit1 :
+  ((bit1 φ : polynomial R) : power_series R) = bit1 (φ : power_series R) :=
+by rw [bit1, bit1, coe_add, coe_one, coe_bit0]
+
 @[simp, norm_cast] lemma coe_X :
   ((X : polynomial R) : power_series R) = power_series.X :=
 coe_monomial _ _
@@ -1846,6 +1866,10 @@ def coe_to_power_series.ring_hom : polynomial R →+* power_series R :=
 
 @[simp] lemma coe_to_power_series.ring_hom_apply : coe_to_power_series.ring_hom φ = φ := rfl
 
+@[simp, norm_cast] lemma coe_pow (n : ℕ):
+  ((φ ^ n : polynomial R) : power_series R) = (φ : power_series R) ^ n :=
+coe_to_power_series.ring_hom.map_pow _ _
+
 variables (A : Type*) [semiring A] [algebra R A]
 
 /--