Finding entry of a matrix with "minimal euclidean valuation"

Stream: new members

[Jamie Reason]

Hey, I'm trying to show there exists a non-zero element of a non-zero matrix with "minimal valuation" (in the sense of the euclidean valuation function). Lean seems to use an equivalence instead of a valuation where if δ was a valuation function, the relation ≺ (euclidean_domain.r) would have property a ≺ b ↔ δ(a) < δ(b).
The exact lemma I want to show is

lemma min_valuation_of_mat {D : Type*} [euclidean_domain D] {n : ℕ} (A : matrix (fin n) (fin n) D) (h : A ≠ 0) :
∃ (k l : fin n), ∀ (i j : fin n), (A k l ≠ 0) ∧ ( A i j ≠ 0 → ¬((A i j) ≺ (A k l)) ) := sorry

The pencil and paper proof would be that there must exist a non-zero element (but finitely many) so pick an arbitrary one a and it either has the property or another element exists b with a "smaller valuation", or with the relation that would be b ≺ a. Since finite number of entries, this must terminate.

Does anybody have any good places to start with this? I've tried using by_contra and push_neg but they seem to not progress it.

Notes: although I have not shown the following lemmas, assume they can be used (I believe they should all hold, let me know if you think they don't),

lemma lt_trans {D : Type*} [euclidean_domain D] : ∀ {a b c : D}, (a ≺ b) → (b ≺ c) → (a ≺ c) := λ a b c hab hbc, by sorry
lemma gt_not_eq_zero {D : Type*} [euclidean_domain D] : ∀ {a b : D}, a ≺ b → b ≠ 0 := λ a b, by sorry
lemma irrefl {D : Type*} [euclidean_domain D] : ∀ {a : D}, ¬ (a ≺ a) := λ a, by sorry
lemma asymm {D : Type*} [euclidean_domain D] : ∀ {a b : D}, (a ≺ b) → ¬(b ≺ a) := λ a b hab, by sorry

(assumue in euclidean_domain namespace)

[Junyan Xu]

You may use dos#finset.filter to filter out the zero entries from finset.univ : finset (fin n × fin n), then you can just use docs#finset.min', and then finset.min'_le and finset.min'_mem give you its desired properties. You do need that the filtered finset is nonempty and that the order is linear. For general preorders, use docs#finset.exists_minimal.