lint(multiset/pi): remove unused instance (#4526)

Removes an unused instance from `multiset/pi`



Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/data/finset/pi.lean

@@ -15,7 +15,14 @@ open multiset
 
 /-! ### pi -/
 section pi
-variables {α : Type*} {δ : α → Type*} [decidable_eq α]
+variables {α : Type*}
+
+/-- The empty dependent product function, defined on the empty set. The assumption `a ∈ ∅` is never
+satisfied. -/
+def pi.empty (β : α → Sort*) (a : α) (h : a ∈ (∅ : finset α)) : β a :=
+multiset.pi.empty β a h
+
+variables {δ : α → Type*} [decidable_eq α]
 
 /-- Given a finset `s` of `α` and for all `a : α` a finset `t a` of `δ a`, then one can define the
 finset `s.pi t` of all functions defined on elements of `s` taking values in `t a` for `a ∈ s`.
@@ -30,11 +37,6 @@ def pi (s : finset α) (t : Πa, finset (δ a)) : finset (Πa∈s, δ a) :=
   f ∈ s.pi t ↔ (∀a (h : a ∈ s), f a h ∈ t a) :=
 mem_pi _ _ _
 
-/-- The empty dependent product function, defined on the emptyset. The assumption `a ∈ ∅` is never
-satisfied. -/
-def pi.empty (β : α → Sort*) (a : α) (h : a ∈ (∅ : finset α)) : β a :=
-multiset.pi.empty β a h
-
 /-- Given a function `f` defined on a finset `s`, define a new function on the finset `s ∪ {a}`,
 equal to `f` on `s` and sending `a` to a given value `b`. This function is denoted
 `s.pi.cons a b f`. If `a` already belongs to `s`, the new function takes the value `b` at `a`

src/data/multiset/pi.lean

@@ -12,23 +12,27 @@ import data.multiset.nodup
 namespace multiset
 
 section pi
-variables {α : Type*} [decidable_eq α] {δ : α → Type*}
+variables {α : Type*}
 open function
 
-/-- Given `δ : α → Type*`, a multiset `m` and a term `a`, as well as a term `b : δ a` and a function `f`
-such that `f a' : δ a'` for all `a'` in `m`, `pi.cons m a b f` is a function `g` such that
-`g a'' : δ a''` for all `a''` in `a :: m`. -/
+/-- Given `δ : α → Type*`, `pi.empty δ` is the trivial dependent function out of the empty
+multiset. -/
+def pi.empty (δ : α → Type*) : (Πa∈(0:multiset α), δ a) .
+
+variables [decidable_eq α] {δ : α → Type*}
+
+/-- Given `δ : α → Type*`, a multiset `m` and a term `a`, as well as a term `b : δ a` and a
+function `f` such that `f a' : δ a'` for all `a'` in `m`, `pi.cons m a b f` is a function `g` such
+that `g a'' : δ a''` for all `a''` in `a :: m`. -/
 def pi.cons (m : multiset α) (a : α) (b : δ a) (f : Πa∈m, δ a) : Πa'∈a::m, δ a' :=
 λa' ha', if h : a' = a then eq.rec b h.symm else f a' $ (mem_cons.1 ha').resolve_left h
 
-/-- Given `δ : α → Type*`, `pi.empty δ` is the trivial dependent function out of the empty multiset. -/
-def pi.empty (δ : α → Type*) : (Πa∈(0:multiset α), δ a) .
-
 lemma pi.cons_same {m : multiset α} {a : α} {b : δ a} {f : Πa∈m, δ a} (h : a ∈ a :: m) :
   pi.cons m a b f a h = b :=
 dif_pos rfl
 
-lemma pi.cons_ne {m : multiset α} {a a' : α} {b : δ a} {f : Πa∈m, δ a} (h' : a' ∈ a :: m) (h : a' ≠ a) :
+lemma pi.cons_ne {m : multiset α} {a a' : α} {b : δ a} {f : Πa∈m, δ a}
+  (h' : a' ∈ a :: m) (h : a' ≠ a) :
   pi.cons m a b f a' h' = f a' ((mem_cons.1 h').resolve_left h) :=
 dif_neg h