diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean
index e7d4db9a1..dffffe629 100644
--- a/hott/init/tactic.hlean
+++ b/hott/init/tactic.hlean
@@ -148,4 +148,5 @@ nat.rec id (λn t', and_then t t') (nat.of_num n)
 
 end tactic
 tactic_infixl `;`:15 := tactic.and_then
+tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2))
 tactic_notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index bd27e8193..1f16ab20a 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -147,4 +147,5 @@ definition do (n : num) (t : tactic) : tactic :=
 nat.rec id (λn t', and_then t t') (nat.of_num n)
 end tactic
 tactic_infixl `;`:15 := tactic.and_then
+tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2))
 tactic_notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
diff --git a/tests/lean/771.lean b/tests/lean/771.lean
index 1bd2cdad1..f7a7938b1 100644
--- a/tests/lean/771.lean
+++ b/tests/lean/771.lean
@@ -3,7 +3,7 @@ definition id_1 (n : nat) :=
    by exact n
 
 definition id_2 (n : nat) :=
-   (by exact n : nat)
+   ((by exact n) : nat)
 
 definition id_3 (n : nat) : nat :=
 by exact n
diff --git a/tests/lean/775.lean b/tests/lean/775.lean
new file mode 100644
index 000000000..82c9f0417
--- /dev/null
+++ b/tests/lean/775.lean
@@ -0,0 +1,10 @@
+open nat
+
+tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2))
+
+example (P Q : ℕ → ℕ → Prop) (n m : ℕ) (p : P n m) : Q n m ∧ false :=
+begin
+  split,
+  revert m p, induction n : intro m; induction m : intro p,
+  state, repeat exact sorry
+end
diff --git a/tests/lean/775.lean.expected.out b/tests/lean/775.lean.expected.out
new file mode 100644
index 000000000..67acb60cc
--- /dev/null
+++ b/tests/lean/775.lean.expected.out
@@ -0,0 +1,29 @@
+775.lean:9:2: proof state
+P Q : ℕ → ℕ → Prop,
+p : P 0 0
+⊢ Q 0 0
+
+P Q : ℕ → ℕ → Prop,
+a : ℕ,
+v_0 : P 0 a → Q 0 a,
+p : P 0 (succ a)
+⊢ Q 0 (succ a)
+
+P Q : ℕ → ℕ → Prop,
+a : ℕ,
+v_0 : ∀ (m : ℕ), P a m → Q a m,
+p : P (succ a) 0
+⊢ Q (succ a) 0
+
+P Q : ℕ → ℕ → Prop,
+a : ℕ,
+v_0 : ∀ (m : ℕ), P a m → Q a m,
+a_1 : ℕ,
+v_0_1 : P (succ a) a_1 → Q (succ a) a_1,
+p : P (succ a) (succ a_1)
+⊢ Q (succ a) (succ a_1)
+
+P Q : ℕ → ℕ → Prop,
+n m : ℕ,
+p : P n m
+⊢ false