diff --git a/library/init/nat.lean b/library/init/nat.lean
index 7a37e4a1f..e2c694cca 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -138,9 +138,9 @@ namespace nat
 
   theorem le.rec_on {a : nat} {P : nat → Prop} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b :=
   begin
-    cases H with b' hlt,
+    cases H with b hlt,
       apply H₁,
-      apply H₂ b' hlt
+      apply H₂ b hlt
   end
 
   theorem lt.irrefl (a : nat) : ¬ a < a :=
diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index 59d7fef91..bf420eafc 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -156,10 +156,10 @@ class inversion_tac {
         constraint_seq cs;
         if (m_tc.is_def_eq(lhs_type, rhs_type, justification(), cs) && !cs) {
             return mk_pair(mk_app(mk_constant(get_eq_name(), to_list(l)), lhs_type, lhs, rhs),
-                           mk_app(mk_constant(get_eq_refl_name(), to_list(l)), rhs_type, rhs));
+                           mk_app(mk_constant(get_eq_refl_name(), to_list(l)), lhs_type, lhs));
         } else {
             return mk_pair(mk_app(mk_constant(get_heq_name(), to_list(l)), lhs_type, lhs, rhs_type, rhs),
-                           mk_app(mk_constant(get_heq_refl_name(), to_list(l)), rhs_type, rhs));
+                           mk_app(mk_constant(get_heq_refl_name(), to_list(l)), lhs_type, lhs));
         }
     }
 
@@ -274,7 +274,7 @@ class inversion_tac {
                 expr t_type = binding_domain(d);
                 expr t      = mk_local(m_ngen.next(), g.get_unused_name(t_prefix, nidx), t_type, binder_info());
                 expr const & index = I_args[i];
-                add_eq(t, index);
+                add_eq(index, t);
                 h_new_type  = mk_app(h_new_type, t);
                 hyps.push_back(t);
                 ts.push_back(t);
@@ -282,7 +282,7 @@ class inversion_tac {
             }
             expr h_new    = mk_local(m_ngen.next(), h_new_name, h_new_type, local_info(h));
             if (m_dep_elim)
-                add_eq(h_new, h);
+                add_eq(h, h_new);
             hyps.push_back(h_new);
             expr new_type = Pi(eqs, g.get_type());
             expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
diff --git a/tests/lean/cases_tac.lean b/tests/lean/cases_tac.lean
index e84ccb53d..cb7456f2c 100644
--- a/tests/lean/cases_tac.lean
+++ b/tests/lean/cases_tac.lean
@@ -13,7 +13,7 @@ mk : Π a b : A, foo₂ a b
 
 example (A : Type) (B : A → Type) (f : A → A) (a : A) (H : foo₂ (f a) a) (Hb : H = H) (Hc : a = a) : A :=
 begin
-  cases H with [c, d],
+  cases H,
   state,
-  exact d
+  exact a
 end
diff --git a/tests/lean/cases_tac.lean.expected.out b/tests/lean/cases_tac.lean.expected.out
index 3a160486a..2926b0c60 100644
--- a/tests/lean/cases_tac.lean.expected.out
+++ b/tests/lean/cases_tac.lean.expected.out
@@ -1,14 +1,14 @@
 cases_tac.lean:7:2: proof state
 A : Type,
 B : A → Type,
-a_1 : A,
-Hb : B a_1
+a : A,
+Hb : B a
 ⊢ A
 cases_tac.lean:17:2: proof state
 A : Type,
 B : A → Type,
 f : A → A,
-d : A,
-Hc : d = d,
-Hb : foo₂.mk (f d) d = foo₂.mk (f d) d
+a : A,
+Hc : a = a,
+Hb : foo₂.mk (f a) a = foo₂.mk (f a) a
 ⊢ A
diff --git a/tests/lean/run/inversion1.lean b/tests/lean/run/inversion1.lean
index f246488e7..fcfbc2022 100644
--- a/tests/lean/run/inversion1.lean
+++ b/tests/lean/run/inversion1.lean
@@ -13,8 +13,8 @@ namespace fin
                          (f  : fin (succ n)) : C n f :=
   begin
     cases f,
-    apply (H₁ n_1),
-    apply (H₂ n_1 a)
+    apply (H₁ n),
+    apply (H₂ n a)
   end
 
 end fin
diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean
index 9ac6f64e3..94061c22c 100644
--- a/tests/lean/run/vector.lean
+++ b/tests/lean/run/vector.lean
@@ -107,14 +107,14 @@ namespace vector
   @vector.brec_on A P n w
   (λ (n : nat) (w : vector A n),
      begin
-       cases w with [n₁, h₁, t₁],
+       cases w with [n', h₁, t₁],
        show @below A P zero vnil → vector B zero → vector C zero, from
          λ b v, vnil,
-       show @below A P (succ n₁) (h₁ :: t₁) → vector B (succ n₁) → vector C (succ n₁), from
+       show @below A P (succ n') (h₁ :: t₁) → vector B (succ n') → vector C (succ n'), from
          λ b v,
          begin
-           cases v with [n₂, h₂, t₂],
-           have r : vector B n₂ → vector C n₂, from pr₁ b,
+           cases v with [n', h₂, t₂],
+           have r : vector B n' → vector C n', from pr₁ b,
            exact ((f h₁ h₂) :: r t₂),
          end
      end) v