∀ {n : Type u_2} {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (P : Matrix n n 𝕜 → Prop)
  (M : Matrix n n 𝕜),
  M.det ≠ 0 →
    (∀ (D : n → 𝕜), (Matrix.diagonal D).det ≠ 0 → P (Matrix.diagonal D)) →
      ∀ (D : n → 𝕜), (Matrix.diagonal D).det = M.det → (fun N => N.det ≠ 0 ∧ P N) (Matrix.diagonal D)