Robotswana 9: hints not displayed because of unfold

[TentativeConvert]

The unfold in the line

Robo/Game/Levels/MatrixTrace/L09_EvalOnEBasis.lean

Line 51 in 2fff910

unfold E

is necessary to close the goal with simp. However, if the user does not unfold, the following hints will not be displayed!

[TentativeConvert]

Without the following hint, the students got themselves into a very intransparent situation, in which two sides of an equation looked identical on the screen but where not indentical to lean (rfl failed).

apply nat_mul_inj' (n := n.succ)
rw [←smul_eq_mul, ← LinearMap.map_smul]
trans f (∑ x : Fin n.succ, E i i)
simp
rw [← smul_eq_mul]
rw [← LinearMap.map_smul]
rw [←smul_eq_mul]
rfl

[joneugster]

I see, the intransparency is that the left the left • is for Mat[succ n, succ n][ℝ] as ℝ-module, while the right one is a scalar multiplication as Mat[succ n, succ n][ℝ]-module