Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: Match mathlib#16761 #840

Merged
merged 2 commits into from Dec 4, 2022
Merged

feat: Match mathlib#16761 #840

merged 2 commits into from Dec 4, 2022

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Dec 3, 2022 •
edited by Ruben-VandeVelde

I cannot figure out why this fails, but I'm sure someone will :^)

See leanprover-community/mathlib#16761.

@semorrison
Copy link
Contributor

Like the error message says, there is no refl tactic. It is called rfl now.

@semorrison
Copy link
Contributor

bors d+

Please merge once the mathlib3 PR is approved.

@bors
Copy link

bors bot commented Dec 4, 2022

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@semorrison semorrison merged commit e6628dd into master Dec 4, 2022
@bors bors bot deleted the mul_le_mul_iff_of_ge branch December 4, 2022 02:05
rosborn added a commit that referenced this pull request Dec 4, 2022
@rosborn
Merge branch 'master' into CategoryTheory.Functor.FullyFaithful
a57ac3a 
* master:
  chore: parallelize testing in CI (#845)
  feat: Match mathlib#17801 (#839)
  feat: Match mathlib#16761 (#840)
  feat: port CategoryTheory.NatIso (#820)
  feat: port algebra.ring.basic (#830)
  feat: port Combinatorics.Quiver.ConnectedComponent (#836)
  chore: bump to nightly-2022-12-03 (#838)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

Assignees
No one assigned
Labels
delegated
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@YaelDillies @semorrison @Ruben-VandeVelde