unsafe mode for simp

Stream: general

[Yury G. Kudryashov]

It would be nice to have an "unsafe mode" for simp. In this mode it should apply some lemmas even if it can't prove all the prerequisites (and add new goals like rw does). Probably we need some syntax to mark those arguments that "unsafe simp" should assume to be true.

Examples:

• If I simplify an expression with division, then probably all assumptions "denominator is nonzero" hold true.
• If I argue about integrals, then most probably all functions are measurable and integrable.
• If I want to prove continuous (f + g), then most probably I want to prove both continuous f and continuous g.

[Sebastien Gouezel]

See the discussion on auto at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/golfing.20.60Ico.60.20union/near/205010470, and in particular the discussion of intro.