mathlib3

a6444313 - fix(refine_struct): fix regression from #2319