mathlib3

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

#2319

Merged