[Merged by Bors] - feat(data/set/intervals/infinite): intervals are infinite

[rwbarton]

---

[PatrickMassot]

Should we have things like:

variables {α : Type*} [preorder α]

noncomputable
instance has_bot_of_finite [fintype α] [nonempty α] : has_bot α :=
⟨classical.some $ (fintype.well_founded_of_trans_of_irrefl _ : well_founded (@has_lt.lt α _)).has_min univ univ_nonempty⟩

lemma fintype.not_lt_bot [fintype α] [nonempty α] : ∀ x : α, ¬ x < ⊥ :=
begin
  classical,
  rcases classical.some_spec ((fintype.well_founded_of_trans_of_irrefl _ : well_founded (@has_lt.lt α _)).has_min univ univ_nonempty) with ⟨-, H⟩,
  exact λ x, H x trivial
end

(maybe not as a global instance) and the version with le for linear orders?

[jcommelin]

I think those should definitely not be global instances. Otherwise you'll get a lot of pain when using fin.

[jcommelin]

Suggested change

	refine hm ⟨z, hz₁, lt_trans hz₂ m.2.2⟩ trivial hz₂
	exact hm ⟨z, hz₁, lt_trans hz₂ m.2.2⟩ trivial hz₂

[jcommelin]

Suggested change

	refine hm ⟨z, lt_trans hz m.2⟩ trivial hz
	exact hm ⟨z, lt_trans hz m.2⟩ trivial hz

[jcommelin]

@PatrickMassot Would those definitions help in golfing these proofs?

[rwbarton]

I refactored the proofs along the general lines of Patrick's suggestion.

[fpvandoorn]

LGTM

bors merge

[jcommelin]

bors wake up

[jcommelin]

bors merge

[bryangingechen]

Hmm, bors seems to have crashed on this again. Third time's the charm?
bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests