Commit 2022-10-07 00:39 c4cf55bf

View on Github →

feat(Mathlib/Tactic/Contrapose): add contrapose tactic (#454) This ports contrapose and contrapose! as a collection of macro rules and provides a few basic tests.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/Contrapose.lean

added theorem Mathlib.Tactic.Contrapose.mtr

Created test/Contrapose.lean