Matrix Is MDS of Is MDS

lemma matrix_IsMDS_of_IsMDS [Field F] [DecidableEq F] {G : Matrix (Fin k) (Fin n) F}    (hCode : (fromRowGenMat G).IsMDS) (hrank : G.rank = k) : Matrix.IsMDS G := by  contrapose! hCode  simp_all only [Matrix.IsMDS, ne_eq, not_forall, Decidable.not_not]  obtain ⟨σ, hσ⟩ := hCode  obtain ⟨v, hv⟩ : ∃ v : Fin k → F, v ≠ 0 ∧ Matrix.vecMul v (G.submatrix id σ) = 0 :=    exists_vecMul_eq_zero_iff.mpr hσ  set c : Fin n → F := v ᵥ* G  have hc_ne_zero : c ≠ 0 := by    have h_inj : Function.Injective (Matrix.vecMulLinear G) := by      apply vecMul_injective_of_rank_eq      assumption    exact fun h => hv.1 (h_inj <| by simpa using h)  have hc_in_code : c ∈ fromRowGenMat G := ⟨v, rfl⟩  have hc_norm : hammingNorm c ≤ n - k := by    have hc_norm : ∀ j : Fin k, c (σ j) = 0 := by      intro j      specialize hv      replace hv := congr_fun hv.2 j      aesop    have hc_norm :    Finset.card (Finset.univ.filter (fun i => c i ≠ 0)) ≤    Finset.card (Finset.univ \ Finset.image σ Finset.univ) :=      Finset.card_le_card fun i hi => by aesop    simp_all only [ne_eq, Finset.card_sdiff, Finset.card_univ, Fintype.card_fin,      Finset.inter_univ, Finset.card_image_of_injective _ σ.injective, ge_iff_le]    exact hc_norm  have h_dist_le_norm : Code.dist (fromRowGenMat G).carrier ≤ hammingNorm c := by    refine Nat.sInf_le ⟨c, hc_in_code, 0, ?_, ?_, ?_⟩ <;> simp [hc_ne_zero]  unfold LinearCode.IsMDS  simp_all only [ne_eq, Code.dist, Submodule.carrier_eq_coe,    SetLike.mem_coe]  refine ne_of_lt (lt_of_le_of_lt h_dist_le_norm (lt_of_le_of_lt hc_norm ?_))  simp [length, dim_fromRowGenMat, hrank]