diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org
index 32bd2531bd..f1cca3b933 100644
--- a/doc/lean/tutorial.org
+++ b/doc/lean/tutorial.org
@@ -761,7 +761,7 @@ of two even numbers is an even number.
     exists_intro (w1 + w2)
       (calc a + b  =  2*w1 + b      : {Hw1}
               ...  =  2*w1 + 2*w2   : {Hw2}
-              ...  =  2*(w1 + w2)   : symm (mul_add_distr_right 2 w1 w2))))
+              ...  =  2*(w1 + w2)   : symm (mul_distr_left 2 w1 w2))))
 
 #+END_SRC
 
@@ -781,6 +781,5 @@ With this macro we can write the example above in a more natural way
     exists_intro (w1 + w2)
       (calc a + b  =  2*w1 + b      : {Hw1}
               ...  =  2*w1 + 2*w2   : {Hw2}
-              ...  =  2*(w1 + w2)   : symm (mul_add_distr_right 2 w1 w2))
+              ...  =  2*(w1 + w2)   : symm (mul_distr_left 2 w1 w2))
 #+END_SRC
-
diff --git a/tests/lean/empty.lean.expected.out b/tests/lean/empty.lean.expected.out
index e13eabedf2..88c2487e33 100644
--- a/tests/lean/empty.lean.expected.out
+++ b/tests/lean/empty.lean.expected.out
@@ -1,5 +1,5 @@
-empty.lean:5:25: error: type error in placeholder assigned to
-  inhabited_Prop
+empty.lean:6:25: error: type error in placeholder assigned to
+  Prop_inhabited
 placeholder has type
   inhabited Prop
 but is expected to have type