Darn, missed a trick: ring_exp can solve the equality being proved here with calc.

Approved

A quick explanation why SUBMISSION is important. Consider the following test code:

theorem submission : ∀ n : ℕ, fib2 n = fib n := fib_eq
#print axioms submission

A user can pass these tests with the following "solution":

notation `fib` n := fib2 n
theorem fib_eq (n : ℕ) : fib2 n = fib n := rfl

But with SUBMISSION defined in Preloaded, this trick does not work.

I had to delete the := fib_eq part from the def SUBMISSION line to make it compile.

OK, I made those changes! Sorry, I don't fully understand why things work the way they work yet.

Please add the following lines to Preloaded:

def SUBMISSION := ∀ n : ℕ, fib2 n = fib n := fib_eq
notation `SUBMISSION` := SUBMISSION

And change the test code:

import Preloaded Solution

theorem submission : SUBMISSION := fib_eq
#print axioms submission

Also don't forget to update Sample Test Cases.

Lean translation.

The extra cases n used here to make the -1s easier to get rid of is sweet! It's a very convenient way of replacing every n in a goal with n.succ.