golf: use compute_degree_le to simplify two proofs#5883
Closed
golf: use compute_degree_le to simplify two proofs#5883
compute_degree_le to simplify two proofs#5883Conversation
1 task
compute_degree_le to restore a mathlib3 proofcompute_degree_le to simplify two proofs
|
This PR/issue depends on:
|
Add docs, remove tests from Tactic file. Improve docs in tests. Add degree disclaimer Fix issue with 1. Add pre-existing ml3 tests. Use compute_degree_le, remove porting note Add debug-mode and a few explicit terms Parse optional `!`. Use MVarIds Remove unneeded deg-->natDeg lemma Update Mathlib/Tactic/ComputeDegree.lean Update Mathlib/Tactic/ComputeDegree.lean Update Mathlib/Tactic/ComputeDegree.lean Update Mathlib/Tactic/ComputeDegree.lean Update Mathlib/Tactic/ComputeDegree.lean Update Mathlib/Tactic/ComputeDegree.lean Update Mathlib/Tactic/ComputeDegree.lean Extract `getPolsName` from `cDegCore` Adjust `open`s and `section` Fix typo Error golf Cosmetic changes Golf? Symmetric support for natDegree and degree Trivial lemmas for compute_degree_le Restore newer "all" files Rename lemmas Section PRed lemmas Partial introduction of DegInfo More tests with Ring Streamline and golf from cdle_dev Add repeated `OfNat` test
a0de17f to
bc068bc
Compare
Contributor
Author
|
This PR was a sample usage of a tactic |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR simply uses the tactic
compute_degree_lefrom #5882 to remove golf two proofs.One of the two proofs was the only
mathlib3use ofcompute_degree_leand the new tactic removes a porting note.compute_degree_le#5882, where the tacticcompute_degree_leis defined