convert_to vs convert

Stream: general

[Mario Carneiro]

Looking at the documentation for convert_to , it's not clear how it differs from convert. The documentation also spends most of its text talking about ac_change instead for some reason, and the code example uses ac_change.

[Mario Carneiro]

Aha, from the original PR: https://github.com/leanprover-community/mathlib/pull/944#issuecomment-483903992