feat(ring_theory/laurent): coercion of R[x] to R((x)) lemmas (#11295)

Make the coercion be `simp`-normal as opposed to `(algebra_map _ _)`.
Also generalize `of_power_series Γ R (power_series.C R r) = hahn_series.C r` and similarly for `X` to be true for any `[ordered semiring Γ]`, not just `ℤ`.

src/ring_theory/laurent_series.lean

@@ -99,24 +99,36 @@ begin
     coe_power_series],
 end
 
+@[simp] lemma of_power_series_C (r : R) :
+  of_power_series ℤ R (power_series.C R r) = hahn_series.C r :=
+begin
+  ext n,
+  simp only [C, single_coeff, of_power_series_apply, ring_hom.coe_mk],
+  split_ifs with hn hn,
+  { rw [hn, ←int.coe_nat_zero],
+    convert @emb_domain_coeff _ _ _ _ _ _ _ _ 0,
+    simp },
+  { rw emb_domain_notin_image_support,
+    simp only [not_exists, set.mem_image, to_power_series_symm_apply_coeff, mem_support,
+               power_series.coeff_C],
+    intro,
+    simp [ne.symm hn] {contextual := tt} }
+end
+
 @[simp] lemma of_power_series_X :
   of_power_series ℤ R power_series.X = single 1 1 :=
 begin
   ext n,
-  cases n,
-  { rw [int.of_nat_eq_coe, ← int.nat_cast_eq_coe_nat, of_power_series_apply_coeff],
-    by_cases h1 : n = 1,
-    { simp [h1] },
-    { rw [power_series.coeff_X, single_coeff, if_neg h1, if_neg],
-      contrapose! h1,
-      rw [← nat.cast_one] at h1,
-      exact nat.cast_injective h1 } },
-  { rw [of_power_series_apply, emb_domain_notin_range, single_coeff_of_ne],
-    { dec_trivial },
-    rw [set.mem_range, not_exists],
-    intro m,
-    simp only [rel_embedding.coe_fn_mk, function.embedding.coe_fn_mk, int.nat_cast_eq_coe_nat],
-    dec_trivial }
+  simp only [single_coeff, of_power_series_apply, ring_hom.coe_mk],
+  split_ifs with hn hn,
+  { rw [hn, ←int.coe_nat_one],
+    convert @emb_domain_coeff _ _ _ _ _ _ _ _ 1,
+    simp },
+  { rw emb_domain_notin_image_support,
+    simp only [not_exists, set.mem_image, to_power_series_symm_apply_coeff, mem_support,
+               power_series.coeff_X],
+    intro,
+    simp [ne.symm hn] {contextual := tt} }
 end
 
 end semiring
@@ -181,3 +193,58 @@ is_localization.of_le (submonoid.powers (power_series.X : power_series K)) _
     hahn_series.of_power_series_injective hf)
 
 end laurent_series
+
+namespace polynomial
+
+section laurent_series
+
+variables [comm_semiring R] (p q : polynomial R)
+
+open polynomial laurent_series hahn_series
+
+lemma coe_laurent : (p : laurent_series R) = of_power_series ℤ R p := rfl
+
+@[norm_cast] lemma coe_coe : ((p : power_series R) : laurent_series R) = p := rfl
+
+@[simp] lemma coe_laurent_zero : ((0 : polynomial R) : laurent_series R) = 0 :=
+by rw [coe_laurent, coe_zero, _root_.map_zero]
+
+@[simp] lemma coe_laurent_one : ((1 : polynomial R) : laurent_series R) = 1 :=
+by rw [coe_laurent, coe_one, _root_.map_one]
+
+@[norm_cast] lemma coe_laurent_add : ((p + q : polynomial R) : laurent_series R) = p + q :=
+by rw [coe_laurent, coe_add, _root_.map_add, ←coe_laurent, ←coe_laurent]
+
+@[norm_cast] lemma coe_laurent_mul : ((p * q : polynomial R) : laurent_series R) = p * q :=
+by rw [coe_laurent, coe_mul, _root_.map_mul, ←coe_laurent, ←coe_laurent]
+
+@[norm_cast] lemma coeff_coe_laurent_coe (i : ℕ) :
+  ((p : polynomial R) : laurent_series R).coeff i = p.coeff i :=
+by rw [←coe_coe, coeff_coe_power_series, coeff_coe]
+
+lemma coeff_coe_laurent (i : ℤ) :
+  ((p : polynomial R) : laurent_series R).coeff i = if i < 0 then 0 else p.coeff i.nat_abs :=
+begin
+  cases i,
+  { rw [int.nat_abs_of_nat_core, int.of_nat_eq_coe, coeff_coe_laurent_coe,
+        if_neg (int.coe_nat_nonneg _).not_lt] },
+  { rw [coe_laurent, of_power_series_apply, emb_domain_notin_image_support,
+        if_pos (int.neg_succ_lt_zero _)],
+    simp only [not_exists, rel_embedding.coe_fn_mk, set.mem_image, not_and, coeff_coe,
+               function.embedding.coe_fn_mk, ne.def, to_power_series_symm_apply_coeff, mem_support,
+               int.nat_cast_eq_coe_nat, int.coe_nat_eq, implies_true_iff, not_false_iff] }
+end
+
+@[simp] lemma coe_laurent_C (r : R) : ((C r : polynomial R) : laurent_series R) = hahn_series.C r :=
+by rw [coe_laurent, coe_C, of_power_series_C]
+
+@[simp] lemma coe_laurent_X : ((X : polynomial R) : laurent_series R) = single 1 1 :=
+by rw [coe_laurent, coe_X, of_power_series_X]
+
+@[norm_cast] lemma coe_laurent_smul (r : R) :
+  ((r • p : polynomial R) : laurent_series R) = r • p :=
+by rw [smul_eq_C_mul, coe_laurent_mul, coe_laurent_C, C_mul_eq_smul]
+
+end laurent_series
+
+end polynomial