rewrite cannot handle even the simplest of lemmas involving nat.rec

[JasonGross]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

@[simp]
def fact (n : ℕ) : ℕ :=
  nat.rec
    1
    (λ n' fact_n', (nat.succ n') * fact_n')
    n

universe u
@[simp]
def nat.rec_succ {P : ℕ → Type u} (o : P 0) (s : ∀ n, P n → P (nat.succ n)) (n : ℕ) : (nat.rec o s (nat.succ n) : P (nat.succ n)) = s n (nat.rec o s n) := rfl

example : fact 5 = 5 :=
begin
  simp [fact,has_mul.mul,nat.mul],
  rewrite [nat.rec_succ]
-- 15:3: failed
-- state:
-- ⊢ nat.rec 1 (λ (n' : ℕ), nat.mul (nat.succ n')) 5 = 5
end

Expected behavior: rewrite succeeds

Actual behavior: rewrite fails

Reproduces how often: [What percentage of the time does it reproduce?] 100%

Versions

$ lean --version
Lean (version 3.4.2, commit cbd2b6686ddb, Release)
$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 16.04.6 LTS
Release:        16.04
Codename:       xenial
$ uname -a
Linux jgross-Leopard-WS 4.4.0-161-generic #189-Ubuntu SMP Tue Aug 27 08:10:16 UTC 2019 x86_64 x86_64 x86_64 GNU/Linux

[JasonGross]

Note that making it non-dependent doesn't fix anything