Try weaker variant of simp_all

[JLimperg]

Aesop uses simp_all by default. This rewrites with equations from the context, which can cause issues when the equations are not 'properly' oriented. We could instead try to use a weakened variant of simp_all that still does propositional rewriting (which is quite important) but doesn't use equations.

See https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/aesop.20with.20a.20.22bad.20simp.20hypothesis.22.20in.20the.20context

[JLimperg]

Also evaluate on https://github.com/artie2000/real_closed_field