Sebastian Ullrich merges two fixes to how Lean modules export theorems