fix(tactic/delta_instance): beta reduce type of instance (#6396)

The delta derive handler was creating instances that weren't beta reduced, which isn't a problem for type class inference but can be unexpected. @gebner fixed the line in doc-gen that assumed beta reduction, but we should also produce the expected instance in the first place.

Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/doc-gen.20is.20failing



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/tactic/delta_instance.lean

@@ -65,6 +65,8 @@ do new_decl ← get_decl new_decl_name,
    new_decl_pexpr ← resolve_name new_decl_name,
    arity ← get_pexpr_arg_arity_with_tgt cls new_decl.type,
    tgt ← to_expr $ apply_under_n_pis cls new_decl_pexpr new_decl.type (new_decl.type.pi_arity - arity),
+   (vs, tgt') ← open_pis tgt,
+   tgt ← whnf tgt' transparency.none >>= pis vs,
    (_, inst) ← solve_aux tgt $ tactic.delta_instance [new_decl_name],
    inst ← instantiate_mvars inst,
    inst ← replace_univ_metas_with_univ_params inst,