кто совсем не знает Lean и готов потратить два часа на развлечение (в самом низу там ссылка на онлайн версию Lean) с ним: знать ничего не нужно, просто наводите курсор на текст или двигаете текстовый курсор и смотрите, как меняются переменные справа (я то же самое пытался в Visual Studio делать, но иногда ерунда какая-то выходила — видимо, другая версия Lean. С другой стороны, Copilot нехило так подсказывает, что вообще ничего делать не надо (когда работает). А иногда не компилится и хрен знает почему). за два часа можно освоить как доказываются простые факты про пределы последовательностей вещественных чисел. В общем, это иллюстрация, что такое Тактики в Lean. Я помню, таким же образом когда-то Python учил, когда сразу дают программу, и, в ней разбираясь, изучаешь язык.