Dim eq deg of le

lemma dim_eq_deg_of_le [Fintype ι]  {α : ι ↪ F} (h : n ≤ Fintype.card ι) :  LinearCode.dim (ReedSolomon.code α n) = n := by  by_cases hcard : Fintype.card ι = 0  · aesop (add simp [      Module.finrank_eq_zero_of_subsingleton,      Fintype.card_eq_zero_iff,      ReedSolomon.code,      dim])  · 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]    rw [h_range, LinearMap.finrank_range_of_inj]    · rw [Polynomial.finrank_degreeLT_n]    · -- Injectivity proof      rw [←LinearMap.ker_eq_bot]      ext p      simp only [LinearMap.mem_ker, LinearMap.domRestrict_apply, Submodule.mem_bot]      constructor      · intro hfp        apply Subtype.ext        apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero' p.val (Finset.univ.map α)        · intro x hx          simp only [Finset.mem_map, Finset.mem_univ, true_and] at hx          rcases hx with ⟨i, rfl⟩          exact congr_fun hfp i        · simp only [Finset.card_map]          by_cases hn : n = 0          · subst hn            have h : ∀ i, p.val.coeff i = 0 := by              intro i              rcases p with ⟨p, hp⟩              simp [S, Polynomial.degreeLT] at hp              simp [hp i]            have h : p.val.natDegree = 0 := by              rw [Polynomial.natDegree_eq_zero_iff_degree_le_zero]              rw [Polynomial.degree_le_zero_iff]              ext n              rw [h n]              rcases n with _ | n <;> simp [h 0]            rw [h]            simp            omega          · calc p.val.natDegree < n              := @natDegree_lt_of_mem_degreeLT _ _ _ _ (⟨hn⟩) p.2                _ ≤ Fintype.card ι := h      · intro hfp        simp [hfp]