In:
Game/Levels/L10Pset/L10Pset3.lean
Line 33:
have hc' : ∀ n, c n = b n * a n := by intro n; rewrite [hc]; ring_nf
is really not easy to guess based on what was covered up to this point. I had to ask Gemini what it's doing. An explicit hint may be needed.
In:
Game/Levels/L10Pset/L10Pset3.lean
Line 33:
have hc' : ∀ n, c n = b n * a n := by intro n; rewrite [hc]; ring_nf
is really not easy to guess based on what was covered up to this point. I had to ask Gemini what it's doing. An explicit hint may be needed.