I will describe a problem which I have in fact solved, but with considerable pain. My question is whether there are better methods for dealing with similar issues.
Lean was giving me messages that did not seem to make sense. After various manoeuvres to try to simplify and isolate the problem, I got a message like this (in which
k are all natural numbers).
invalid type ascription, term has type (n1 * r) ^ k = n1 ^ k * r ^ k but is expected to have type (n1 * r) ^ k = ?m_1
Visually, it appears that the term
h = mul_pow n1 r k in question has precisely the expected type, so this message is confusing. Eventually I entered
set_option pp.all true, and thereby got a much longer and more explicit version of the above message. From this I saw that in the goal, multiplication and powers were defined in the usual way for natural numbers. However, in the term
h there was all sorts of stuff about linear orders that I did not expect. I later worked out that I had inadvertently given
ℕ an alternative monoid structure based on its structure as a lattice under the divisibility relation, and that that had been used by
mul_pow when I defined
h. After removing the import that defined this unwanted instance, the problem went away.
a ^ 2 = a ^ 2by
refl, only to realize after some head scratching that
2 : ℕyet
2 : ℝ! Right now,
set_option pp.numerals falseis a way to debug that one. $\endgroup$