refactor(data/list/basic,...): more explicit args (#4866)

This makes the `p` in most lemmas involving the following functions explicit, following the usual explicitness conventions:
- `list.filter`,
- `list.countp`,
- `list.take_while`,
- `multiset.filter`,
- `multiset.countp`,
- `finset.filter`

src/algebra/big_operators/basic.lean

@@ -335,7 +335,7 @@ by rw [←prod_sdiff h]; simp only [this, prod_const_one, one_mul]
 @[to_additive]
 lemma prod_filter_of_ne {p : α → Prop} [decidable_pred p] (hp : ∀ x ∈ s, f x ≠ 1 → p x) :
   (∏ x in (s.filter p), f x) = (∏ x in s, f x) :=
-prod_subset (filter_subset _) $ λ x,
+prod_subset (filter_subset _ _) $ λ x,
   by { classical, rw [not_imp_comm, mem_filter], exact λ h₁ h₂, ⟨h₁, hp _ h₁ h₂⟩ }
 
 -- If we use `[decidable_eq β]` here, some rewrites fail because they find a wrong `decidable`
@@ -352,7 +352,7 @@ calc (∏ a in s.filter p, f a) = ∏ a in s.filter p, if p a then f a else 1 :
     prod_congr rfl (assume a h, by rw [if_pos (mem_filter.1 h).2])
   ... = ∏ a in s, if p a then f a else 1 :
     begin
-      refine prod_subset (filter_subset s) (assume x hs h, _),
+      refine prod_subset (filter_subset _ s) (assume x hs h, _),
       rw [mem_filter, not_and] at h,
       exact if_neg (h hs)
     end

src/algebra/monoid_algebra.lean

@@ -208,7 +208,7 @@ calc (f * g) x = (∑ a₁ in f.support, ∑ a₂ in g.support, F (a₁, a₂))
   (finset.sum_filter _ _).symm
 ... = ∑ p in s.filter (λ p : G × G, p.1 ∈ f.support ∧ p.2 ∈ g.support), f p.1 * g p.2 :
   sum_congr (by { ext, simp only [mem_filter, mem_product, hs, and_comm] }) (λ _ _, rfl)
-... = ∑ p in s, f p.1 * g p.2 : sum_subset (filter_subset _) $ λ p hps hp,
+... = ∑ p in s, f p.1 * g p.2 : sum_subset (filter_subset _ _) $ λ p hps hp,
   begin
     simp only [mem_filter, mem_support_iff, not_and, not_not] at hp ⊢,
     by_cases h1 : f p.1 = 0,

src/analysis/convex/basic.lean

@@ -977,7 +977,7 @@ end
 
 lemma finset.center_mass_filter_ne_zero :
   (t.filter (λ i, w i ≠ 0)).center_mass w z = t.center_mass w z :=
-finset.center_mass_subset z (filter_subset _) $ λ i hit hit',
+finset.center_mass_subset z (filter_subset _ _) $ λ i hit hit',
 by simpa only [hit, mem_filter, true_and, ne.def, not_not] using hit'
 
 variable {z}

src/analysis/convex/caratheodory.lean

@@ -52,7 +52,7 @@ begin
     obtain ⟨x, hx, hgx⟩ : ∃ x ∈ t, 0 < g x := gpos,
     exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩, },
   have hg   : 0 < g i₀ := by { rw mem_filter at mem, exact mem.2 },
-  have hi₀  : i₀ ∈ t   := filter_subset _ mem,
+  have hi₀  : i₀ ∈ t   := filter_subset _ _ mem,
   let  k    : E → ℝ    := λ z, f z - (f i₀ / g i₀) * g z,
   have hk   : k i₀ = 0 := by field_simp [k, ne_of_gt hg],
   have ksum : ∑ e in t.erase i₀, k e = 1,
