Why does norm_num simplify these two values?

Stream: mathlib4

[Bolton Bailey]

Mwe:

import Mathlib.Data.Polynomial.Div

open scoped BigOperators Classical


def f (x : Fin 4) : Nat :=
  match x with
  | ⟨0, _⟩ => 1
  | ⟨1, _⟩ => 2
  | ⟨2, _⟩ => 3
  | ⟨3, _⟩ => 4

def g (h : 9 = ∑ x : Fin 4, f x) : false := by
  simp_rw [f] at h
  simp_rw [Fin.sum_univ_succ, Fin.sum_univ_zero] at h
  norm_num at h

results in the state

h: 9 =
  (match 0 with
    | { val := 0, isLt := isLt } => 1
    | { val := 1, isLt := isLt } => 2
    | { val := 2, isLt := isLt } => 3
    | { val := 3, isLt := isLt } => 4) +
    (2 +
      (3 +
        match Fin.succ 2 with
        | { val := 0, isLt := isLt } => 1
        | { val := 1, isLt := isLt } => 2
        | { val := 2, isLt := isLt } => 3
        | { val := 3, isLt := isLt } => 4))
⊢ false = true

Why does it only simply two of the four things I want simplified?

[Bolton Bailey]

(before the norm_num the matches are on Fin.succ 0, Fin.succ (Fin.succ 0) etc.)