Dim eq card of lt

lemma dim_eq_card_of_lt [Fintype ι] {α : ι ↪ F} (h : Fintype.card ι < n) :  LinearCode.dim (ReedSolomon.code α n) = Fintype.card ι := by  rw [LinearCode.dim]  let f := ReedSolomon.evalOnPoints (F := F) α  let S := Polynomial.degreeLT F n  have h_code : ReedSolomon.code α n = S.map f := rfl  rw [h_code]  have h_range : S.map f = LinearMap.range (f.domRestrict S) := by    ext    simp [Submodule.mem_map]  simp only [ModuleCode]  apply le_antisymm  · apply le_trans    · apply Submodule.finrank_le    · simp  · have h_sub : ReedSolomon.code α (Fintype.card ι) ≤ ReedSolomon.code α n :=      code_mono (le_of_lt h) α    have h_sub := Submodule.finrank_mono h_sub    have dim_eq := dim_eq_deg_of_le      (n := Fintype.card ι)      (α := α)      (by simp)    simp only [dim] at dim_eq    rw [dim_eq] at h_sub    exact h_sub