@@ -69,7 +69,7 @@ begin
       exact w _ hes, },
     { calc _ ≤ 0   : mul_nonpos_of_nonneg_of_nonpos _ _ -- prove two goals below
          ... ≤ f e : fpos e het,
-      { apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset t) mem)) (le_of_lt hg) },
+      { apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg) },
       { simpa only [mem_filter, het, true_and, not_lt] using hes }, } },
   { simp only [subtype.coe_mk, center_mass_eq_of_sum_1 _ id ksum, id],
     calc ∑ e in t.erase i₀, k e • e = ∑ e in t, k e • e :
@@ -225,11 +225,11 @@ begin
       exact multiset.mem_filter_of_mem m (lt_of_le_of_ne (pos z m) (ne.symm nz)), },
     { intros _ _ _ _ _ _ a, exact a, },
     { intros z m nz,
-      exact ⟨z, mem_of_subset (filter_subset t) m, nz, rfl⟩, },
+      exact ⟨z, mem_of_subset (filter_subset _ t) m, nz, rfl⟩, },
     { intros, refl, }, },
   refine ⟨t', _, _, f, ⟨_, _, _⟩⟩,
-  { exact subset.trans (filter_subset t) w, },
-  { exact le_trans (card_le_of_subset (filter_subset t)) b, },
+  { exact subset.trans (filter_subset _ t) w, },
+  { exact le_trans (card_le_of_subset (filter_subset _ t)) b, },
   { exact λ y H, (mem_filter.mp H).right, },
   { exact t'sum, },
   { convert center using 1,
@@ -243,6 +243,6 @@ begin
       exact multiset.mem_filter_of_mem m (lt_of_le_of_ne (pos z m) (ne.symm nz')), },
     { intros _ _ _ _ _ _ a, exact a, },
     { intros z m nz,
-      exact ⟨z, mem_of_subset (filter_subset t) m, nz, rfl⟩, },
+      exact ⟨z, mem_of_subset (filter_subset _ t) m, nz, rfl⟩, },
     { intros, refl, }, },
 end

src/combinatorics/partition.lean

@@ -78,7 +78,7 @@ def of_sums (n : ℕ) (l : multiset ℕ) (hl : l.sum = n) : partition n :=
   parts_pos := λ i hi, nat.pos_of_ne_zero $ by apply of_mem_filter hi,
   parts_sum :=
   begin
-    have lt : l.filter (= 0) + l.filter (≠ 0) = l := filter_add_not l,
+    have lt : l.filter (= 0) + l.filter (≠ 0) = l := filter_add_not _ l,
     apply_fun multiset.sum at lt,
     have lz : (l.filter (= 0)).sum = 0,
     { rw multiset.sum_eq_zero_iff,

src/data/finset/basic.lean

@@ -973,24 +973,27 @@ end decidable_pi_exists
 
 /-! ### filter -/
 section filter
-variables {p q : α → Prop} [decidable_pred p] [decidable_pred q]
+variables (p q : α → Prop) [decidable_pred p] [decidable_pred q]
 
 /-- `filter p s` is the set of elements of `s` that satisfy `p`. -/
-def filter (p : α → Prop) [decidable_pred p] (s : finset α) : finset α :=
+def filter (s : finset α) : finset α :=
 ⟨_, nodup_filter p s.2⟩
 
 @[simp] theorem filter_val (s : finset α) : (filter p s).1 = s.1.filter p := rfl
 
-@[simp] theorem mem_filter {s : finset α} {a : α} : a ∈ s.filter p ↔ a ∈ s ∧ p a := mem_filter
+@[simp] theorem filter_subset (s : finset α) : s.filter p ⊆ s := filter_subset _ _
+
+variable {p}
 
-@[simp] theorem filter_subset (s : finset α) : s.filter p ⊆ s := filter_subset _
+@[simp] theorem mem_filter {s : finset α} {a : α} : a ∈ s.filter p ↔ a ∈ s ∧ p a := mem_filter
 
 theorem filter_ssubset {s : finset α} : s.filter p ⊂ s ↔ ∃ x ∈ s, ¬ p x :=
 ⟨λ h, let ⟨x, hs, hp⟩ := set.exists_of_ssubset h in ⟨x, hs, mt (λ hp, mem_filter.2 ⟨hs, hp⟩) hp⟩,
-  λ ⟨x, hs, hp⟩, ⟨s.filter_subset, λ h, hp (mem_filter.1 (h hs)).2⟩⟩
+  λ ⟨x, hs, hp⟩, ⟨s.filter_subset _, λ h, hp (mem_filter.1 (h hs)).2⟩⟩
 
-theorem filter_filter (s : finset α) :
-  (s.filter p).filter q = s.filter (λa, p a ∧ q a) :=
+variable (p)
+
+theorem filter_filter (s : finset α) : (s.filter p).filter q = s.filter (λa, p a ∧ q a) :=
 ext $ assume a, by simp only [mem_filter, and_comm, and.left_comm]
 
 lemma filter_true {s : finset α} [h : decidable_pred (λ _, true)] :
@@ -1000,6 +1003,8 @@ by ext; simp
 @[simp] theorem filter_false {h} (s : finset α) : @filter α (λa, false) h s = ∅ :=
 ext $ assume a, by simp only [mem_filter, and_false]; refl
 
+variables {p q}
+
 /-- If all elements of a `finset` satisfy the predicate `p`, `s.filter p` is `s`. -/
 @[simp] lemma filter_true_of_mem {s : finset α} (h : ∀ x ∈ s, p x) : s.filter p = s :=
 ext $ λ x, ⟨λ h, (mem_filter.1 h).1, λ hx, mem_filter.2 ⟨hx, h x hx⟩⟩
@@ -1011,8 +1016,9 @@ eq_empty_of_forall_not_mem (by simpa)
 lemma filter_congr {s : finset α} (H : ∀ x ∈ s, p x ↔ q x) : filter p s = filter q s :=
 eq_of_veq $ filter_congr H
 
-lemma filter_empty : filter p ∅ = ∅ :=
-subset_empty.1 $ filter_subset _
+variables (p q)
+
+lemma filter_empty : filter p ∅ = ∅ := subset_empty.1 $ filter_subset _ _
 
 lemma filter_subset_filter {s t : finset α} (h : s ⊆ t) : s.filter p ⊆ t.filter p :=
 assume a ha, mem_filter.2 ⟨h (mem_filter.1 ha).1, (mem_filter.1 ha).2⟩
@@ -1025,26 +1031,24 @@ by { classical, ext x, simp, split_ifs with h; by_cases h' : x = a; simp [h, h']
 
 variable [decidable_eq α]
 
-theorem filter_union (s₁ s₂ : finset α) :
-  (s₁ ∪ s₂).filter p = s₁.filter p ∪ s₂.filter p :=
+theorem filter_union (s₁ s₂ : finset α) : (s₁ ∪ s₂).filter p = s₁.filter p ∪ s₂.filter p :=
 ext $ λ _, by simp only [mem_filter, mem_union, or_and_distrib_right]
 
-theorem filter_union_right (p q : α → Prop) [decidable_pred p] [decidable_pred q] (s : finset α) :
-  s.filter p ∪ s.filter q = s.filter (λx, p x ∨ q x) :=
+theorem filter_union_right (s : finset α) : s.filter p ∪ s.filter q = s.filter (λx, p x ∨ q x) :=
 ext $ λ x, by simp only [mem_filter, mem_union, and_or_distrib_left.symm]
 
 lemma filter_mem_eq_inter {s t : finset α} [Π i, decidable (i ∈ t)] :
   s.filter (λ i, i ∈ t) = s ∩ t :=
 ext $ λ i, by rw [mem_filter, mem_inter]
 
-theorem filter_inter {s t : finset α} : filter p s ∩ t = filter p (s ∩ t) :=
+theorem filter_inter (s t : finset α) : filter p s ∩ t = filter p (s ∩ t) :=
 by { ext, simp only [mem_inter, mem_filter, and.right_comm] }
 
-theorem inter_filter {s t : finset α} : s ∩ filter p t = filter p (s ∩ t) :=
+theorem inter_filter (s t : finset α) : s ∩ filter p t = filter p (s ∩ t) :=
 by rw [inter_comm, filter_inter, inter_comm]
 
 theorem filter_insert (a : α) (s : finset α) :
-  filter p (insert a s) = if p a then insert a (filter p s) else (filter p s) :=
+  filter p (insert a s) = if p a then insert a (filter p s) else filter p s :=
 by { ext x, simp, split_ifs with h; by_cases h' : x = a; simp [h, h'] }
 
 theorem filter_or [decidable_pred (λ a, p a ∨ q a)] (s : finset α) :
@@ -1075,7 +1079,7 @@ by { simp [subset.antisymm_iff,sdiff_subset_self],
 
 theorem filter_union_filter_neg_eq [decidable_pred (λ a, ¬ p a)]
   (s : finset α) : s.filter p ∪ s.filter (λa, ¬ p a) = s :=
-by simp only [filter_not, union_sdiff_of_subset (filter_subset s)]
+by simp only [filter_not, union_sdiff_of_subset (filter_subset p s)]
 
 theorem filter_inter_filter_neg_eq (s : finset α) : s.filter p ∩ s.filter (λa, ¬ p a) = ∅ :=
 by simp only [filter_not, inter_sdiff_self]
@@ -1120,7 +1124,7 @@ end classical
 -- This is not a good simp lemma, as it would prevent `finset.mem_filter` from firing
 -- on, e.g. `x ∈ s.filter(eq b)`.
 lemma filter_eq [decidable_eq β] (s : finset β) (b : β) :
-  s.filter(eq b) = ite (b ∈ s) {b} ∅ :=
+  s.filter (eq b) = ite (b ∈ s) {b} ∅ :=
 begin
   split_ifs,
   { ext,
@@ -2142,7 +2146,7 @@ by split; simp [disjoint_left] {contextual := tt}
 lemma disjoint_filter_filter {s t : finset α} {p q : α → Prop} [decidable_pred p]
   [decidable_pred q] :
   (disjoint s t) → disjoint (s.filter p) (t.filter q) :=
-disjoint.mono (filter_subset _) (filter_subset _)
+disjoint.mono (filter_subset _ _) (filter_subset _ _)
 
 lemma disjoint_iff_disjoint_coe {α : Type*} {a b : finset α} [decidable_eq α] :
   disjoint a b ↔ disjoint (↑a : set α) (↑b : set α) :=

src/data/finsupp/basic.lean

@@ -312,7 +312,7 @@ rfl
 
 @[simp] lemma support_on_finset_subset {s : finset α} {f : α → M} {hf} :
   (on_finset s f hf).support ⊆ s :=
-filter_subset _
+filter_subset _ _
 
 @[simp] lemma mem_support_on_finset
   {s : finset α} {f : α → M} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) {a : α} :

src/data/fintype/basic.lean

@@ -798,7 +798,7 @@ if h : ∃ a, β a then ⟨{⟨h.fst, h.snd⟩}, λ ⟨_, _⟩, by simp⟩ else
 instance set.fintype [fintype α] : fintype (set α) :=
 ⟨(@finset.univ α _).powerset.map ⟨coe, coe_injective⟩, λ s, begin
   classical, refine mem_map.2 ⟨finset.univ.filter s, mem_powerset.2 (subset_univ _), _⟩,
-  apply (coe_filter _).trans, rw [coe_univ, set.sep_univ], refl
+  apply (coe_filter _ _).trans, rw [coe_univ, set.sep_univ], refl
 end⟩
 
 instance pfun_fintype (p : Prop) [decidable p] (α : p → Type*)

src/data/list/basic.lean

@@ -2784,13 +2784,14 @@ end
 theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a ∈ l, ¬p a :=
 by simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]
 
+variable (p)
 theorem filter_sublist_filter {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ :=
 filter_map_eq_filter p ▸ s.filter_map _
 
 theorem filter_of_map (f : β → α) (l) : filter p (map f l) = map f (filter (p ∘ f) l) :=
 by rw [← filter_map_eq_map, filter_filter_map, filter_map_filter]; refl
 
-@[simp] theorem filter_filter {q} [decidable_pred q] : ∀ l,
+@[simp] theorem filter_filter (q) [decidable_pred q] : ∀ l,
   filter p (filter q l) = filter (λ a, p a ∧ q a) l
 | [] := rfl
 | (a :: l) := by by_cases hp : p a; by_cases hq : q a; simp only [hp, hq, filter, if_true, if_false,
@@ -2804,21 +2805,19 @@ by convert filter_eq_self.2 (λ _ _, trivial)
   @filter α (λ _, false) h l = [] :=
 by convert filter_eq_nil.2 (λ _ _, id)
 
-@[simp] theorem span_eq_take_drop (p : α → Prop) [decidable_pred p] :
-  ∀ (l : list α), span p l = (take_while p l, drop_while p l)
+@[simp] theorem span_eq_take_drop : ∀ (l : list α), span p l = (take_while p l, drop_while p l)
 | []     := rfl
 | (a::l) :=
     if pa : p a then by simp only [span, if_pos pa, span_eq_take_drop l, take_while, drop_while]
     else by simp only [span, take_while, drop_while, if_neg pa]
 
-@[simp] theorem take_while_append_drop (p : α → Prop) [decidable_pred p] :
-  ∀ (l : list α), take_while p l ++ drop_while p l = l
+@[simp] theorem take_while_append_drop : ∀ (l : list α), take_while p l ++ drop_while p l = l
 | []     := rfl
 | (a::l) := if pa : p a then by rw [take_while, drop_while, if_pos pa, if_pos pa, cons_append,
       take_while_append_drop l]
     else by rw [take_while, drop_while, if_neg pa, if_neg pa, nil_append]
 
-@[simp] theorem countp_nil (p : α → Prop) [decidable_pred p] : countp p [] = 0 := rfl
+@[simp] theorem countp_nil : countp p [] = 0 := rfl
 
 @[simp] theorem countp_cons_of_pos {a : α} (l) (pa : p a) : countp p (a::l) = countp p l + 1 :=
 if_pos pa
@@ -2829,7 +2828,7 @@ if_neg pa
 theorem countp_eq_length_filter (l) : countp p l = length (filter p l) :=
 by induction l with x l ih; [refl, by_cases (p x)];
   [simp only [filter_cons_of_pos _ h, countp, ih, if_pos h],
-   simp only [countp_cons_of_neg _ h, ih, filter_cons_of_neg _ h]]; refl
+   simp only [countp_cons_of_neg _ _ h, ih, filter_cons_of_neg _ h]]; refl
 
 local attribute [simp] countp_eq_length_filter
 
@@ -2840,7 +2839,7 @@ theorem countp_pos {l} : 0 < countp p l ↔ ∃ a ∈ l, p a :=
 by simp only [countp_eq_length_filter, length_pos_iff_exists_mem, mem_filter, exists_prop]
 
 theorem countp_le_of_sublist {l₁ l₂} (s : l₁ <+ l₂) : countp p l₁ ≤ countp p l₂ :=
-by simpa only [countp_eq_length_filter] using length_le_of_sublist (filter_sublist_filter s)
+by simpa only [countp_eq_length_filter] using length_le_of_sublist (filter_sublist_filter p s)
 
 @[simp] theorem countp_filter {q} [decidable_pred q] (l : list α) :
   countp p (filter q l) = countp (λ a, p a ∧ q a) l :=
@@ -2874,15 +2873,15 @@ theorem count_tail : Π (l : list α) (a : α) (h : 0 < l.length),
 | (_ :: _) a h := by { rw [count_cons], split_ifs; simp }
 
 theorem count_le_of_sublist (a : α) {l₁ l₂} : l₁ <+ l₂ → count a l₁ ≤ count a l₂ :=
-countp_le_of_sublist
+countp_le_of_sublist _
 
 theorem count_le_count_cons (a b : α) (l : list α) : count a l ≤ count a (b :: l) :=
 count_le_of_sublist _ (sublist_cons _ _)
 
 theorem count_singleton (a : α) : count a [a] = 1 := if_pos rfl
 
 @[simp] theorem count_append (a : α) : ∀ l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
-countp_append
+countp_append _
 
 theorem count_concat (a : α) (l : list α) : count a (concat l a) = succ (count a l) :=
 by simp [-add_comm]

src/data/list/perm.lean

@@ -359,7 +359,7 @@ by rw [countp_eq_length_filter, countp_eq_length_filter];
 
 theorem subperm.countp_le (p : α → Prop) [decidable_pred p]
   {l₁ l₂ : list α} : l₁ <+~ l₂ → countp p l₁ ≤ countp p l₂
-| ⟨l, p', s⟩ := p'.countp_eq p ▸ countp_le_of_sublist s
+| ⟨l, p', s⟩ := p'.countp_eq p ▸ countp_le_of_sublist p s
 
 theorem perm.count_eq [decidable_eq α] {l₁ l₂ : list α}
   (p : l₁ ~ l₂) (a) : count a l₁ = count a l₂ :=