mathlib

486830b0 - feat(tactic/choose): `choose` can now decompose conjunctions (#3699)