Is MDS of matrix Is MDS

lemma IsMDS_of_matrix_IsMDS [Field F] [DecidableEq F] {G : Matrix (Fin k) (Fin n) F}    (hMDS : Matrix.IsMDS G) (hkn : k ≤ n) (hk : 0 < k) : (fromRowGenMat G).IsMDS := by  have h_singleton_bound : (Module.finrank F (fromRowGenMat G)) ≤                           (Fintype.card (Fin n)) - (Code.dist (fromRowGenMat G).carrier) + 1 :=      LinearCode.singleton_bound_linear (fromRowGenMat G)  have h_rank_eq_k : (Module.finrank F (fromRowGenMat G)) = k := by    rw [← LinearCode.dim, dim_fromRowGenMat]    have h_rank : Matrix.rank (subLeftFull G (Fin.castLE hkn)) = k := by        apply Matrix.rank_eq_if_det_ne_zero        exact hMDS (⟨Fin.castLE hkn, Fin.castLE_injective hkn⟩)    convert Matrix.full_row_rank_via_rank_subLeftFull hkn h_rank using 1  have h_dist_ge : Code.dist (fromRowGenMat G).carrier ≥ n - k + 1 := by    have h_dist_ge : ∀ (c : Fin n → F), c ∈ fromRowGenMat G → c ≠ 0 → hammingNorm c ≥ n - k + 1 :=    by      apply_rules [minWt_ge_of_MDS]    refine le_csInf ?_ ?_;    · obtain ⟨u, hu⟩ : ∃ u : Fin n → F, u ∈ fromRowGenMat G ∧ u ≠ 0 := by        contrapose! h_rank_eq_k;        rw [show fromRowGenMat G = ⊥ from eq_bot_iff.mpr h_rank_eq_k]        simp only [Module.finrank_eq_zero_of_subsingleton, ne_eq]        linarith      exact ⟨_, ⟨u, hu.1, 0, by simp only [Submodule.carrier_eq_coe, SetLike.mem_coe, zero_mem],      hu.2, le_rfl⟩⟩    · rintro d ⟨u, hu, v, hv, huv, hd⟩      refine le_trans (h_dist_ge (u - v) ?_ ?_) ?_      · exact Submodule.sub_mem _ hu hv      · exact sub_ne_zero_of_ne huv      · simpa only [hammingNorm, hammingDist, Pi.sub_apply, sub_ne_zero] using hd  have h_dist_le : Code.dist (fromRowGenMat G).carrier ≤ n - k + 1 := by    contrapose! h_singleton_bound    rw [tsub_add_eq_add_tsub ]    · rw [tsub_lt_iff_left ] <;> norm_num      · linarith! [Nat.sub_add_cancel hkn]      · refine le_trans (Code.dist_le_card _) ?_        simp only [Fintype.card_fin, le_add_iff_nonneg_right, zero_le]    · convert Code.dist_le_card _  convert le_antisymm h_dist_le h_dist_ge using 1  unfold LinearCode.IsMDS  simp only [Submodule.carrier_eq_coe]  unfold length dim  simp [h_rank_eq_k]