Nice merge conflicts

Stream: general

[Yaël Dillies]

It's like the third time in a row that Yury adds the same lemma as me under the same name

<<<<<<< HEAD
lemma coe_pi_finset (t : Π a, finset (δ a)) :
  (fintype.pi_finset t : set (Π a, δ a)) = (set.univ : set α).pi (λ a, t a) :=
set.ext $ λ x, by { rw set.mem_univ_pi, exact fintype.mem_pi_finset }
=======
@[simp] lemma coe_pi_finset (t : Π a, finset (δ a)) :
  (pi_finset t : set (Π a, δ a)) = set.pi set.univ (λ a, t a) :=
by { ext, simp }
>>>>>>> origin/master

I'm starting to think people steal stuff from my branches :rofl:

[Yaël Dillies]

Genuinely though, this shows that our naming convention is very robust. We're one hive mind.

[Kevin Buzzard]

I was super-skeptical about the naming convention when I had it explained to me -- I was basically "just call everything lemma345345, it's no different, this isn't going to scale anyway". It scales much much further than I had imagined.

[Mario Carneiro]

I use duplicate definition errors as library_search