chore(data/finsupp/basic): make arguments explicit (#14551)

This follow the pattern that arguments to an `=` lemma should be explicit if they're not implied by other arguments.

src/algebra/monoid_algebra/grading.lean

@@ -95,7 +95,7 @@ instance grade_by.graded_monoid [add_monoid M] [add_monoid ι] [comm_semiring R]
     { rw [H , finsupp.single_zero] at h,
       exfalso,
       exact h },
-    { rw [finsupp.support_single_ne_zero H, finset.mem_singleton] at h,
+    { rw [finsupp.support_single_ne_zero _ H, finset.mem_singleton] at h,
       rw [h, add_monoid_hom.map_zero] }
   end,
   mul_mem := λ i j a b ha hb c hc, begin
@@ -156,12 +156,12 @@ begin
     exact add_monoid_hom.map_zero _ },
   { intros m b y hmy hb ih hmby,
     have : disjoint (finsupp.single m b).support y.support,
-    { simpa only [finsupp.support_single_ne_zero hb, finset.disjoint_singleton_left] },
+    { simpa only [finsupp.support_single_ne_zero _ hb, finset.disjoint_singleton_left] },
     rw [mem_grade_by_iff, finsupp.support_add_eq this, finset.coe_union,
       set.union_subset_iff] at hmby,
     cases hmby with h1 h2,
     have : f m = i,
-    { rwa [finsupp.support_single_ne_zero hb, finset.coe_singleton,
+    { rwa [finsupp.support_single_ne_zero _ hb, finset.coe_singleton,
         set.singleton_subset_iff] at h1 },
     subst this,
     simp only [alg_hom.map_add, submodule.coe_mk, decompose_aux_single f m],

src/data/finsupp/basic.lean

@@ -232,13 +232,13 @@ if_pos rfl
 @[simp] lemma single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ M) a' = 0 :=
 if_neg h
 
-lemma single_eq_update [decidable_eq α] : ⇑(single a b) = function.update 0 a b :=
+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]
 
-lemma single_eq_pi_single [decidable_eq α] : ⇑(single a b) = pi.single a b :=
-single_eq_update
+lemma single_eq_pi_single [decidable_eq α] (a : α) (b : M) : ⇑(single a b) = pi.single a b :=
+single_eq_update a b
 
-@[simp] lemma single_zero : (single a 0 : α →₀ M) = 0 :=
+@[simp] lemma single_zero (a : α) : (single a 0 : α →₀ M) = 0 :=
 coe_fn_injective $ by simpa only [single_eq_update, coe_zero]
   using function.update_eq_self a (0 : α → M)
 
@@ -252,7 +252,7 @@ begin
   { rw [zero_apply, single_apply, if_t_t], },
 end
 
-lemma support_single_ne_zero (hb : b ≠ 0) : (single a b).support = {a} :=
+lemma support_single_ne_zero (a : α) (hb : b ≠ 0) : (single a b).support = {a} :=
 if_neg hb
 
 lemma support_single_subset : (single a b).support ⊆ {a} :=
@@ -318,11 +318,11 @@ lemma single_left_inj (h : b ≠ 0) : single a b = single a' b ↔ a = a' :=
 
 lemma support_single_ne_bot (i : α) (h : b ≠ 0) :
   (single i b).support ≠ ⊥ :=
-by simpa only [support_single_ne_zero h] using singleton_ne_empty _
+by simpa only [support_single_ne_zero _ h] using singleton_ne_empty _
 
 lemma support_single_disjoint [decidable_eq α] {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} :
   disjoint (single i b).support (single j b').support ↔ i ≠ j :=
-by rw [support_single_ne_zero hb, support_single_ne_zero hb', disjoint_singleton]
+by rw [support_single_ne_zero _ hb, support_single_ne_zero _ hb', disjoint_singleton]
 
 @[simp] lemma single_eq_zero : single a b = 0 ↔ b = 0 :=
 by simp [ext_iff, single_eq_indicator]
@@ -354,12 +354,12 @@ by rw [unique_ext_iff, unique.eq_default a, unique.eq_default a', single_eq_same
 lemma support_eq_singleton {f : α →₀ M} {a : α} :
   f.support = {a} ↔ f a ≠ 0 ∧ f = single a (f a) :=
 ⟨λ h, ⟨mem_support_iff.1 $ h.symm ▸ finset.mem_singleton_self a,
-  eq_single_iff.2 ⟨subset_of_eq h, rfl⟩⟩, λ h, h.2.symm ▸ support_single_ne_zero h.1⟩
+  eq_single_iff.2 ⟨subset_of_eq h, rfl⟩⟩, λ h, h.2.symm ▸ support_single_ne_zero _ h.1⟩
 
 lemma support_eq_singleton' {f : α →₀ M} {a : α} :
   f.support = {a} ↔ ∃ b ≠ 0, f = single a b :=
 ⟨λ h, let h := support_eq_singleton.1 h in ⟨_, h.1, h.2⟩,
-  λ ⟨b, hb, hf⟩, hf.symm ▸ support_single_ne_zero hb⟩
+  λ ⟨b, hb, hf⟩, hf.symm ▸ support_single_ne_zero _ hb⟩
 
 lemma card_support_eq_one {f : α →₀ M} : card f.support = 1 ↔ ∃ a, f a ≠ 0 ∧ f = single a (f a) :=
 by simp only [card_eq_one, support_eq_singleton]
@@ -616,7 +616,7 @@ lemma single_of_emb_domain_single
   ∃ x, l = single x b ∧ f x = a :=
 begin
   have h_map_support : finset.map f (l.support) = {a},
-    by rw [←support_emb_domain, h, support_single_ne_zero hb]; refl,
+    by rw [←support_emb_domain, h, support_single_ne_zero _ hb]; refl,
   have ha : a ∈ finset.map f (l.support),
     by simp only [h_map_support, finset.mem_singleton],
   rcases finset.mem_map.1 ha with ⟨c, hc₁, hc₂⟩,
@@ -752,7 +752,8 @@ f.prod_of_support_subset (subset_univ _) g (λ x _, h x)
 lemma prod_single_index {a : α} {b : M} {h : α → M → N} (h_zero : h a 0 = 1) :
   (single a b).prod h = h a b :=
 calc (single a b).prod h = ∏ x in {a}, h x (single a b x) :
-  prod_of_support_subset _ support_single_subset h $ λ x hx, (mem_singleton.1 hx).symm ▸ h_zero
+  prod_of_support_subset _ support_single_subset h $
+    λ x hx, (mem_singleton.1 hx).symm ▸ h_zero
 ... = h a b : by simp
 
 @[to_additive]
@@ -873,7 +874,7 @@ le_antisymm support_zip_with $ assume a ha,
     by simp only [mem_support_iff, not_not] at *;
     simpa only [add_apply, this, zero_add])
 
-@[simp] lemma single_add {a : α} {b₁ b₂ : M} : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
+@[simp] lemma single_add (a : α) (b₁ b₂ : M) : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
 ext $ assume a',
 begin
   by_cases h : a = a',
@@ -889,7 +890,7 @@ fun_like.coe_injective.add_zero_class _ coe_zero coe_add
 See `finsupp.lsingle` for the stronger version as a linear map.
 -/
 @[simps] def single_add_hom (a : α) : M →+ α →₀ M :=
-⟨single a, single_zero, λ _ _, single_add⟩
+⟨single a, single_zero a, single_add a⟩
 
 /-- Evaluation of a function `f : α →₀ M` at a point as an additive monoid homomorphism.
 
@@ -1124,7 +1125,7 @@ fun_like.coe_injective.add_comm_group _ coe_zero coe_add coe_neg coe_sub (λ _ _
 
 lemma single_multiset_sum [add_comm_monoid M] (s : multiset M) (a : α) :
   single a s.sum = (s.map (single a)).sum :=
-multiset.induction_on s single_zero $ λ a s ih,
+multiset.induction_on s (single_zero _) $ λ a s ih,
 by rw [multiset.sum_cons, single_add, ih, multiset.map_cons, multiset.sum_cons]
 
 lemma single_finset_sum [add_comm_monoid M] (s : finset ι) (f : ι → M) (a : α) :
@@ -1584,15 +1585,15 @@ lemma map_domain_comp {f : α → β} {g : β → γ} :
   map_domain (g ∘ f) v = map_domain g (map_domain f v) :=
 begin
   refine ((sum_sum_index _ _).trans _).symm,
-  { intros, exact single_zero },
-  { intros, exact single_add },
+  { intro, exact single_zero _ },
+  { intro, exact single_add _ },
   refine sum_congr (λ _ _, sum_single_index _),
-  { exact single_zero }
+  { exact single_zero _ }
 end
 
 @[simp]
 lemma map_domain_single {f : α → β} {a : α} {b : M} : map_domain f (single a b) = single (f a) b :=
-sum_single_index single_zero
+sum_single_index $ single_zero _
 
 @[simp] lemma map_domain_zero {f : α → β} : map_domain f (0 : α →₀ M) = (0 : β →₀ M) :=
 sum_zero_index
@@ -1602,7 +1603,7 @@ lemma map_domain_congr {f g : α → β} (h : ∀x∈v.support, f x = g x) :
 finset.sum_congr rfl $ λ _ H, by simp only [h _ H]
 
 lemma map_domain_add {f : α → β} : map_domain f (v₁ + v₂) = map_domain f v₁ + map_domain f v₂ :=
-sum_add_index' (λ _, single_zero) (λ _ _ _, single_add)
+sum_add_index' (λ _, single_zero _) (λ _, single_add _)
 
 @[simp] lemma map_domain_equiv_apply {f : α ≃ β} (x : α →₀ M) (a : β) :
   map_domain f x a = x (f.symm a) :=
@@ -1838,8 +1839,8 @@ begin
   rcases eq_or_ne m 0 with rfl | hm,
   { simp only [single_zero, comap_domain_zero] },
   { rw [eq_single_iff, comap_domain_apply, comap_domain_support, ← finset.coe_subset, coe_preimage,
-      support_single_ne_zero hm, coe_singleton, coe_singleton, single_eq_same],
-    rw [support_single_ne_zero hm, coe_singleton] at hif,
+      support_single_ne_zero _ hm, coe_singleton, coe_singleton, single_eq_same],
+    rw [support_single_ne_zero _ hm, coe_singleton] at hif,
     exact ⟨λ x hx, hif hx rfl hx, rfl⟩ }
 end
 
@@ -2185,10 +2186,10 @@ ext $ λ _, rfl
   (v - v').subtype_domain p = v.subtype_domain p - v'.subtype_domain p :=
 ext $ λ _, rfl
 
-@[simp] lemma single_neg {a : α} {b : G} : single a (-b) = -single a b :=
+@[simp] lemma single_neg (a : α) (b : G) : single a (-b) = -single a b :=
 (single_add_hom a : G →+ _).map_neg b
 
-@[simp] lemma single_sub {a : α} {b₁ b₂ : G} : single a (b₁ - b₂) = single a b₁ - single a b₂ :=
+@[simp] lemma single_sub (a : α) (b₁ b₂ : G) : single a (b₁ - b₂) = single a b₁ - single a b₂ :=
 (single_add_hom a : G →+ _).map_sub b₁ b₂
 
 @[simp] lemma erase_neg (a : α) (f : α →₀ G) : erase a (-f) = -erase a f :=

src/data/finsupp/multiset.lean

@@ -89,7 +89,7 @@ begin
   { rw [to_multiset_zero, multiset.to_finset_zero, support_zero] },
   { assume a n f ha hn ih,
     rw [to_multiset_add, multiset.to_finset_add, ih, to_multiset_single, support_add_eq,
-      support_single_ne_zero hn, multiset.to_finset_nsmul _ _ hn, multiset.to_finset_singleton],
+      support_single_ne_zero _ hn, multiset.to_finset_nsmul _ _ hn, multiset.to_finset_singleton],
     refine disjoint.mono_left support_single_subset _,
     rwa [finset.disjoint_singleton_left] }
 end

src/data/mv_polynomial/basic.lean

@@ -165,7 +165,7 @@ lemma C_apply : (C a : mv_polynomial σ R) = monomial 0 a := rfl
 lemma C_mul_monomial : C a * monomial s a' = monomial s (a * a') :=
 by simp [C_apply, monomial, single_mul_single]
 
-@[simp] lemma C_add : (C (a + a') : mv_polynomial σ R) = C a + C a' := single_add
+@[simp] lemma C_add : (C (a + a') : mv_polynomial σ R) = C a + C a' := single_add _ _ _
 
 @[simp] lemma C_mul : (C (a * a') : mv_polynomial σ R) = C a * C a' := C_mul_monomial.symm
 
@@ -241,7 +241,7 @@ lemma monomial_eq_C_mul_X {s : σ} {a : R} {n : ℕ} :
 by rw [← zero_add (single s n), monomial_add_single, C_apply]
 
 @[simp] lemma monomial_zero {s : σ →₀ ℕ} : monomial s (0 : R) = 0 :=
-single_zero
+single_zero _
 
 @[simp] lemma monomial_zero' : (monomial (0 : σ →₀ ℕ) : R → mv_polynomial σ R) = C := rfl
 

src/data/mv_polynomial/variables.lean

@@ -252,7 +252,8 @@ by rw [vars, degrees_monomial_eq _ _ h, finsupp.to_finset_to_multiset]
 by rw [vars, degrees_C, multiset.to_finset_zero]
 
 @[simp] lemma vars_X [nontrivial R] : (X n : mv_polynomial σ R).vars = {n} :=
-by rw [X, vars_monomial (@one_ne_zero R _ _), finsupp.support_single_ne_zero (one_ne_zero : 1 ≠ 0)]
+by rw [X, vars_monomial (@one_ne_zero R _ _),
+  finsupp.support_single_ne_zero _ (one_ne_zero : 1 ≠ 0)]
 
 lemma mem_vars (i : σ) :
   i ∈ p.vars ↔ ∃ (d : σ →₀ ℕ) (H : d ∈ p.support), i ∈ d.support :=
@@ -408,7 +409,7 @@ by simp [vars, degrees_map_of_injective _ hf]
 
 lemma vars_monomial_single (i : σ) {e : ℕ} {r : R} (he : e ≠ 0) (hr : r ≠ 0) :
   (monomial (finsupp.single i e) r).vars = {i} :=
-by rw [vars_monomial hr, finsupp.support_single_ne_zero he]
+by rw [vars_monomial hr, finsupp.support_single_ne_zero _ he]
 
 lemma vars_eq_support_bUnion_support : p.vars = p.support.bUnion finsupp.support :=
 by { ext i, rw [mem_vars, finset.mem_bUnion] }

src/data/polynomial/basic.lean

@@ -537,7 +537,7 @@ by rw [←one_smul R p, ←h, zero_smul]
 section fewnomials
 
 lemma support_monomial (n) {a : R} (H : a ≠ 0) : (monomial n a).support = singleton n :=
-by rw [←of_finsupp_single, support, finsupp.support_single_ne_zero H]
+by rw [←of_finsupp_single, support, finsupp.support_single_ne_zero _ H]
 
 lemma support_monomial' (n) (a : R) : (monomial n a).support ⊆ singleton n :=
 by { rw [←of_finsupp_single, support], exact finsupp.support_single_subset }

src/group_theory/free_abelian_group_finsupp.lean

@@ -156,7 +156,7 @@ by { rw [support, finsupp.not_mem_support_iff], exact iff.rfl }
 by simp only [support, finsupp.support_zero, add_monoid_hom.map_zero]
 
 @[simp] lemma support_of (x : X) : support (of x) = {x} :=
-by simp only [support, to_finsupp_of, finsupp.support_single_ne_zero (one_ne_zero)]
+by simp only [support, to_finsupp_of, finsupp.support_single_ne_zero _ one_ne_zero]
 
 @[simp] lemma support_neg (a : free_abelian_group X) : support (-a) = support a :=
 by simp only [support, add_monoid_hom.map_neg, finsupp.support_neg]

src/linear_algebra/dimension.lean

@@ -599,7 +599,7 @@ begin
       rw hJ at this,
       replace : v.repr (v i) ∈ (finsupp.supported R R (⋃ j, S j)) := this trivial,
       rw [v.repr_self, finsupp.mem_supported,
-        finsupp.support_single_ne_zero one_ne_zero] at this,
+        finsupp.support_single_ne_zero _ one_ne_zero] at this,
       { subst b,
         rcases mem_Union.1 (this (finset.mem_singleton_self _)) with ⟨j, hj⟩,
         exact mem_Union.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩ },

src/linear_algebra/std_basis.lean

@@ -144,13 +144,7 @@ end
 
 lemma std_basis_eq_single {a : R} :
   (λ (i : ι), (std_basis R (λ _ : ι, R) i) a) = λ (i : ι), (finsupp.single i a) :=
-begin
-  ext i j,
-  rw [std_basis_apply, finsupp.single_apply],
-  split_ifs,
-  { rw [h, function.update_same] },
-  { rw [function.update_noteq (ne.symm h)], refl },
-end
+funext $ λ i, (finsupp.single_eq_pi_single i a).symm
 
 end linear_map
 

src/ring_theory/finiteness.lean

@@ -707,7 +707,7 @@ lemma of'_mem_span [nontrivial R] {m : M} {S : set M} :
 begin
   refine ⟨λ h, _, λ h, submodule.subset_span $ set.mem_image_of_mem (of R M) h⟩,
   rw [of', ← finsupp.supported_eq_span_single, finsupp.mem_supported,
-    finsupp.support_single_ne_zero (@one_ne_zero R _ (by apply_instance))] at h,
+    finsupp.support_single_ne_zero _ (@one_ne_zero R _ (by apply_instance))] at h,
   simpa using h
 end
 
@@ -863,7 +863,7 @@ lemma of_mem_span_of_iff [nontrivial R] {m : M} {S : set M} :
 begin
   refine ⟨λ h, _, λ h, submodule.subset_span $ set.mem_image_of_mem (of R M) h⟩,
   rw [of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, finsupp.mem_supported,
-    finsupp.support_single_ne_zero (@one_ne_zero R _ (by apply_instance))] at h,
+    finsupp.support_single_ne_zero _ (@one_ne_zero R _ (by apply_instance))] at h,
   simpa using h
 end
 

src/ring_theory/polynomial/homogeneous.lean

@@ -152,7 +152,7 @@ lemma is_homogeneous_X (i : σ) :
   is_homogeneous (X i : mv_polynomial σ R) 1 :=
 begin
   apply is_homogeneous_monomial,
-  simp only [finsupp.support_single_ne_zero one_ne_zero, finset.sum_singleton],
+  simp only [finsupp.support_single_ne_zero _ one_ne_zero, finset.sum_singleton],
   exact finsupp.single_eq_same
 end
 

src/ring_theory/polynomial/symmetric.lean

@@ -196,12 +196,12 @@ begin
   simp only [← single_eq_monomial],
   convert finsupp.support_sum_eq_bUnion (powerset_len n (univ : finset σ)) _,
   intros s t hst d,
-  simp only [finsupp.support_single_ne_zero one_ne_zero, and_imp, inf_eq_inter, mem_inter,
+  simp only [finsupp.support_single_ne_zero _ one_ne_zero, and_imp, inf_eq_inter, mem_inter,
              mem_singleton],
   rintro h rfl,
   have := congr_arg finsupp.support h,
   rw [finsupp.support_sum_eq_bUnion, finsupp.support_sum_eq_bUnion] at this,
-  { simp only [finsupp.support_single_ne_zero one_ne_zero, bUnion_singleton_eq_self] at this,
+  { simp only [finsupp.support_single_ne_zero _ one_ne_zero, bUnion_singleton_eq_self] at this,
     exact absurd this hst.symm },
   all_goals { intros x y, simp [finsupp.support_single_disjoint] }
 end
@@ -213,7 +213,7 @@ begin
   rw support_esymm'',
   congr,
   funext,
-  exact finsupp.support_single_ne_zero one_ne_zero
+  exact finsupp.support_single_ne_zero _ one_ne_zero
 end
 
 lemma support_esymm (n : ℕ) [decidable_eq σ] [nontrivial R] :