diff --git a/library/data/finset/card.lean b/library/data/finset/card.lean
index a30d49e97..1d2da0426 100644
--- a/library/data/finset/card.lean
+++ b/library/data/finset/card.lean
@@ -77,9 +77,9 @@ finset.induction_on s
     have H4 : f a ∉ image f t,
       proof
         assume H5 : f a ∈ image f t,
-        obtain x (H6 : x ∈ t ∧ f x = f a), from exists_of_mem_image H5,
-        have H7 : x = a, from H1 (mem_insert_of_mem _ (and.left H6)) !mem_insert (and.right H6),
-        show false, from H (H7 ▸ and.left H6)
+        obtain x (H6l : x ∈ t) (H6r : f x = f a), from exists_of_mem_image H5,
+        have H7 : x = a, from H1 (mem_insert_of_mem _ H6l) !mem_insert H6r,
+        show false, from H (H7 ▸ H6l)
       qed,
     calc
       card (image f (insert a t)) = card (insert (f a) (image f t)) : image_insert
diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean
index 351aa204a..3a771740d 100644
--- a/library/data/finset/comb.lean
+++ b/library/data/finset/comb.lean
@@ -41,32 +41,31 @@ quot.induction_on s
 theorem mem_image_iff (f : A → B) {s : finset A} {y : B} : y ∈ image f s ↔ ∃x, x ∈ s ∧ f x = y :=
 iff.intro exists_of_mem_image
   (assume H,
-    obtain x (H1 : x ∈ s ∧ f x = y), from H,
-    mem_image_of_mem_of_eq (and.left H1) (and.right H1))
+    obtain x (H₁ : x ∈ s) (H₂ : f x = y), from H,
+    mem_image_of_mem_of_eq H₁ H₂)
 
 theorem mem_image_eq (f : A → B) {s : finset A} {y : B} : y ∈ image f s = ∃x, x ∈ s ∧ f x = y :=
 propext (mem_image_iff f)
 
 theorem mem_image_of_mem_image_of_subset {f : A → B} {s t : finset A} {y : B}
     (H1 : y ∈ image f s) (H2 : s ⊆ t) : y ∈ image f t :=
-obtain x (H3: x ∈ s ∧ f x = y), from exists_of_mem_image H1,
-have H4 : x ∈ t, from mem_of_subset_of_mem H2 (and.left H3),
-show y ∈ image f t, from mem_image_of_mem_of_eq H4 (and.right H3)
+obtain x (H3: x ∈ s) (H4 : f x = y), from exists_of_mem_image H1,
+have H5 : x ∈ t, from mem_of_subset_of_mem H2 H3,
+show y ∈ image f t, from mem_image_of_mem_of_eq H5 H4
 
 theorem image_insert [h' : decidable_eq A] (f : A → B) (s : finset A) (a : A) :
   image f (insert a s) = insert (f a) (image f s) :=
 ext (take y, iff.intro
   (assume H : y ∈ image f (insert a s),
-    obtain x (H1 : x ∈ insert a s ∧ f x = y), from exists_of_mem_image H,
-    have H2 : x = a ∨ x ∈ s, from eq_or_mem_of_mem_insert (and.left H1),
+    obtain x (H1l : x ∈ insert a s) (H1r :f x = y), from exists_of_mem_image H,
+    have H2 : x = a ∨ x ∈ s, from eq_or_mem_of_mem_insert H1l,
     or.elim H2
       (assume H3 : x = a,
-        have H4 : f a = y, from eq.subst H3 (and.right H1),
+        have H4 : f a = y, from eq.subst H3 H1r,
         show y ∈ insert (f a) (image f s), from eq.subst H4 !mem_insert)
       (assume H3 : x ∈ s,
-        have H4 : f x = y, from and.right H1,
         have H5 : f x ∈ image f s, from mem_image_of_mem f H3,
-        show y ∈ insert (f a) (image f s), from eq.subst H4 (mem_insert_of_mem _ H5)))
+        show y ∈ insert (f a) (image f s), from eq.subst H1r (mem_insert_of_mem _ H5)))
   (assume H : y ∈ insert (f a) (image f s),
     have H1 : y = f a ∨ y ∈ image f s, from eq_or_mem_of_mem_insert H,
     or.elim H1
@@ -237,8 +236,8 @@ theorem any_of_mem {p : A → Prop} {s : finset A} {a : A} : a ∈ s → p a →
 quot.induction_on s (λ l H1 H2, list.any_of_mem H1 H2)
 
 theorem any_of_exists {p : A → Prop} {s : finset A} (H : ∃a, a ∈ s ∧ p a) : any s p :=
-obtain a H', from H,
-any_of_mem (and.left H') (and.right H')
+obtain a H₁ H₂, from H,
+any_of_mem H₁ H₂
 
 theorem any_iff_exists (p : A → Prop) (s : finset A) : any s p ↔ (∃a, a ∈ s ∧ p a) :=
 iff.intro exists_of_any any_of_exists
@@ -249,8 +248,8 @@ any_of_mem (mem_insert a s) H
 
 theorem any_of_insert_right [h : decidable_eq A] {p : A → Prop} {s : finset A} (a : A) (H : any s p) :
   any (insert a s) p :=
-obtain b (H' : b ∈ s ∧ p b), from exists_of_any H,
-any_of_mem (mem_insert_of_mem a (and.left H')) (and.right H')
+obtain b (H₁ : b ∈ s) (H₂ : p b), from exists_of_any H,
+any_of_mem (mem_insert_of_mem a H₁) H₂
 
 definition decidable_any [instance] (p : A → Prop) [h : decidable_pred p] (s : finset A) :
   decidable (any s p) :=
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index d0f3d239a..e44c10124 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -48,8 +48,8 @@ theorem exists_of_mem_map {A B : Type} {f : A → B} {b : B} :
                 (assume H1 : b = f c,
                   exists.intro c (and.intro !mem_cons (eq.symm H1)))
                 (assume H1 : b ∈ map f l,
-                  obtain a (H : a ∈ l ∧ f a = b), from exists_of_mem_map H1,
-                  exists.intro a (and.intro (mem_cons_of_mem _ (and.left H)) (and.right H)))
+                  obtain a (Hl : a ∈ l) (Hr : f a = b), from exists_of_mem_map H1,
+                  exists.intro a (and.intro (mem_cons_of_mem _ Hl) Hr))
 
 theorem eq_of_map_const {A B : Type} {b₁ b₂ : B} : ∀ {l : list A}, b₁ ∈ map (const A b₂) l → b₁ = b₂
 | []     h := absurd h !not_mem_nil
@@ -234,8 +234,8 @@ theorem exists_of_any {p : A → Prop} : ∀{l : list A}, any l p → ∃a, a 
 | (b::l) H := or.elim H
                 (assume H1 : p b, exists.intro b (and.intro !mem_cons H1))
                 (assume H1 : any l p,
-                  obtain a (H2 : a ∈ l ∧ p a), from exists_of_any H1,
-                  exists.intro a (and.intro (mem_cons_of_mem b (and.left H2)) (and.right H2)))
+                  obtain a (H2l : a ∈ l) (H2r : p a), from exists_of_any H1,
+                  exists.intro a (and.intro (mem_cons_of_mem b H2l) H2r))
 
 definition decidable_all (p : A → Prop) [H : decidable_pred p] : ∀ l, decidable (all l p)
 | []       := decidable_true