application type mismatch error

Stream: mathlib4

[Jihoon Hyun]

I am working on is_special_iff for #1408.
The code is as follows:

theorem is_special_iff : u.is_special ↔ u.is_special' := by
  dsimp [is_special, is_special']
  constructor <;> intro h
  . simp_arith [mul_coe u.w u.z, w, z, succPNat, ← h]
    repeat' rw [Nat.succ_eq_add_one]
    simp only [mul_eq]; ring
  . apply Nat.succ.inj
    replace h := congr_arg (Coe.coe : ℕ+ → ℕ) h
    simp only [w, z] at h
    unfold Coe.coe coePNatNat at h
    simp at h; rw [Nat.mul_succ, Nat.succ_mul] at h
    rw [Nat.add_comm _ (succ u.wp), Nat.add_comm _ u.zp, ← Nat.add_assoc _ u.zp _] at h
    rw [Nat.succ_add u.wp, Nat.succ_add] at h
    exact h
#align pnat.xgcd_type.is_special_iff PNat.XgcdType.is_special_iff

I believe that the proof is done, but there is a error application type mismatch, saying that

argument has type
  { x // 0 < x }
but function has type
  ℕ → List ℕ → List ℕ

What should be the problem here?

[Jihoon Hyun]

I fixed the error. For some reason simp_arith does not work properly.