[Merged by Bors] - chore(data/fintype): drop a decidable_pred assumption

[urkud]

OTOH, now the proof depends on classical.choice.

---

[vihdzp]

Why is this new proof so much longer than the old one? Can't you just do?

Suggested change

	fintype.of_bijective (sum.elim (coe : {b // b = a} → α) (coe : {b // b ≠ a} → α)) $
	by { classical, exact (equiv.sum_compl (= a)).bijective }
	by { classical, exact fintype.of_equiv _ (equiv.sum_compl (= a)) }

[urkud]

With my proof, it is clear that the "data" part of the definition does not depend on classical.choice. I don't know if your definition is computable.

[vihdzp]

This is just the old proof with classical slapped on top, so the data part should be computable as well.

[urkud]

Your definition is noncomputable. My definition still compiles if I remove type annotations from coe but I'm not sure how much this will affect readability.

[kmill]

Here is a bit more straightforward of an algorithm data-wise, but it still depends on classical.choice -- the goal is equivalent to x = a ∨ ¬x = a, and I wouldn't be surprised if LEM could be proved from this definition.

Suggested change

	fintype.of_bijective (sum.elim (coe : {b // b = a} → α) (coe : {b // b ≠ a} → α)) $
	by { classical, exact (equiv.sum_compl (= a)).bijective }
	⟨((finset.univ : finset {b // b ≠ a}).map (function.embedding.subtype _)).cons a (by simp),
	λ x, by { cases eq_or_ne x a; simp [*] }⟩

@vihdzp The reason it's not computable when you put classical at the beginning is that the generated term is of the form let I := foo in bar where foo is the noncomputable classical decidability instance.

[kmill]

Here is a bit more straightforward of an algorithm data-wise, but it still depends on classical.choice -- the goal is equivalent to x = a ∨ ¬x = a, and I wouldn't be surprised if LEM could be proved from this definition.

Suggested change

	fintype.of_bijective (sum.elim (coe : {b // b = a} → α) (coe : {b // b ≠ a} → α)) $
	by { classical, exact (equiv.sum_compl (= a)).bijective }
	⟨((finset.univ : finset {b // b ≠ a}).map (function.embedding.subtype _)).cons a (by simp),
	λ x, by { cases eq_or_ne x a; simp [*] }⟩

@vihdzp The reason it's not computable when you put classical at the beginning is that the generated term is of the form let I := foo in bar where foo is the noncomputable classical decidability instance.

[sgouezel]

bors r+
Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

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