Robotswana 9: hints not displayed because of unfold

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪

https://adam.math.hhu.de

Apache License 2.0

16 stars 9 forks source link

Robotswana 9: hints not displayed because of unfold #36

Open TentativeConvert opened 3 months ago

TentativeConvert commented 3 months ago

The unfold in the line https://github.com/hhu-adam/Robo/blob/2fff9106b1e4610acb25dd09d4dfd2e4319ac95a/Game/Levels/MatrixTrace/L09_EvalOnEBasis.lean#L51 is necessary to close the goal with simp. However, if the user does not unfold, the following hints will not be displayed!

TentativeConvert commented 3 months ago

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 commented 3 months ago

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