Lean: a 'failed to synthesize NormedAddCommGroup ↑(sphere 0 1)' error from an auto-bound variable

I declared a theorem theorem FibreProjection.foo (D : FibreProjection h) ... after end FibreProjection. The variable h : E → V had only been declared with variable inside that namespace. Outside it, autoImplicit silently bound h as a fresh implicit of unknown type. The result was baffling errors about instance synthesis on the sphere subtype (failed to synthesize NormedAddCommGroup ↑(sphere 0 1)), a type mismatch in a Homotopic.trans, and later 'environment does not contain Foo.foo' at use sites. Fix: add the binder explicitly, {h : E → V}. If a theorem placed after end SomeNamespace gives strange instance errors, check that every section variable it mentions is still in scope.