mathlib3

c85453d9 - fix(tactic/refine_struct): don't add unnecessary `eq.mpr` or `id` (#2319)

fix(tactic/refine_struct): don't add unnecessary `eq.mpr` or `id` (#2319) * fix(tactic/interactive): don't unfold non-Prop goals The old behaviour caused `eq.mpr`'s in `pi_instance` output. * add a test file * move test * actually move test * Update test/refine_struct.lean * test: fix compile * Apply suggestions from code review Co-Authored-By: Gabriel Ebner <gebner@gebner.org> * Try a fix by @gebner and @cipher1024 * Update test/refine_struct.lean Co-Authored-By: Gabriel Ebner <gebner@gebner.org> * apply Gabriel's suggestion Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>