Proof of Cassini's identity in Lean 3

cassini.lean

import data.nat.fib
import data.matrix.basic
import data.matrix.notation
import linear_algebra.matrix.determinant

theorem matrix.map_pow {m α β : Type*} [fintype m] [decidable_eq m] [semiring α]
                       {M : matrix m m α} {n : ℕ} [semiring β] {f : α →+* β} :
  (M ^ n).map ⇑f = (M.map ⇑f) ^ n :=
begin
  induction n,
  simp,
  { rw pow_succ, rw pow_succ, simp, rw n_ih },
end

lemma fib_matrix (n : ℕ) {hn : n > 0} :
  !![1, 1; 1, 0] ^ n = !![nat.fib (n+1), nat.fib n; nat.fib n, nat.fib (n-1)] :=
begin
  cases n,
  exfalso,
  exact nat.lt_asymm hn hn,

  induction n with nn hi,
  simp,

  rw pow_succ,
  rw hi,
  simp,
  nth_rewrite 0 nat.add_comm,
  rw ←nat.fib_add_two,
  nth_rewrite 1 nat.add_comm,
  rw ←nat.fib_add_two,

  exact nat.zero_lt_succ nn,
end

lemma fib_cassini (n : ℕ) {hn : n > 0} :
  ↑(nat.fib (n+1) * nat.fib (n-1)) - ↑(nat.fib n ^ 2) = (-int.one) ^ n :=
begin
  transitivity (matrix.map !![nat.fib (n+1), nat.fib n; nat.fib n, nat.fib (n-1)] (nat.cast_ring_hom ℤ)).det,
  rw matrix.det_fin_two,
  simp,
  ring,
  rw ←@fib_matrix n hn,
  rw matrix.map_pow,
  rw matrix.det_pow,
  rw matrix.det_fin_two,
  simp,
  refl,
end