Remove decide ... = true from Bool hypothesis

Stream: new members

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation
variable (M : Matrix (Fin m) (Fin n) Rat) (hm : m>0) (hn : n>0)

abbrev colListofMat := List.map List.ofFn (List.ofFn M.transpose)

def list_allZero (l : List Rat) : Bool := l.all (fun x => (x==0))

def findNonzCol : ℕ := (colListofMat M).findIdx (fun col => ¬ list_allZero col)

lemma findNonzCol_get_HasNonz (h : findNonzCol M < (colListofMat M).length) :
  ∃ x ∈ (colListofMat M).get ⟨findNonzCol M,h⟩, x≠0 := by
  have := List.findIdx_get (w:=h)

What can I do to to get rid of the decide ... = true in this?

[Yaël Dillies]

simp at this

[Vivek Rajesh Joshi]

It also simplifies some other definitions that I don't want simplified. How do I specifically simplify the decide part?

[Vivek Rajesh Joshi]

Nvm, simp? at this tells me what I want. Thanks anyways!