A large power modulo the square of eleven

(even if you do not know Fermat's little theorem but notice that $121=11^2$ )

$2014^{2015} = (1+183\cdot 11)^{2015}$

$= 1+ (2015)(183\cdot 11) + \dots (183\cdot 11)^2 + \dots$

(Higher order terms which has $11^2$ , hence divisible by 121)

Now all we have to do is to see that $2015 \cdot 183 \equiv 2 \cdot 7 \equiv 3 \bmod 11$

so the answer is

$= 1 + 3 \cdot 11 = 34$

Source: InternLM Lean-Workbook, record lean_workbook_10411 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.