mathlib3
f74cc70c - fix(tactic/tauto): use intro1 to deal with negations (#1354)

Commit

6 years ago

fix(tactic/tauto): use intro1 to deal with negations (#1354) * fix(tactic/tauto): use intro1 to deal with negations * test(tactic/tauto): add tests

References

Author

robertylewis

Committer

mergify[bot]

Parents