diff --git a/src/frontends/lean/notation.h b/src/frontends/lean/notation.h
index f5e934d3f..476ebd2ca 100644
--- a/src/frontends/lean/notation.h
+++ b/src/frontends/lean/notation.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 namespace lean {
 constexpr unsigned g_eq_precedence    = 50;
-constexpr unsigned g_arrow_precedence = 70;
+constexpr unsigned g_arrow_precedence = 25;
 class frontend;
 void init_builtin_notation(frontend & fe);
 }
diff --git a/tests/lean/cast2.lean b/tests/lean/cast2.lean
index 4194ca4ac..32cc69b36 100644
--- a/tests/lean/cast2.lean
+++ b/tests/lean/cast2.lean
@@ -2,7 +2,7 @@ Variable A : Type
 Variable B : Type
 Variable A' : Type
 Variable B' : Type
-Axiom H : A -> B = A' -> B'
+Axiom H : (A -> B) = (A' -> B')
 Variable a : A
 Check DomInj H
 Theorem BeqB' : B = B' := RanInj H a
diff --git a/tests/lean/cast3.lean b/tests/lean/cast3.lean
index dd536e07f..ada90b3c8 100644
--- a/tests/lean/cast3.lean
+++ b/tests/lean/cast3.lean
@@ -4,10 +4,10 @@ Eval cast (Refl A) x
 Eval x = (cast (Refl A) x)
 Variable b : B
 Definition f (x : A) : B := b
