chore(data/seq,data/hash_map): adapt to changes in injection tactic (l…

…eanprover/lean3@8a10d4c)

data/hash_map.lean

@@ -211,7 +211,7 @@ show valid_aux (λa, (mk_idx n (hash_fn a)).1) (array.iterate_aux bkts (λ_ v l,
 theorem valid.find_aux_iff {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) (a : α) (b : β a) :
  find_aux a (bkts.read hash_fn a) = some b ↔ sigma.mk a b ∈ bkts.as_list :=
 iff.trans (find_aux_iff _ _ _ (v.nodup _ _))
-  $ iff.trans (by exact ⟨λm, ⟨_, m⟩, λ⟨⟨i, h⟩, m⟩, by rwa [← v.eq' _ m] at m⟩)
+  $ iff.trans (by exact ⟨λm, ⟨_, m⟩, λ⟨⟨i, h⟩, m⟩, let h := v.eq' _ m in by rwa [←h] at m⟩)
    (iff.symm (bkts.mem_as_list _))
 
 theorem valid.contains_aux_iff {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) (a : α) :

data/seq/computation.lean

@@ -64,7 +64,7 @@ begin
   { apply subtype.eq, apply funext,
     dsimp [return], intro n,
     induction n with n IH,
-    { injection h, rwa h at f0 },
+    { injection h with h', rwa h' at f0 },
     { exact s.2 IH } }
 end
 
@@ -73,7 +73,7 @@ theorem destruct_eq_think {s : computation α} {s'} :
 begin
   dsimp [destruct],
   ginduction s.1 0 with f0 a'; intro h,
-  { injection h, rw ←h,
+  { injection h with h', rw ←h',
     cases s with f al,
     apply subtype.eq, dsimp [think, tail],
     rw ←f0, exact (stream.eta f).symm },
@@ -381,7 +381,7 @@ end
 
 @[simp] theorem results_think_iff {s : computation α} {a n} :
   results (think s) a (n + 1) ↔ results s a n :=
-⟨λ h, let ⟨n', r, e⟩ := of_results_think h in by injection e; rwa h,
+⟨λ h, let ⟨n', r, e⟩ := of_results_think h in by injection e with h'; rwa h',
 results_think⟩
 
 theorem results_thinkN {s : computation α} {a m} :

data/seq/parallel.lean

@@ -68,8 +68,8 @@ begin
         rw e at e', { contradiction },
         have := IH' m _ e,
         simp [parallel.aux2] at e',
-        cases destruct c; injection e',
-        rw ←h, simp [this] } },
+        cases destruct c; injection e' with h',
+        rw ←h', simp [this] } },
     ginduction parallel.aux2 l with h a l',
     { exact lem1 _ _ ⟨a, h⟩ },
     { have H2 : corec parallel.aux1 (l, S) = think _,
@@ -153,15 +153,15 @@ begin
             exact ⟨d, or.inr dm, ad⟩ } } } } },
   intros C aC, refine mem_rec_on aC _ (λ C' IH, _);
   intros l S e; have e' := congr_arg destruct e; have := lem1 l;
-  simp [parallel.aux1] at e'; cases parallel.aux2 l with a' l'; injection e',
-  { rw h at this, cases this with c cl, cases cl with cl ac,
+  simp [parallel.aux1] at e'; cases parallel.aux2 l with a' l'; injection e' with h',
+  { rw h' at this, cases this with c cl, cases cl with cl ac,
     exact ⟨c, or.inl cl, ac⟩ },
-  { ginduction seq.destruct S with e a; rw e at h,
-    { exact let ⟨d, o, ad⟩ := IH _ _ h,
+  { ginduction seq.destruct S with e a; rw e at h',
+    { exact let ⟨d, o, ad⟩ := IH _ _ h',
         ⟨c, cl, ac⟩ := this a ⟨d, o.resolve_right (not_mem_nil _), ad⟩ in
       ⟨c, or.inl cl, ac⟩ },
-    { cases a with o S', cases o with c; simp [parallel.aux1] at h;
-      cases IH _ _ h with d dm; cases dm with o ad; cases o with dl dS',
+    { cases a with o S', cases o with c; simp [parallel.aux1] at h';
+      cases IH _ _ h' with d dm; cases dm with o ad; cases o with dl dS',
       { exact let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩ in ⟨c, or.inl cl, ac⟩ },
       { refine ⟨d, or.inr _, ad⟩,
         rw seq.destruct_eq_cons e,

data/seq/seq.lean

@@ -122,7 +122,8 @@ begin
     rw TH, apply h1 _ _ (or.inl rfl) },
   revert e, apply s.cases_on _ (λ b s', _); intro e,
   { injection e },
-  { rw [show (cons b s').val (nat.succ k) = s'.val k, by cases s'; refl] at e,
+  { have h_eq : (cons b s').val (nat.succ k) = s'.val k, { cases s'; refl },
+    rw [h_eq] at e,
     apply h1 _ _ (or.inr (IH e)) }
 end
 
@@ -506,7 +507,7 @@ theorem mem_map (f : α → β) {a : α} : ∀ {s : seq α}, a ∈ s → f a ∈
 
 theorem exists_of_mem_map {f} {b : β} : ∀ {s : seq α}, b ∈ map f s → ∃ a, a ∈ s ∧ f a = b
 | ⟨g, al⟩ h := let ⟨o, om, oe⟩ := stream.exists_of_mem_map h in
-  by cases o; injection oe; exact ⟨a, om, h⟩
+  by cases o; injection oe with h'; exact ⟨a, om, h'⟩
 
 def of_mem_append {s₁ s₂ : seq α} {a : α} (h : a ∈ append s₁ s₂) : a ∈ s₁ ∨ a ∈ s₂ :=
 begin

data/seq/wseq.lean

@@ -544,7 +544,7 @@ theorem head_some_of_head_tail_some {s : wseq α} {a}
 begin
   unfold head at h,
   cases exists_of_mem_map h with o ho, cases ho with md e, clear h,
-  cases o with o; injection e, clear e h,
+  cases o with o; injection e with h', clear e h',
   cases destruct_some_of_destruct_tail_some md with a am,
   exact ⟨_, mem_map ((<$>) (@prod.fst α (wseq α))) am⟩
 end
@@ -612,12 +612,16 @@ begin
   { rw [i4, i5],
     cases s' with f al,
     unfold cons has_mem.mem wseq.mem seq.mem seq.cons, simp,
-    rw [show a = a' ↔ some (some a) = some (some a'),
-        by constructor; intro h; [rw h, repeat {injection h}]],
+    have h_a_eq_a' : a = a' ↔ some (some a) = some (some a'),
+      { constructor,
+        { intro h, rw h },
+        { intro h, injection h with h', injection h' } },
+    rw [h_a_eq_a'],
     refine ⟨stream.eq_or_mem_of_mem_cons, λo, _⟩,
     { cases o with e m,
       { rw e, apply stream.mem_cons },
-      { exact stream.mem_cons_of_mem _ m } } },
+      { exact stream.mem_cons_of_mem _ m } }
+  },
   { simp, exact IH i2 }
 end
 
@@ -648,9 +652,9 @@ theorem nth_mem {s : wseq α} {a n} : some a ∈ nth s n → a ∈ s :=
 begin
   revert s, induction n with n IH; intros s h,
   { cases exists_of_mem_map h with o h, cases h with h1 h2,
-    cases o with o; injection h2,
+    cases o with o; injection h2 with h',
     cases o with a' s',
-    exact (eq_or_mem_iff_mem h1).2 (or.inl h.symm) },
+    exact (eq_or_mem_iff_mem h1).2 (or.inl h'.symm) },
   { have := @IH (tail s), rw nth_tail at this,
     exact mem_of_mem_tail (this h) }
 end
@@ -712,7 +716,7 @@ seq.mem_append_left
 
 theorem exists_of_mem_map {f} {b : β} : ∀ {s : wseq α}, b ∈ map f s → ∃ a, a ∈ s ∧ f a = b
 | ⟨g, al⟩ h := let ⟨o, om, oe⟩ := seq.exists_of_mem_map h in
-  by cases o; injection oe; exact ⟨a, om, h⟩
+  by cases o; injection oe with h'; exact ⟨a, om, h'⟩
 
 @[simp] def lift_rel_nil (R : α → β → Prop) : lift_rel R nil nil :=
 by rw [lift_rel_destruct_iff]; simp