Theorem Proving in Lean test errors

Running Sphinx v3.1.2
/theorem_proving_in_lean/lean_sphinx.py:4: RemovedInSphinx40Warning: sphinx.directives.CodeBlock is deprecated. Check CHANGES for Sphinx API modifications.
  from sphinx.directives import CodeBlock
making output directory... done
building [mo]: targets for 0 po files that are out of date
building [leantest]: targets for 12 source files that are out of date
updating environment: [new config] 12 added, 0 changed, 0 removed
reading sources... [100%] type_classes
looking for now-outdated files... none found
pickling environment... done
checking consistency... done
preparing documents... done
writing output... [100%] type_classes

Sphinx error:

lean exited with errors:
/theorem_proving_in_lean/_build/leantest/tactics_86.lean:1:0: error: file 'data/list/basic' not found in the search path
/theorem_proving_in_lean/_build/leantest/tactics_87.lean:1:0: error: file 'data/list/basic' not found in the search path
/theorem_proving_in_lean/_build/leantest/tactics_88.lean:1:0: error: file 'data/list/basic' not found in the search path
/theorem_proving_in_lean/_build/leantest/tactics_90.lean:1:0: error: file 'data/list/basic' not found in the search path
/theorem_proving_in_lean/_build/leantest/tactics_94.lean:1:0: error: file 'data/list/basic' not found in the search path
/theorem_proving_in_lean/_build/leantest/tactics_91.lean:1:0: error: file 'data/list/basic' not found in the search path
/theorem_proving_in_lean/_build/leantest/tactics_75.lean:1:0: error: file 'data/list/basic' not found in the search path
/theorem_proving_in_lean/_build/leantest/tactics_95.lean:1:0: error: file 'data/list/basic' not found in the search path
/theorem_proving_in_lean/_build/leantest/tactics_92.lean:1:0: error: file 'data/list/basic' not found in the search path
/theorem_proving_in_lean/_build/leantest/tactics_93.lean:1:0: error: file 'data/list/basic' not found in the search path
/theorem_proving_in_lean/_build/leantest/tactics_86.lean:1:0: error: invalid import: data.list.basic
/theorem_proving_in_lean/_build/leantest/tactics_89.lean:1:0: error: file 'data/list/basic' not found in the search path
/theorem_proving_in_lean/_build/leantest/tactics_87.lean:1:0: error: invalid import: data.list.basic
/theorem_proving_in_lean/_build/leantest/tactics_88.lean:1:0: error: invalid import: data.list.basic
/theorem_proving_in_lean/_build/leantest/tactics_90.lean:1:0: error: invalid import: data.list.basic
/theorem_proving_in_lean/_build/leantest/tactics_94.lean:1:0: error: invalid import: data.list.basic
/theorem_proving_in_lean/_build/leantest/tactics_91.lean:1:0: error: invalid import: data.list.basic
/theorem_proving_in_lean/_build/leantest/tactics_75.lean:1:0: error: invalid import: data.list.basic
/theorem_proving_in_lean/_build/leantest/tactics_95.lean:1:0: error: invalid import: data.list.basic
/theorem_proving_in_lean/_build/leantest/tactics_92.lean:1:0: error: invalid import: data.list.basic
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:1:25: error: unknown identifier 'ordered_ring'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_37.lean:1:8: error: unknown identifier 'add_le_add_left'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_8.lean:1:7: error: unknown identifier 'add_sub_cancel'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_52.lean:1:7: error: unknown identifier 'sub_self'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_38.lean:1:7: error: unknown identifier 'mul_inv_self'
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:1:22: error: unknown identifier 'comm_ring'
/theorem_proving_in_lean/_build/leantest/tactics_93.lean:1:0: error: invalid import: data.list.basic
/theorem_proving_in_lean/_build/leantest/tactics_89.lean:1:0: error: invalid import: data.list.basic
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_37.lean:2:8: error: unknown identifier 'add_le_add_right'
/theorem_proving_in_lean/_build/leantest/tactics_77.lean:3:23: error: unknown identifier 'mul_comm'
/theorem_proving_in_lean/_build/leantest/tactics_77.lean:3:32: error: unknown identifier 'mul_assoc'
/theorem_proving_in_lean/_build/leantest/tactics_77.lean:3:42: error: unknown identifier 'mul_left_comm'
/theorem_proving_in_lean/_build/leantest/tactics_77.lean:3:0: error: unknown declaration 'mul_comm'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_23.lean:3:3: error: unknown identifier 'mul_add'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_38.lean:2:7: error: unknown identifier 'neg_add_self'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_35.lean:4:8: error: unknown identifier 'neg_neg'
/theorem_proving_in_lean/_build/leantest/tactics_70.lean:3:2: error: unknown identifier 'add_assoc'
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:3:23: error: unknown identifier 'mul_comm'
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:3:32: error: unknown identifier 'mul_assoc'
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:3:42: error: unknown identifier 'mul_left_comm'
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:3:0: error: unknown declaration 'mul_comm'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_15.lean:3:53: error: unknown identifier 'mul_add'
/theorem_proving_in_lean/_build/leantest/tactics_83.lean:3:3: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:3:22: error: unknown identifier 'ring'
/theorem_proving_in_lean/_build/leantest/propositions_and_proofs_23.lean:4:20: error: invalid expression
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_8.lean:3:7: error: unknown identifier '_root_.add_sub_cancel'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_33.lean:10:36: error: unknown identifier 'mul_add'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_23.lean:7:3: error: unknown identifier 'mul_add'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_34.lean:4:8: error: unknown identifier 'mul_zero'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_34.lean:7:39: error: unknown identifier 'mul_add'
/theorem_proving_in_lean/_build/leantest/tactics_76.lean:6:5: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/tactics_70.lean:8:2: error: unknown identifier 'add_assoc'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_15.lean:4:53: error: unknown identifier 'add_mul'
/theorem_proving_in_lean/_build/leantest/axioms_and_computation_7.lean:4:44: error: unknown identifier 'zero_add'
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:12: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:20: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:28: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:10:22: error: unknown identifier 'group'
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:34: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:26: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:22: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:10: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:6: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:4: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:8: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:16: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:10:54: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:4:24: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:10:48: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_78.lean:3:23: error: unknown identifier 'mul_comm'
/theorem_proving_in_lean/_build/leantest/tactics_78.lean:3:32: error: unknown identifier 'mul_assoc'
/theorem_proving_in_lean/_build/leantest/tactics_78.lean:3:42: error: unknown identifier 'mul_left_comm'
/theorem_proving_in_lean/_build/leantest/tactics_78.lean:3:0: error: unknown declaration 'mul_comm'
/theorem_proving_in_lean/_build/leantest/propositions_and_proofs_23.lean:4:20: error: command expected
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:3:23: error: unknown identifier 'add_zero'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:4:34: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:4:32: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_22.lean:4:54: error: unknown identifier 'mul_add'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_34.lean:5:8: error: unknown identifier 'mul_one'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_22.lean:5:54: error: unknown identifier 'add_mul'
/theorem_proving_in_lean/_build/leantest/tactics_77.lean:6:5: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_22.lean:6:54: error: unknown identifier 'add_mul'
/theorem_proving_in_lean/_build/leantest/induction_and_recursion_45.lean:8:10: error: function expected at
/theorem_proving_in_lean/_build/leantest/induction_and_recursion_45.lean:8:19: error: don't know how to synthesize placeholder (a)
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_22.lean:7:54: error: unknown identifier 'add_assoc'
/theorem_proving_in_lean/_build/leantest/induction_and_recursion_45.lean:7:4: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_36.lean:4:8: error: unknown identifier 'add_lt_add_of_lt_of_le'
/theorem_proving_in_lean/_build/leantest/inductive_types_59.lean:6:16: error: unknown identifier 'add_zero'
/theorem_proving_in_lean/_build/leantest/tactics_85.lean:6:5: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/tactics_70.lean:13:2: error: unknown identifier 'add_assoc'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_15.lean:5:49: error: unknown identifier 'add_assoc'
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:5:25: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:5:30: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:5:34: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/axioms_and_computation_7.lean:4:55: error: invalid field notation, type is not of the form (C ...) where C is a constant
/theorem_proving_in_lean/_build/leantest/tactics_73.lean:11:3: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_74.lean:5:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:4:23: error: unknown identifier 'zero_add'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:5:36: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:5:34: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_71.lean:4:5: error: unknown identifier 'add_zero'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_34.lean:6:8: error: unknown identifier 'sub_add_eq_add_sub'
/theorem_proving_in_lean/_build/leantest/tactics_77.lean:10:5: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_26.lean:8:7: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/inductive_types_59.lean:9:16: error: unknown identifier 'add_zero'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_15.lean:10:7: error: unknown identifier 'mul_add'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_15.lean:12:8: error: unknown identifier 'add_mul'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_15.lean:12:26: error: unknown identifier 'add_mul'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_15.lean:13:10: error: unknown identifier 'add_assoc'
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:8:39: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:8:34: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:8:55: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:8:51: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:8:47: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_85.lean:10:5: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:8:59: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:8:26: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_79.lean:8:30: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_75.lean:8:3: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:5:23: error: unknown identifier 'mul_one'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:6:37: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:6:50: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_78.lean:6:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/inductive_types_67.lean:15:9: error: function expected at
/theorem_proving_in_lean/_build/leantest/tactics_88.lean:10:3: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/tactics_87.lean:10:21: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/tactics_90.lean:11:3: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/tactics_94.lean:10:3: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_15.lean:12:23: error: invalid 'eq.subst' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but term
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_15.lean:13:52: error: invalid field notation, type is not of the form (C ...) where C is a constant
/theorem_proving_in_lean/_build/leantest/tactics_91.lean:12:3: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/inductive_types_59.lean:13:5: error: unknown identifier 'add_zero'
/theorem_proving_in_lean/_build/leantest/tactics_75.lean:12:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_16.lean:12:19: error: unknown identifier 'add_comm'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:6:23: error: unknown identifier 'one_mul'
/theorem_proving_in_lean/_build/leantest/tactics_74.lean:9:5: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/tactics_92.lean:11:3: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/tactics_95.lean:10:22: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_31.lean:11:0: error: unknown identifier group
/theorem_proving_in_lean/_build/leantest/inductive_types_38.lean:13:6: error: unknown identifier 'zero_add'
/theorem_proving_in_lean/_build/leantest/tactics_78.lean:9:6: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/tactics_90.lean:15:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/tactics_91.lean:16:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:7:24: error: unknown identifier 'neg_add_self'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_1.lean:10:5: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/inductive_types_59.lean:16:16: error: unknown identifier 'add_zero'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_31.lean:11:17: error: unknown identifier 'group'
/theorem_proving_in_lean/_build/leantest/tactics_93.lean:10:3: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/tactics_89.lean:10:3: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_19.lean:10:3: error: unknown identifier 'add_comm'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_20.lean:10:3: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/tactics_90.lean:20:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/tactics_91.lean:21:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:8:24: error: unknown identifier 'add_neg_self'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_18.lean:12:22: error: unknown identifier 'add_comm'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:12:13: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_92.lean:17:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:15:28: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:12:9: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:15:26: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:12:34: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:12:26: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_95.lean:18:5: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_17.lean:13:22: error: unknown identifier 'add_comm'
/theorem_proving_in_lean/_build/leantest/tactics_89.lean:15:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:9:23: error: unknown identifier 'sub_self'
/theorem_proving_in_lean/_build/leantest/tactics_94.lean:19:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:18:39: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:18:37: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:18:52: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:18:50: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:19:9: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:10:27: error: unknown identifier 'add_comm'
/theorem_proving_in_lean/_build/leantest/tactics_92.lean:22:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:19:22: error: failed to synthesize type class instance for
/theorem_proving_in_lean/_build/leantest/tactics_95.lean:23:5: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/tactics_89.lean:20:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_30.lean:8:17: error: unknown identifier 'ring'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:11:37: error: unknown identifier 'add_assoc'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_1.lean:16:5: error: unknown identifier 'add_mul'
/theorem_proving_in_lean/_build/leantest/tactics_94.lean:24:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/tactics_93.lean:18:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_30.lean:9:14: error: unknown identifier 'ring'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:12:27: error: unknown identifier 'mul_comm'
/theorem_proving_in_lean/_build/leantest/tactics_95.lean:28:5: error: unknown identifier 'reverse_append'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:13:37: error: unknown identifier 'mul_assoc'
/theorem_proving_in_lean/_build/leantest/tactics_93.lean:23:3: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:14:41: error: unknown identifier 'mul_add'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:15:41: error: unknown identifier 'left_distrib'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:16:41: error: unknown identifier 'add_mul'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_26.lean:26:21: error: simplify tactic failed to simplify
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:17:41: error: unknown identifier 'right_distrib'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:18:41: error: unknown identifier 'mul_sub'
/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_14.lean:19:41: error: unknown identifier 'sub_mul'
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_26.lean:29:5: error: tactic failed, there are unsolved goals
/theorem_proving_in_lean/_build/leantest/interacting_with_lean_26.lean:35:4: error: unknown identifier 'mul_add'

make: *** [Makefile:28: leantest] Error 2