-Axiom H : A -> B = A' -> B
+Axiom H : (A -> B) = (A' -> B)
 Variable a' : A'
 Eval (cast H f) a'
-Axiom H2 : A -> B = A' -> B'
+Axiom H2 : (A -> B) = (A' -> B')
 Definition g (x : B') : Nat := 0
 Eval g ((cast H2 f) a')
 Check g ((cast H2 f) a')
diff --git a/tests/lean/elab2.lean b/tests/lean/elab2.lean
index e49185c02..ba7b9525a 100644
--- a/tests/lean/elab2.lean
+++ b/tests/lean/elab2.lean
@@ -6,19 +6,19 @@ Variable D : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A,
 Variable R : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
              (B a) = (B' (C A A' (D A A' B B' H) a))
 
-Theorem R2 (A A' B B' : Type) (H : A -> B = A' -> B') (a : A) : B = B' := R _ _ _ _ H a
+Theorem R2 (A A' B B' : Type) (H : (A -> B) = (A' -> B')) (a : A) : B = B' := R _ _ _ _ H a
 
 Show Environment 1
 
-Theorem R3 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
-    fun (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1),
+Theorem R3 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
+    fun (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1),
         R _ _ _ _ H a
 
-Theorem R4 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
-    fun (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : _),
+Theorem R4 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
+    fun (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : _),
         R _ _ _ _ H a
 
-Theorem R5 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
+Theorem R5 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
     fun (A1 A2 B1 B2 : Type) (H : _) (a : _),
         R _ _ _ _ H a
 
diff --git a/tests/lean/elab2.lean.expected.out b/tests/lean/elab2.lean.expected.out
index c7867a23f..b2e168736 100644
--- a/tests/lean/elab2.lean.expected.out
+++ b/tests/lean/elab2.lean.expected.out
@@ -4,9 +4,9 @@
   Assumed: D
   Assumed: R
   Proved: R2
-Theorem R2 (A A' B B' : Type) (H : A → B = A' → B') (a : A) : B = B' := R A A' (λ x : A, B) (λ x : A', B') H a
+Theorem R2 (A A' B B' : Type) (H : (A → B) = (A' → B')) (a : A) : B = B' := R A A' (λ x : A, B) (λ x : A', B') H a
   Proved: R3
   Proved: R4
   Proved: R5
-Theorem R5 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
+Theorem R5 (A1 A2 B1 B2 : Type) (H : (A1 → B1) = (A2 → B2)) (a : A1) : B1 = B2 :=
     R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a
diff --git a/tests/lean/elab3.lean b/tests/lean/elab3.lean
index 821d09632..937b776a1 100644
--- a/tests/lean/elab3.lean
+++ b/tests/lean/elab3.lean
@@ -5,7 +5,7 @@ Variable D : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A,
 Variable R : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
              (B a) = (B' (C A A' (D A A' B B' H) a))
 
-Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
+Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
     fun A1 A2 B1 B2 H a,
         R _ _ _ _ H a
 
diff --git a/tests/lean/elab3.lean.expected.out b/tests/lean/elab3.lean.expected.out
index 6c0393c85..053d4b78a 100644
--- a/tests/lean/elab3.lean.expected.out
+++ b/tests/lean/elab3.lean.expected.out
@@ -4,5 +4,5 @@
   Assumed: D
   Assumed: R
   Proved: R2
-Theorem R2 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
+Theorem R2 (A1 A2 B1 B2 : Type) (H : (A1 → B1) = (A2 → B2)) (a : A1) : B1 = B2 :=
     R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a
diff --git a/tests/lean/elab4.lean b/tests/lean/elab4.lean
index 068146433..026610862 100644
--- a/tests/lean/elab4.lean
+++ b/tests/lean/elab4.lean
@@ -5,7 +5,7 @@ Variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x)
 Variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A) :
              (B a) = (B' (C (D H) a))
 
-Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
+Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
     fun A1 A2 B1 B2 H a, R H a
 
 Set pp::implicit true
diff --git a/tests/lean/elab5.lean b/tests/lean/elab5.lean
index fe61720a7..619148a65 100644
--- a/tests/lean/elab5.lean
+++ b/tests/lean/elab5.lean
@@ -5,7 +5,7 @@ Variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x)
 Variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A) :
              (B a) = (B' (C (D H) a))
 
-Theorem R2 : Pi (A1 A2 B1 B2 : Type), (A1 -> B1 = A2 -> B2) -> A1 -> (B1 = B2) :=
+Theorem R2 : Pi (A1 A2 B1 B2 : Type), ((A1 -> B1) = (A2 -> B2)) -> A1 -> (B1 = B2) :=
     fun A1 A2 B1 B2 H a, R H a
 
 Set pp::implicit true
diff --git a/tests/lean/interactive/t11.lean b/tests/lean/interactive/t11.lean
new file mode 100644
index 000000000..1621249f2
--- /dev/null
+++ b/tests/lean/interactive/t11.lean
@@ -0,0 +1,14 @@
+(**
+auto = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
+**)
+
+Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
+     fun assumption : A /\ B,
+          let lemma1     : A      := _,
+              lemma2     : B      := _,
+              conclusion : B /\ A := _
+          in conclusion.
+   apply auto. done.
+   apply auto. done.
+   apply auto. done.
+
diff --git a/tests/lean/interactive/t11.lean.expected.out b/tests/lean/interactive/t11.lean.expected.out
new file mode 100644
index 000000000..914f7fed0
--- /dev/null
+++ b/tests/lean/interactive/t11.lean.expected.out
@@ -0,0 +1,17 @@
+Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
+#   Set: pp::colors
+  Set: pp::unicode
+Proof state:
+A : Bool, B : Bool, assumption : A ∧ B ⊢ A
+## Proof state:
+no goals
+## Proof state:
+A : Bool, B : Bool, assumption : A ∧ B, lemma1 : A ⊢ B
+## Proof state:
+no goals
+## Proof state:
+A : Bool, B : Bool, assumption : A ∧ B, lemma1 : A, lemma2 : B ⊢ B ∧ A
+## Proof state:
+no goals
+##   Proved: T2
+# 
\ No newline at end of file
diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out
index 89f98d1fa..ea33444cf 100644
--- a/tests/lean/tst1.lean.expected.out
+++ b/tests/lean/tst1.lean.expected.out
@@ -13,7 +13,7 @@
   Defined: select
   Defined: map
 Axiom two_lt_three : two < three
-Definition vector (A : Type) (n : N) : Type := Π (i : N), (i < n) → A
+Definition vector (A : Type) (n : N) : Type := Π (i : N), i < n → A
 Definition const {A : Type} (n : N) (d : A) : vector A n := λ (i : N) (H : i < n), d
 Definition const::explicit (A : Type) (n : N) (d : A) : vector A n := const n d
 Definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n :=
@@ -30,7 +30,7 @@ if (two == two) ⊤ ⊥
 update (const three ⊥) two ⊤ : vector Bool three
 
 --------
-select::explicit : Π (A : Type) (n : N) (v : vector A n) (i : N), (i < n) → A
+select::explicit : Π (A : Type) (n : N) (v : vector A n) (i : N), i < n → A
 
 map type ---> 
 map::explicit : Π (A B C : Type) (n : N), (A → B → C) → (vector A n) → (vector B n) → (vector C n)
@@ -39,11 +39,11 @@ map normal form -->
 λ (A B C : Type)
   (n : N)
   (f : A → B → C)
-  (v1 : Π (i : N), (i < n) → A)
-  (v2 : Π (i : N), (i < n) → B)
+  (v1 : Π (i : N), i < n → A)
+  (v2 : Π (i : N), i < n → B)
   (i : N)
   (H : i < n),
   f (v1 i H) (v2 i H)
 
 update normal form --> 
-λ (A : Type) (n : N) (v : Π (i : N), (i < n) → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) d (v j H)
+λ (A : Type) (n : N) (v : Π (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) d (v j H)
diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out
index be6893f83..c567e89ff 100644
--- a/tests/lean/tst11.lean.expected.out
+++ b/tests/lean/tst11.lean.expected.out
@@ -6,7 +6,7 @@
 ⊤
   Assumed: a
 a ⊕ a ⊕ a
-Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → (a == b) → (P b)
+Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → a == b → (P b)
   Proved: EM2
 EM2 : Π a : Bool, a ∨ ¬ a
 EM2 a : a ∨ ¬ a
diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out
index 2603e134e..1866aa825 100644
--- a/tests/lean/tst4.lean.expected.out
+++ b/tests/lean/tst4.lean.expected.out
@@ -11,7 +11,7 @@ f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
 EqNice::explicit N n1 n2
 f::explicit N n1 n2 : N
 Congr::explicit :
-    Π (A : Type U) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), (f == g) → (a == b) → ((f a) == (g b))
+    Π (A : Type U) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), f == g → a == b → (f a) == (g b)
 f::explicit N n1 n2
   Assumed: a
   Assumed: b