Singleton bound linear

theorem singleton_bound_linear [CommRing F] [StrongRankCondition F]    (LC : LinearCode ι F) :    Module.finrank F LC ≤ card ι - (Code.dist LC.carrier) + 1 := by  classical  -- From the min-distance version and `Code.dist ≤ Code.minDist`.  have h1 : Module.finrank F LC ≤ card ι - Code.minDist (LC : Set (ι → F)) + 1 :=    singletonBound (LC := LC)  -- `dist ≤ minDist` since `= d` implies `≤ d` for witnesses  have hdist_le_min : Code.dist LC.carrier ≤ Code.minDist (LC : Set (ι → F)) := by    classical    let S₁ : Set ℕ := {d | ∃ u ∈ LC, ∃ v ∈ LC, u ≠ v ∧ hammingDist u v ≤ d}    let S₂ : Set ℕ := {d | ∃ u ∈ LC, ∃ v ∈ LC, u ≠ v ∧ hammingDist u v = d}    have hsub : S₂ ⊆ S₁ := by      intro d hd; rcases hd with ⟨u, hu, v, hv, hne, heq⟩; exact ⟨u, hu, v, hv, hne, by simp [heq]⟩    by_cases hne : (S₂ : Set ℕ).Nonempty    · have hLB : ∀ m ∈ S₂, sInf S₁ ≤ m := fun m hm => Nat.sInf_le (s := S₁) (hsub hm)      have := sInf.le_sInf_of_LB (S := S₂) hne hLB      simpa [Code.dist, Code.minDist, S₁, S₂] using this    · -- S₂ empty ⇒ S₁ empty as well      have hS₂empty : S₂ = (∅ : Set ℕ) := (Set.not_nonempty_iff_eq_empty).1 (by simpa using hne)      have hS₁empty : S₁ = (∅ : Set ℕ) := by        apply (Set.eq_empty_iff_forall_notMem).2        intro m hm        rcases hm with ⟨u, hu, v, hv, hne, hle⟩        have : hammingDist u v ∈ S₂ := ⟨u, hu, v, hv, hne, rfl⟩        simpa [hS₂empty, this]      simp [Code.dist, Code.minDist, S₁, S₂, hS₁empty, hS₂empty, Nat.sInf_empty]  -- Since a - b is antitone in b, add 1 afterwards  have hmono' : card ι - Code.minDist (LC : Set (ι → F)) + 1 ≤                 card ι - (Code.dist LC.carrier) + 1 := by    simpa [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using      (Nat.add_le_add_right (Nat.sub_le_sub_left hdist_le_min _) 1)  exact h1.trans hmono'