Как доказать формулы математической индукции в программе доказательства теорем LEAN?

Вот мое доказательство. Для работы вам понадобится mathlib.

import algebra.big_operators tactic.ring

open finset

example (n : ℕ) : 2 * (range (n + 1)).sum id = n * (n + 1) :=
begin
  induction n with n ih,
  { refl },
  { rw [sum_range_succ, mul_add, ih, id.def, nat.succ_eq_add_one],
    ring }
end

range (n + 1) - это набор натуральных чисел меньше n + 1, то есть от 0 до n.

Я использовал функцию finset.sum. Если s - финсет, а f - функция, то s.sum f - это $ \ sum_ {x \ in s} f (x) $.

Тактика induction делает индукцию. Тогда есть два случая. Случай n = 0 может быть выполнен с refl, поскольку это не более чем вычисление.

Индуктивный шаг может быть выполнен с rw. Используя VSCode, вы можете щелкнуть после каждой запятой в моем доказательстве, чтобы увидеть, что делает каждый rw. Это придает форму, которую решит тактика ring.