How do I do back? and by_contradiction in Lean 4?

Stream: lean4

[Mr Proof]

I just watched this video https://www.youtube.com/watch?v=ArGLTAjak3g
And it uses things like "back?" and "by_contradiction"

How do you do these two things in Lean 4?

[llllvvuu]

by_contra

re: back?, see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/What.20are.20Lean's.20biggest.20issues.3F/near/203963834, which mentions solve_by_elim and apply_rules; you can also use aesop, apply?

[Kim Morrison]

back? sadly was a bit of cheat, in the sense that it was never released. aesop is what you're looking for today!