Basic.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiVerification.MathlibImports
7 
8 /-!
9 # Komorebi verification smoke theorems
10 
11 These declarations verify that Lean, Lake, and Mathlib can elaborate and check
12 small proofs in the project environment.
13 -/
14 
15 namespace KomorebiVerification
16 
17 /--
18 A small end-to-end check that the project can elaborate a theorem over the
19 reals and invoke a Mathlib normalization tactic.
20 -/
21 theorem binomialSquare (x y : ℝ) :
22     (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
23   ring
24 
25 /-- A second check exercising finite sums and arithmetic normalization. -/
26 theorem sumFirstOddNumbers (n : ℕ) :
27     ∑ k ∈ Finset.range n, (2 * k + 1) = n ^ 2 := by
28   induction n with
29   | zero => simp
30   | succ n ih =>
31       rw [Finset.sum_range_succ, ih]
32       ring
33 
34 end KomorebiVerification

Back to source controls