v4.3.0-rc1

• Many bug fixes:
  • Reduction of Decidable instances very slow when using cases tactic
  • simp not rewriting in binder
  • simp unfolding let even with zeta := false option
  • simp (with beta/zeta disabled) and discrimination trees
  • unknown free variable introduced by rw ... at h
  • dsimp doesn't use rfl theorems which consist of an unapplied constant
  • dsimp does not close reflexive equality goals if they are wrapped in metadata
  • rw [h] uses h from the environment in preference to h from the local context
  • missing withAssignableSyntheticOpaque for assumption tactic
  • ignoring default value for field warning
• Cancel outstanding tasks on document edit in the language server.
• Remove unnecessary % operations in Fin.mod and Fin.div
• Avoid DecidableEq in Array.mem
• Ensure USize.size unifies with ?m + 1
• Improve compatibility with emacs eglot client

Lake:

• Sensible defaults for lake new MyProject math
• Changed postUpdate? configuration option to a post_update declaration. See the post_update syntax docstring for more information on the new syntax.
• A manifest is automatically created on workspace load if one does not exists..
• The := syntax for configuration declarations (i.e., package, lean_lib, and lean_exe) has been deprecated. For example, package foo := {...} is deprecated.
• support for overriding package URLs via LAKE_PKG_URL_MAP