Dist interleaved code to code lb

lemma dist_interleaved_code_to_code_lb    {L : LinearCode ι F} {U_star : WordStack (A := F) κ ι}    {e : ℕ}    (hF : Fintype.card F > e)    (he : (e : ℚ≥0) < ‖(L : Set (ι → F))‖₀ / 3)    (hU : e < Δ₀(⋈|U_star, L^⋈κ)) :    ∃ v ∈ Matrix.rowSpan U_star, e < Δ₀(v, L) := by  classical  have h3e_lt_d : 3 * e < ‖(L : Set (ι → F))‖₀ := by    have h3pos : (0 : ℚ≥0) < 3 := by norm_num    have h' : (3 : ℚ≥0) * (e : ℚ≥0) < (‖(L : Set (ι → F))‖₀ : ℚ≥0) := by      have hmul := mul_lt_mul_of_pos_left he h3pos      have h3ne : (3 : ℚ≥0) ≠ 0 := by norm_num      have h3mul :          (3 : ℚ≥0) * (‖(L : Set (ι → F))‖₀ : ℚ≥0) / 3 =            ‖(L : Set (ι → F))‖₀ := by        simp [h3ne]      have : (3 : ℚ≥0) * (‖(L : Set (ι → F))‖₀ : ℚ≥0) / 3 =          (3 : ℚ≥0) * ((‖(L : Set (ι → F))‖₀ : ℚ≥0) / 3) := by        simpa [mul_div_assoc] using          (mul_div_assoc (3 : ℚ≥0) (‖(L : Set (ι → F))‖₀ : ℚ≥0) (3 : ℚ≥0))      have h3mul' :          (3 : ℚ≥0) * ((‖(L : Set (ι → F))‖₀ : ℚ≥0) / 3) =            ‖(L : Set (ι → F))‖₀ := by        simpa [this] using h3mul      simpa [h3mul'] using hmul    exact_mod_cast h'  have h2e_lt_d : 2 * e < ‖(L : Set (ι → F))‖₀ := by omega  by_contra h_contra  push Not at h_contra  have h_close (v : Matrix.rowSpan U_star) :      Δ₀((v : ι → F), (L : Set (ι → F))) ≤ e :=    h_contra v v.property  have h_exists_codeword (v : Matrix.rowSpan U_star) :      ∃ c ∈ (L : Set (ι → F)), Δ₀((v : ι → F), c) ≤ e := by    simpa using      (Code.closeToCode_iff_closeToCodeword_of_minDist (u := (v : ι → F))        (C := (L : Set (ι → F))) (e := e)).1 (h_close v)  choose dec hdec_mem hdec_dist using h_exists_codeword  have hdec_add (v w : Matrix.rowSpan U_star) : dec (v + w) = dec v + dec w := by    apply Code.eq_of_lt_dist (C := (L : Set (ι → F)))    · exact hdec_mem (v + w)    · exact Submodule.add_mem _ (hdec_mem v) (hdec_mem w)    · have h1 : Δ₀(dec (v + w), (v + w : ι → F)) ≤ e := by        simpa [hammingDist_comm] using hdec_dist (v + w)      have h2 : Δ₀((v + w : ι → F), dec v + dec w) ≤ 2 * e := by        have hv :            Δ₀((v + w : ι → F), (v : ι → F) + dec w) = Δ₀((w : ι → F), dec w) := by          change Δ₀((fun i => (v : ι → F) i + (w : ι → F) i),            fun i => (v : ι → F) i + dec w i) = Δ₀((w : ι → F), dec w)          exact hammingDist_comp (f := fun i ↦ fun t : F ↦ (v : ι → F) i + t)              (x := (w : ι → F)) (y := dec w)              (hf := fun _ ↦ by                intro a b hab                exact add_left_cancel hab)        have hw :            Δ₀((v : ι → F) + dec w, dec v + dec w) = Δ₀((v : ι → F), dec v) := by          change Δ₀((fun i => (v : ι → F) i + dec w i),            fun i => dec v i + dec w i) = Δ₀((v : ι → F), dec v)          exact hammingDist_comp (f := fun i ↦ fun t : F ↦ t + dec w i)              (x := (v : ι → F)) (y := dec v)              (hf := fun _ ↦ by                intro a b hab                exact add_right_cancel hab)        have : Δ₀((v + w : ι → F), dec v + dec w)            ≤ Δ₀((v + w : ι → F), (v : ι → F) + dec w)              + Δ₀((v : ι → F) + dec w, dec v + dec w) := by          exact hammingDist_triangle (v + w : ι → F) ((v : ι → F) + dec w) (dec v + dec w)        calc          Δ₀((v + w : ι → F), dec v + dec w)              ≤ Δ₀((v + w : ι → F), (v : ι → F) + dec w)                + Δ₀((v : ι → F) + dec w, dec v + dec w) := this          _   = Δ₀((w : ι → F), dec w) + Δ₀((v : ι → F), dec v) := by              simp [hv, hw, add_comm]          _   ≤ e + e := Nat.add_le_add (hdec_dist w) (hdec_dist v)          _   = 2 * e := by ring      have h3 : Δ₀(dec (v + w), dec v + dec w) ≤ 3 * e := by        calc          Δ₀(dec (v + w), dec v + dec w)              ≤ Δ₀(dec (v + w), (v + w : ι → F))                + Δ₀((v + w : ι → F), dec v + dec w) := by                  exact                    hammingDist_triangle (dec (v + w)) (v + w : ι → F) (dec v + dec w)          _   ≤ e + 2 * e := Nat.add_le_add h1 h2          _   = 3 * e := by ring      exact lt_of_le_of_lt h3 h3e_lt_d  have hdec_smul (a : F) (v : Matrix.rowSpan U_star) : dec (a • v) = a • dec v := by    apply Code.eq_of_lt_dist (C := (L : Set (ι → F)))    · exact hdec_mem (a • v)    · exact Submodule.smul_mem _ a (hdec_mem v)    · have h1 : Δ₀(dec (a • v), (a • v : ι → F)) ≤ e := by        simpa [hammingDist_comm] using hdec_dist (a • v)      have h2 : Δ₀((a • v : ι → F), a • dec v) ≤ e := by        have := hammingDist_smul_le_hammingDist (k := a) (x := (v : ι → F)) (y := dec v)        exact le_trans this (hdec_dist v)      have h3 : Δ₀(dec (a • v), a • dec v) ≤ 2 * e := by        calc          Δ₀(dec (a • v), a • dec v)              ≤ Δ₀(dec (a • v), (a • v : ι → F))                  + Δ₀((a • v : ι → F), a • dec v) := by                exact hammingDist_triangle (dec (a • v)) (a • v : ι → F) (a • dec v)          _   ≤ e + e := Nat.add_le_add h1 h2          _   = 2 * e := by ring      exact lt_of_le_of_lt h3 h2e_lt_d  let decLin : Matrix.rowSpan U_star →ₗ[F] (ι → F) :=    { toFun := dec, map_add' := hdec_add, map_smul' := hdec_smul }  let err : Matrix.rowSpan U_star →ₗ[F] (ι → F) :=    Submodule.subtype (Matrix.rowSpan U_star) - decLin  have herr_wt (x : LinearMap.range err) :      (vecSupport (F := F) (x : ι → F)).card ≤ e := by    rcases x.property with ⟨v, hv⟩    have h_supp :        (vecSupport (F := F) ((err v) : ι → F)).card = Δ₀((v : ι → F), dec v) := by      simp [err, decLin, vecSupport_sub, hammingDist]    simpa [hv.symm, h_supp] using hdec_dist v  obtain ⟨D, hD_card, hD_zero⟩ :=    exists_common_support_of_wt_le (F := F) (ι := ι) (E := LinearMap.range err) (e := e)      herr_wt hF  have h_row_in_span (k : κ) : U_star k ∈ Matrix.rowSpan U_star := by    unfold Matrix.rowSpan    exact Submodule.subset_span ⟨k, rfl⟩  let V : WordStack (A := F) κ ι := fun k ↦ dec ⟨U_star k, h_row_in_span k⟩  have hV_mem : (⋈|V) ∈ (L^⋈κ) := by    refine (Code.mem_moduleInterleavedCode_iff (F := F) (A := F) (κ := κ) (ι := ι) (MC := L)      (v := (⋈|V))).2 ?_    intro k    simpa [V] using hdec_mem ⟨U_star k, h_row_in_span k⟩  have h_dist_rows : ∀ k j, j ∉ D → U_star k j = V k j := by    intro k j hj    have hz :        (err ⟨U_star k, h_row_in_span k⟩ : ι → F) j = 0 := by      have : (err ⟨U_star k, h_row_in_span k⟩) ∈ LinearMap.range err :=        ⟨⟨U_star k, h_row_in_span k⟩, rfl⟩      exact hD_zero ⟨err ⟨U_star k, h_row_in_span k⟩, this⟩ j hj    have : (U_star k j : F) - V k j = 0 := by      simpa [err, decLin, V, Pi.sub_apply] using hz    exact sub_eq_zero.mp this  have hUV_le : Δ₀(⋈|U_star, ⋈|V) ≤ e := by    refine le_trans      (hamming_dist_le_of_subset_disagree (ι := ι) (u := (⋈|U_star)) (v := (⋈|V))        (D := D) ?_)      hD_card    intro j hj    by_contra hjD    apply hj    funext k    have := h_dist_rows k j hjD    simpa [V] using this  have h_dist_to_code : Δ₀(⋈|U_star, (L^⋈κ)) ≤ e := by    exact le_trans      (Code.distFromCode_le_dist_to_mem (C := (L^⋈κ)) (u := (⋈|U_star)) (v := (⋈|V))        hV_mem)      (by exact_mod_cast hUV_le)  exact (not_lt_of_ge h_dist_to_code) hU