Min Wt ge of MDS

lemma minWt_ge_of_MDS [Field F] [DecidableEq F] {G : Matrix (Fin k) (Fin n) F}(hMDS : Matrix.IsMDS G) {c : Fin n → F} (hc_mem : c ∈ fromRowGenMat G) (hc_ne : c ≠ 0) :    n - k + 1 ≤ hammingNorm c := by  have h_hamming_norm : n - Finset.card (Finset.filter (fun j => c j = 0) Finset.univ)    ≥ n - k + 1 :=  by    rcases le_or_gt k (Finset.card (Finset.filter (fun j => c j = 0) Finset.univ))            with h | h <;> simp only [ge_iff_le, Order.add_one_le_iff]    · have h_contra : ∃ σ : Fin k ↪ Fin n, ∀ j, c (σ j) = 0 := by        obtain ⟨s, hs⟩ : ∃ s : Finset (Fin n), s.card = k ∧ ∀ j ∈ s, c j = 0 := by          exact Exists.elim (Finset.exists_subset_card_eq h) fun s hs => ⟨s, hs.2, fun j hj =>          Finset.mem_filter.mp ( hs.1 hj ) |>.2⟩        exact ⟨⟨fun j => s.orderEmbOfFin (by aesop) j, fun j j' h => by aesop⟩,          fun j => hs.2 _ (by aesop)⟩      obtain ⟨σ, hσ⟩ := h_contra      have h_det : Matrix.det (Matrix.submatrix G id σ) = 0 := by        have h_contra : ∃ v : Fin k → F, v ≠ 0 ∧ Matrix.vecMul v (Matrix.submatrix G id σ) = 0 := by          obtain ⟨v, hv⟩ := hc_mem          refine ⟨v, ?_, ?_⟩ <;> contrapose! hc_ne <;> simp_all +decide [funext_iff, Matrix.vecMul]          grind        exact Matrix.exists_vecMul_eq_zero_iff.mp h_contra;      have := hMDS σ      aesop    · refine Nat.sub_lt_sub_left ?_ h      by_contra h_contra      exact hc_ne (funext fun j => by_contradiction fun hj =>      h_contra <| lt_of_lt_of_le (Finset.card_lt_card <| Finset.filter_ssubset.mpr ⟨j, by aesop⟩)      <| by simp only [Finset.card_univ, Fintype.card_fin, le_refl])  convert h_hamming_norm.le using 1  simp [hammingNorm, Finset.filter_not, Finset.card_sdiff]