diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean
index 133255888..5733d9a6a 100644
--- a/library/data/finset/basic.lean
+++ b/library/data/finset/basic.lean
@@ -213,7 +213,7 @@ decidable.by_cases
   (assume H : a ∈ s, by rewrite [card_insert_of_mem H]; apply le_succ)
   (assume H : a ∉ s, by rewrite [card_insert_of_not_mem H])
 
-lemma non_empty_of_card_succ {s : finset A} {n : nat} : card s = succ n → s ≠ ∅ :=
+lemma ne_empty_of_card_eq_succ {s : finset A} {n : nat} : card s = succ n → s ≠ ∅ :=
 by intros; substvars; contradiction
 
 protected theorem induction [recursor 6] {P : finset A → Prop}
diff --git a/library/data/finset/bigops.lean b/library/data/finset/bigops.lean
index 0536c7bc4..62185d3f4 100644
--- a/library/data/finset/bigops.lean
+++ b/library/data/finset/bigops.lean
@@ -126,7 +126,7 @@ section deceqA
     intros [H1, H2],
     rewrite [Union_insert, H2 _ !mem_insert],
     cases (decidable.em (s' = ∅)) with [seq, sne],
-      {rewrite [seq, Union_empty, union_empty] },
+      {rewrite [seq, Union_empty, union_empty]},
     have H3 : ∀ x, x ∈ s' → f x = t, from (λ x H', H2 x (mem_insert_of_mem _ H')),
     rewrite [IH sne H3, union_self]
   end