## Stream: general

### Topic: contrapose and push_neg

#### Johan Commelin (Aug 01 2019 at 19:09):

@Patrick Massot Thanks a lot for these tactics! They are really nice, and they allow one to reason like a real grown-up mathematician!

#### Patrick Massot (Aug 01 2019 at 21:14):

You're welcome! It's purely a product of my undergraduate teaching with Lean. Those tactics are indeed unavoidable if you want Lean proofs to look like real proofs (unfortunately they are far from sufficient).

#### Johan Commelin (Aug 02 2019 at 07:50):

Should exfalso take an optional argument?
I can imagine exfalso foo working like exfalso; refine foo.

Last updated: May 09 2021 at 19:11 UTC