chore(ring_theory/polynomial/symmetric): golf proofs (#14866)

src/data/finset/basic.lean

@@ -2619,6 +2619,9 @@ rfl
   e.finset_congr.trans (e'.finset_congr) = (e.trans e').finset_congr :=
 by { ext, simp [-finset.mem_map, -equiv.trans_to_embedding] }
 
+lemma finset_congr_to_embedding (e : α ≃ β) :
+  e.finset_congr.to_embedding = (finset.map_embedding e.to_embedding).to_embedding := rfl
+
 /--
 Inhabited types are equivalent to `option β` for some `β` by identifying `default α` with `none`.
 -/

src/data/finset/powerset.lean

@@ -246,5 +246,12 @@ finset.powerset_len_empty _ (lt_add_of_pos_right (finset.card s) hi)
   (s.powerset_len i).val.map finset.val = s.1.powerset_len i :=
 by simp [finset.powerset_len, map_pmap, pmap_eq_map, map_id']
 
+theorem powerset_len_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : finset α) :
+  powerset_len n (s.map f) = (powerset_len n s).map (map_embedding f).to_embedding :=
+eq_of_veq $ multiset.map_injective (@eq_of_veq _) $
+  by simp_rw [map_val_val_powerset_len, map_val, multiset.map_map, function.comp,
+      rel_embedding.coe_fn_to_embedding, map_embedding_apply, map_val, ←multiset.map_map _ val,
+      map_val_val_powerset_len, multiset.powerset_len_map]
+
 end powerset_len
 end finset

src/data/fintype/basic.lean

@@ -182,6 +182,12 @@ eq_univ_of_forall $ hf.forall.2 $ λ _, mem_image_of_mem _ $ mem_univ _
 
 end boolean_algebra
 
+lemma map_univ_of_surjective [fintype β] {f : β ↪ α} (hf : surjective f) : univ.map f = univ :=
+eq_univ_of_forall $ hf.forall.2 $ λ _, mem_map_of_mem _ $ mem_univ _
+
+@[simp] lemma map_univ_equiv [fintype β] (f : β ≃ α) : univ.map f.to_embedding = univ :=
+map_univ_of_surjective f.surjective
+
 @[simp] lemma univ_inter [decidable_eq α] (s : finset α) :
   univ ∩ s = s := ext $ λ a, by simp
 

src/ring_theory/polynomial/symmetric.lean

@@ -141,49 +141,23 @@ end
 lemma esymm_eq_sum_monomial (n : ℕ) : esymm σ R n =
   ∑ t in powerset_len n univ, monomial (∑ i in t, finsupp.single i 1) 1 :=
 begin
-  refine sum_congr rfl (λ x hx, _),
-  rw monic_monomial_eq,
-  rw finsupp.prod_pow,
-  rw ← prod_subset (λ y _, finset.mem_univ y : x ⊆ univ) (λ y _ hy, _),
-  { refine prod_congr rfl (λ x' hx', _),
-    convert (pow_one _).symm,
-    convert (finsupp.apply_add_hom x' : (σ →₀ ℕ) →+ ℕ).map_sum _ x,
-    classical,
-    simp [finsupp.single_apply, finset.filter_eq', apply_ite, apply_ite finset.card],
-    rw if_pos, exact hx', },
-  { convert pow_zero _,
-    convert (finsupp.apply_add_hom y : (σ →₀ ℕ) →+ ℕ).map_sum _ x,
-    classical,
-    simp [finsupp.single_apply, finset.filter_eq', apply_ite, apply_ite finset.card],
-    rw if_neg, exact hy }
+  simp_rw monomial_sum_one,
+  refl,
 end
 
 @[simp] lemma esymm_zero : esymm σ R 0 = 1 :=
 by simp only [esymm, powerset_len_zero, sum_singleton, prod_empty]
 
 lemma map_esymm (n : ℕ) (f : R →+* S) : map f (esymm σ R n) = esymm σ S n :=
-begin
-  rw [esymm, (map f).map_sum],
-  refine sum_congr rfl (λ x hx, _),
-  rw (map f).map_prod,
-  simp,
-end
+by simp_rw [esymm, map_sum, map_prod, map_X]
 
 lemma rename_esymm (n : ℕ) (e : σ ≃ τ) : rename e (esymm σ R n) = esymm τ R n :=
-begin
-  rw [esymm_eq_sum_subtype, esymm_eq_sum_subtype, (rename ⇑e).map_sum],
-  let e' : {s : finset σ // s.card = n} ≃ {s : finset τ // s.card = n} :=
-    equiv.subtype_equiv (equiv.finset_congr e) (by simp),
-  rw ← equiv.sum_comp e'.symm,
-  apply fintype.sum_congr,
-  intro,
-  calc _ = (∏ i in (e'.symm a : finset σ), (rename e) (X i)) : (rename e).map_prod _ _
-     ... = (∏ i in (a : finset τ), (rename e) (X (e.symm i))) : prod_map (a : finset τ) _ _
-     ... = _ : _,
-  apply finset.prod_congr rfl,
-  intros,
-  simp,
-end
+calc rename e (esymm σ R n)
+     = ∑ x in powerset_len n univ, ∏ i in x, X (e i)
+       : by simp_rw [esymm, map_sum, map_prod, rename_X]
+ ... = ∑ t in powerset_len n (univ.map e.to_embedding), ∏ i in t, X i
+       : by simp [finset.powerset_len_map, -finset.map_univ_equiv]
+ ... = ∑ t in powerset_len n univ, ∏ i in t, X i : by rw finset.map_univ_equiv
 
 lemma esymm_is_symmetric (n : ℕ) : is_symmetric (esymm σ R n) :=
 by { intro, rw rename_esymm }