Emit default options in synported files

[gebner]

I often have to add some options just to get the statements of the theorems to elaborate:

set_option synthInstance.maxHeartbeats 100000

In the future we might also want to add options that disable automatic implicit lambdas (see #53).

[dselsam]

It might be nice to bundle them all in one command, e.g. #mathlib_set_defaults

[gebner]

That's a good suggestion, but I'm not sure it's the best idea.

1. In my experience, putting mathport configuration in mathlib4 is a bit of a maintenance headache. For example changing alignments requires adding it to mathlib4, then update mathlib4 in mathport, and then verify that the alignment actually works. I'd rather keep these things in the mathport repo if possible to make it easier to iterate on them.
2. After porting, we might want to remove these options incrementally again. Having several lines makes it easier to clean up the "hackport" options again.

[digama0]

An alignment is a relationship between a lean 3 mathlib definition and a mathlib4 definition; it does not intrinsically involve mathport. It might make sense for rapid iteration purposes to have mathport configuration that overrides these alignment indications, but for reasonably stable alignments that we want to keep I think we should be pushing them to mathlib4.