chore(data/finsupp/defs): redefine finsupp.single as pi.single (#17356)

This also brings it in line with `dfinsupp.single`.

Note that the two are still not defeq due to different decidability instances, but things are least more consistent now.

In order to make some proofs still unify, this makes some type arguments explicit to `constant_coeff_C` and `constant_coeff_X`. These lemmas should have had these as explicit arguments anyway, as the type can't be inferred from the other arguments.

Author: eric-wieser

src/data/finsupp/defs.lean

@@ -202,17 +202,17 @@ variables [has_zero M] {a a' : α} {b : M}
 
 /-- `single a b` is the finitely supported function with value `b` at `a` and zero otherwise. -/
 def single (a : α) (b : M) : α →₀ M :=
-⟨if b = 0 then ∅ else {a}, λ a', if a = a' then b else 0, λ a', begin
-  by_cases hb : b = 0; by_cases a = a';
-    simp only [hb, h, if_pos, if_false, mem_singleton],
-  { exact ⟨false.elim, λ H, H rfl⟩ },
-  { exact ⟨false.elim, λ H, H rfl⟩ },
-  { exact ⟨λ _, hb, λ _, rfl⟩ },
-  { exact ⟨λ H _, h H.symm, λ H, (H rfl).elim⟩ }
+⟨if b = 0 then ∅ else {a}, pi.single a b, λ a', begin
+  obtain rfl | hb := eq_or_ne b 0,
+  { simp },
+  rw [if_neg hb, mem_singleton],
+  obtain rfl | ha := eq_or_ne a' a,
+  { simp [hb] },
+  simp [pi.single_eq_of_ne', ha],
 end⟩
 
 lemma single_apply [decidable (a = a')] : single a b a' = if a = a' then b else 0 :=
-by convert rfl
+by { simp_rw [@eq_comm _ a a'], convert pi.single_apply _ _ _, }
 
 lemma single_apply_left {f : α → β} (hf : function.injective f)
   (x z : α) (y : M) :
@@ -223,10 +223,10 @@ lemma single_eq_indicator : ⇑(single a b) = set.indicator {a} (λ _, b) :=
 by { ext, simp [single_apply, set.indicator, @eq_comm _ a] }
 
 @[simp] lemma single_eq_same : (single a b : α →₀ M) a = b :=
-if_pos rfl
+pi.single_eq_same a b
 
 @[simp] lemma single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ M) a' = 0 :=
-if_neg h
+pi.single_eq_of_ne' h _
 
 lemma single_eq_update [decidable_eq α] (a : α) (b : M) : ⇑(single a b) = function.update 0 a b :=
 by rw [single_eq_indicator, ← set.piecewise_eq_indicator, set.piecewise_singleton]
@@ -577,7 +577,7 @@ support_on_finset_subset
 
 @[simp] lemma map_range_single {f : M → N} {hf : f 0 = 0} {a : α} {b : M} :
   map_range f hf (single a b) = single a (f b) :=
-ext $ λ a', show f (ite _ _ _) = ite _ _ _, by split_ifs; [refl, exact hf]
+ext $ λ a', by simpa only [single_eq_pi_single] using pi.apply_single _ (λ _, hf) a _ a'
 
 lemma support_map_range_of_injective
   {e : M → N} (he0 : e 0 = 0) (f : ι →₀ M) (he : function.injective e) :

src/data/mv_polynomial/basic.lean

@@ -657,15 +657,15 @@ def constant_coeff : mv_polynomial σ R →+* R :=
 
 lemma constant_coeff_eq : (constant_coeff : mv_polynomial σ R → R) = coeff 0 := rfl
 
-@[simp]
-lemma constant_coeff_C (r : R) :
-  constant_coeff (C r : mv_polynomial σ R) = r :=
+variables (σ)
+@[simp] lemma constant_coeff_C (r : R) : constant_coeff (C r : mv_polynomial σ R) = r :=
 by simp [constant_coeff_eq]
+variables {σ}
 
-@[simp]
-lemma constant_coeff_X (i : σ) :
-  constant_coeff (X i : mv_polynomial σ R) = 0 :=
+variables (R)
+@[simp] lemma constant_coeff_X (i : σ) : constant_coeff (X i : mv_polynomial σ R) = 0 :=
 by simp [constant_coeff_eq]
+variables {R}
 
 lemma constant_coeff_monomial [decidable_eq σ] (d : σ →₀ ℕ) (r : R) :
   constant_coeff (monomial d r) = if d = 0 then r else 0 :=
@@ -675,7 +675,7 @@ variables (σ R)
 
 @[simp] lemma constant_coeff_comp_C :
   constant_coeff.comp (C : R →+* mv_polynomial σ R) = ring_hom.id R :=
-by { ext, apply constant_coeff_C }
+by { ext x, exact constant_coeff_C σ x }
 
 @[simp] lemma constant_coeff_comp_algebra_map :
   constant_coeff.comp (algebra_map R (mv_polynomial σ R)) = ring_hom.id R :=

src/data/mv_polynomial/variables.lean

@@ -487,8 +487,7 @@ begin
   congr,
   ext,
   simp only [single, nat.one_ne_zero, add_right_eq_self, add_right_embedding_apply, coe_mk,
-             pi.add_apply, comp_app, ite_eq_right_iff, finsupp.coe_add],
-  cc,
+             pi.add_apply, comp_app, ite_eq_right_iff, finsupp.coe_add, pi.single_eq_of_ne h],
 end
 
 /- TODO in the following we have equality iff f ≠ 0 -/

src/linear_algebra/direct_sum/finsupp.lean

@@ -57,7 +57,7 @@ begin
     { intros g₁ g₂ hg₁ hg₂, simp [tmul_add, hg₁, hg₂], },
     { intros k' n,
       simp only [finsupp_tensor_finsupp_single],
-      simp only [finsupp.single, finsupp.coe_mk],
+      simp only [finsupp.single_apply],
       -- split_ifs; finish can close the goal from here
       by_cases h1 : (i', k') = (i, k),
       { simp only [prod.mk.inj_iff] at h1, simp [h1] },
@@ -89,6 +89,6 @@ by simp [finsupp_tensor_finsupp']
 @[simp] lemma finsupp_tensor_finsupp'_single_tmul_single (a : α) (b : β) (r₁ r₂ : S) :
   finsupp_tensor_finsupp' S α β (finsupp.single a r₁ ⊗ₜ[S] finsupp.single b r₂) =
     finsupp.single (a, b) (r₁ * r₂) :=
-by { ext ⟨a', b'⟩, simp [finsupp.single, ite_and] }
+by { ext ⟨a', b'⟩, simp [finsupp.single_apply, ite_and] }
 
 end tensor_product

src/linear_algebra/matrix/basis.lean

@@ -72,7 +72,7 @@ by { ext M i j, refl, }
 begin
   rw basis.to_matrix,
   ext i j,
-  simp [basis.equiv_fun, matrix.one_apply, finsupp.single, eq_comm]
+  simp [basis.equiv_fun, matrix.one_apply, finsupp.single_apply, eq_comm]
 end
 
 lemma to_matrix_update [decidable_eq ι'] (x : M) :

src/linear_algebra/matrix/to_lin.lean

@@ -444,7 +444,7 @@ end
 lemma linear_map.to_matrix_id : linear_map.to_matrix v₁ v₁ id = 1 :=
 begin
   ext i j,
-  simp [linear_map.to_matrix_apply, matrix.one_apply, finsupp.single, eq_comm]
+  simp [linear_map.to_matrix_apply, matrix.one_apply, finsupp.single_apply, eq_comm]
 end
 
 lemma linear_map.to_matrix_one : linear_map.to_matrix v₁ v₁ 1 = 1 :=

src/ring_theory/polynomial/basic.lean

@@ -745,9 +745,9 @@ begin
 end
 
 lemma prime_C_iff : prime (C r : mv_polynomial σ R) ↔ prime r :=
-⟨ comap_prime C constant_coeff constant_coeff_C,
+⟨ comap_prime C constant_coeff (constant_coeff_C _),
   λ hr, ⟨ λ h, hr.1 $ by { rw [← C_inj, h], simp },
-    λ h, hr.2.1 $ by { rw ← constant_coeff_C r, exact h.map _ },
+    λ h, hr.2.1 $ by { rw ← constant_coeff_C _ r, exact h.map _ },
     λ a b hd, begin
       obtain ⟨s,a',b',rfl,rfl⟩ := exists_finset_rename₂ a b,
       rw ← algebra_map_eq at hd, have : algebra_map R _ r ∣ a' * b',