[Merged by Bors] - chore: remove unnecessary cdots#12417
[Merged by Bors] - chore: remove unnecessary cdots#12417
Conversation
grunweg
left a comment
There was a problem hiding this comment.
Thank you for doing this! The code changes look good to me; I trust you/the linter that all these instances actually have only a single goal active.
| apply add_lt_add | ||
| exact Nat.mul_self_lt_mul_self h | ||
| apply Nat.add_lt_add_right; assumption | ||
| · exact Nat.mul_self_lt_mul_self h |
There was a problem hiding this comment.
This is adding cdots (but looks like a good change regardless).
There was a problem hiding this comment.
You are right: I messed up with git and pulled in a change from the other PR that was adding the cdots.
| noncomputable instance _root_.Function.Embedding.fintype {α β} [Fintype α] [Fintype β] : | ||
| Fintype (α ↪ β) := | ||
| by classical. exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β) | ||
| by classical exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β) |
There was a problem hiding this comment.
That's a plus of looking at the SyntaxNodeKind, rather than what the user actually typed...
|
Thanks! bors merge |
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
These `·` are scoping when there is a single active goal. These were found using a modification of the linter at #12339.
|
Pull request successfully merged into master. Build succeeded: |
These `·` are scoping when there is a single active goal. These were found using a modification of the linter at #12339.
These `·` are scoping when there is a single active goal. These were found using a modification of the linter at #12339.
These
·are scoping when there is a single active goal.These were found using a modification of the linter at #12339.