mathlib3

43647988 - fix(data/fin): better defeqs in fin.has_le instance (#3869)

fix(data/fin): better defeqs in fin.has_le instance (#3869) This ensures that the instances from `fin.decidable_linear_order` match the direct instances. They were defeq before but not at instance reducibility.