mathlib

df2f2cfe - Make `ereal.coe_` lemmas protected; fix `simp` looping when rewriting to the left with specific lemmas