diff --git a/data/equiv/list.lean b/data/equiv/list.lean
index bfb13a3c15ff8..6810dbb7a1019 100644
--- a/data/equiv/list.lean
+++ b/data/equiv/list.lean
@@ -177,7 +177,7 @@ lemma raise_lower : ∀ {l n}, list.sorted (≤) (n :: l) → raise (lower l n)
            raise_lower (list.sorted_of_sorted_cons h)]
 
 lemma raise_chain : ∀ l n, list.chain (≤) n (raise l n)
-| []       n := list.chain.nil _ _
+| []       n := list.chain.nil
 | (m :: l) n := list.chain.cons (nat.le_add_left _ _) (raise_chain _ _)
 
 lemma raise_sorted : ∀ l n, list.sorted (≤) (raise l n)
@@ -217,7 +217,7 @@ lemma raise_lower' : ∀ {l n}, (∀ m ∈ l, n ≤ m) → list.sorted (<) l →
     (list.rel_of_sorted_cons h₂ : ∀ a ∈ l, m < a) (list.sorted_of_sorted_cons h₂)]
 
 lemma raise'_chain : ∀ l {m n}, m < n → list.chain (<) m (raise' l n)
-| []       m n h := list.chain.nil _ _
+| []       m n h := list.chain.nil
 | (a :: l) m n h := list.chain.cons
   (lt_of_lt_of_le h (nat.le_add_left _ _)) (raise'_chain _ (lt_succ_self _))
 
diff --git a/data/list/sigma.lean b/data/list/sigma.lean
index d8afc7da2c2a6..22365b7e449df 100644
--- a/data/list/sigma.lean
+++ b/data/list/sigma.lean
@@ -20,7 +20,7 @@ def nodupkeys (l : list (sigma β)) : Prop :=
 theorem nodupkeys_iff_pairwise {l} : nodupkeys l ↔
   pairwise (λ s s' : sigma β, s.1 ≠ s'.1) l := pairwise_map _
 
-@[simp] theorem nodupkeys_nil : @nodupkeys α β [] := pairwise.nil _
+@[simp] theorem nodupkeys_nil : @nodupkeys α β [] := pairwise.nil
 
 @[simp] theorem nodupkeys_cons {a : α} {b : β a} {l : list (sigma β)} :
   nodupkeys (⟨a, b⟩::l) ↔ (∀ b' : β a, sigma.mk a b' ∉ l) ∧ nodupkeys l :=