mathlib

67593dcd - fix(tactic/ring_exp): fix normalization proof of unchanged subexpressions (#11394)

fix(tactic/ring_exp): fix normalization proof of unchanged subexpressions (#11394) When trying to simplify a goal (instead of proving equalities), `ring_exp` will rewrite subexpressions to a normal form, then simplify this normal form by removing extraneous `+ 0`s and `* 1`s. Both steps return a new expression and a proof that the *step*'s input expression equals the output expression. In some cases where the normal form and simplified form coincide, `ex.simplify` would instead output a proof that *ring_exp*'s input expression equals the output expression, so we'd get a type error in trying to compose a proof that `a = b` with a proof that `a = b`. This PR fixes that bug by returning instead a proof that `b = b`, as expected.