linter.fugue.byCasesBang

by_cases h : p then push_neg at h is by_cases! h : p — the ! runs the push_neg itself. Same for by_contra / by_contra!.