Joint Agreement implies lin Span proximity

theorem jointAgreement_implies_linSpan_proximity {ι : Type} [Fintype ι] [Nonempty ι]    {F : Type} [Field F] [DecidableEq F] {k : ℕ}    (C : Submodule F (ι → F)) {δ : ℝ≥0} {W : Fin k → ι → F}    (h : jointAgreement (C := (C : Set (ι → F))) (δ := δ) (W := W)) :    ∀ x ∈ Submodule.span F (Set.range W), δᵣ(x, (C : Set (ι → F))) ≤ δ := by  rcases h with ⟨S, hS_card, v, hv⟩  intro x hx  rw [Submodule.mem_span_range_iff_exists_fun] at hx  rcases hx with ⟨c, rfl⟩  set v' : ι → F := ∑ i : Fin k, c i • v i with hv'_def  have hv'_mem : v' ∈ C := by    refine Submodule.sum_mem C (fun i _ => ?_)    exact Submodule.smul_mem C (c i) (hv i).1  have hagree : ∀ j ∈ S, (∑ i, c i • v i) j = (∑ i, c i • W i) j := by    intro j hj    simp only [Finset.sum_apply, Pi.smul_apply]    refine Finset.sum_congr rfl (fun i _ => ?_)    have h_j_in_filter : j ∈ Finset.filter (fun j => v i j = W i j) Finset.univ :=      (hv i).2 hj    have : v i j = W i j := by simpa [Finset.mem_filter] using h_j_in_filter    rw [this]  have hdist : δᵣ(∑ i, c i • W i, v') ≤ δ := by    rw [Code.relCloseToWord_iff_exists_agreementCols      (u := ∑ i, c i • W i) (v := v') (δ := δ)]    refine ⟨S, ?_, ?_⟩    · have hS' : (1 - δ) * (Fintype.card ι : ℝ≥0) ≤ (S.card : ℝ≥0) := by        simpa [ge_iff_le, mul_comm, mul_left_comm, mul_assoc] using hS_card      exact (Code.relDist_floor_bound_iff_complement_bound (n := Fintype.card ι)        (upperBound := S.card) (δ := δ)).2 hS'    · intro j      constructor      · intro hj        exact (hagree j hj).symm      · intro hj_ne hj        exact hj_ne (hagree j hj).symm  exact    (Code.relCloseToCode_iff_relCloseToCodeword_of_minDist      (u := ∑ i, c i • W i) (C := (C : Set (ι → F))) (δ := δ)).2      ⟨v', hv'_mem, hdist⟩