fix(library/aux_definition): also zeta expand the local context

@leodemoura The forced zeta-expansion in mk_aux_definition might
cause problems if we use tactic.abstract without zeta-reduction.
However, we never use the non-zeta mode, and it already fails right now
if you accidentally use zeta-expansion in the proof we want to abstract.

src/library/aux_definition.cpp

@@ -109,7 +109,7 @@ struct mk_aux_definition_fn {
         name_map<expr> new_types;
         for (unsigned i = 0; i < m_params.size(); i++) {
             expr x = m_params[i];
-            expr new_type = collect(m_ctx.instantiate_mvars(m_ctx.infer(x)));
+            expr new_type = collect(zeta_expand(m_ctx.lctx(), m_ctx.instantiate_mvars(m_ctx.infer(x))));
             new_types.insert(mlocal_name(x), new_type);
         }
         local_context const & lctx = m_ctx.lctx();

tests/lean/run/abstract_zeta.lean

@@ -0,0 +1,14 @@
+-- The type of h depends on the zeta-expansion of n.  When we abstract the
+-- subterm proving `n < 5`, we need to zeta-expand n not just in the subterm,
+-- but also in the local context.
+
+lemma bug₁ : fin 5 :=
+let n : ℕ := 3 in
+have h : n < 5, from dec_trivial,
+⟨n, by abstract { exact h }⟩
+
+def bug₂ : fin 5 :=
+let n : ℕ := 3 in
+have h : n < 5, from dec_trivial,
+⟨n, show n < 5, from h⟩
+ -- ^^^^ the show is only used to trigger automatic abstraction