[Merged by Bors] - feat(computability/language): le on languages

[foxthomson]

---

• depends on: feat(data/list/backwards): backwards recursors on lists #5700

[foxthomson]

I used set's has_le, will this cause problems later on, I had to use set.le_eq_subset as the first step a bit which felt odd.

[gebner]

I used set's has_le, will this cause problems later on, I had to use set.le_eq_subset as the first step a bit which felt odd.

In many cases you don't need to unfold this definition explicitly. Try deleting the rw set.le_eq_subset, most of your proofs still work fine without it.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• feat(data/list/backwards): backwards recursors on lists #5700

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[gebner]

bors d+

[bors]

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

[foxthomson]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests