Extra explanation might help for 0022 example in 02_iff_if_and.lean

[stanescuUW]

This is about the last example in 02_iff_if_and.lean. Lines 511-512 in the solutions file. The goal fact is immediately dispensed with by a simple rw. I would think a newcomer would expect the output of that rw ← dvd_gcd_iff to be gcd a b ∣ gcd a b. Instead, the rw dispenses with this trivial goal on the fly and closes the fact goal. It may be useful to explain why this happens in a few words to avoid undue confusion. dvd_refl is tagged with simp so the latter would close that gcd a b ∣ gcd a b, but why does the rw close it by itself?

[PatrickMassot]

I was confused for a while, see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/refl.20power. But this is indeed the usual stuff: rw always tries refl to close the goal after rewriting. I'm not sure what to say here. Do you have a wording suggestion?

It's interesting because this behavior of rw is one of the things that @kbuzzard changed in the NNG, hence offering a crippled rw for pedagogical purposes. And you seem to also think this is important. But I didn't see any issue with this when I used (almost) those files on real students.

[stanescuUW]

Maybe my wording was not clear enough, sorry for that. What I'm trying to say is that a newbie won't know that rw also closes refl goals. Not sure I can bet on this, but it was not mentioned in the tutorials up to that point, though it is standard behavior. So my suggestion would be to add a few words about that example 0022. Something like "Notice that, when working on the goal fact the rw tactic will invoke refl and hence close it. A separate use of refl is not needed. This is standard rw behavior."
Your students will benefit of your being there to clarify any questions. Users of the online tutorials might not have such advantage and may be puzzled by this. It will also be a nice clarification for those coming from the NNG.

[PatrickMassot]

This repository is now obsolete.