Gen matrix exists

lemma gen_matrix_exists [Field F] (LC : LinearCode ι F) :    ∃ (G : Matrix (Fin (dim LC)) ι F), LC = fromRowGenMat G := by  unfold fromRowGenMat  have LC_basis := Module.finBasis F LC  let G : Matrix (Fin (Module.finrank F ↥LC)) ι F :=    fun i => LC_basis i  use G  simp only [range_vecMulLinear, G, Matrix.row]  ext x  rw [Submodule.mem_span_range_iff_exists_fun]  constructor  · intros h    use LC_basis.equivFun ⟨x, h⟩    have x_to_lin_comb : (⟨x, h⟩ : LC).1 = ∑ i, LC_basis.equivFun ⟨x, h⟩ i • (LC_basis i).1 := by      rw (occs := .pos [1]) [←Module.Basis.sum_equivFun LC_basis ⟨x, h⟩, @Submodule.coe_sum]      congr    simp only [Module.Basis.equivFun_apply] at x_to_lin_comb ⊢    exact x_to_lin_comb.symm  · rintro ⟨x, h⟩    rw [←h]    apply Submodule.sum_smul_mem LC x    intros c _    exact Submodule.coe_mem (LC_basis c)