CA split rowwise implies CA

theorem CA_split_rowwise_implies_CA    {ϑ : ℕ} (u : WordStack A (Fin (2 ^ (ϑ + 1))) ι) (e : ℕ) :    let U₀ : WordStack A (Fin (2^ϑ)) ι := (splitHalfRowWiseInterleavedWords (ϑ := ϑ) u).1    let U₁ : WordStack A (Fin (2^ϑ)) ι := (splitHalfRowWiseInterleavedWords (ϑ := ϑ) u).2    jointProximityNat₂ (u₀ := ⋈|U₀) (u₁ := ⋈|U₁) (e := e) (C := C ^⋈ (Fin (2 ^ ϑ)))      → jointProximityNat (u := u) (e := e) (C := C) := by  -- 1. Unfold definitions  unfold jointProximityNat₂ jointProximityNat  simp only  set U₀ := (splitHalfRowWiseInterleavedWords (ϑ := ϑ) u).1  set U₁ := (splitHalfRowWiseInterleavedWords (ϑ := ϑ) u).2  conv_lhs => rw [Code.closeToCode_iff_closeToCodeword_of_minDist]  intro hCA_split_rowwise  rcases hCA_split_rowwise with ⟨vSplit, hvSplit_mem, hvSplit_dist_le_e⟩  -- ⊢ Δ₀(⋈|u, ↑(C ^⋈ (Fin (2 ^ (ϑ + 1))))) ≤ ↑e  rw [closeToWord_iff_exists_possibleDisagreeCols] at hvSplit_dist_le_e  rcases hvSplit_dist_le_e with ⟨D, hD_card_le_e, h_agree_outside_D⟩  conv_lhs => rw [←interleavedCode_eq_interleavedCodeSet (C := C)]  rw [Code.closeToCode_iff_closeToCodeword_of_minDist    (u := ⋈|u) (e := e) (C := C ^⋈ (Fin (2 ^ (ϑ + 1))))]  simp_rw [closeToWord_iff_exists_possibleDisagreeCols]  let VSplit_rowwise := Matrix.transpose vSplit  let VSplit₀_rowwise := Matrix.transpose (VSplit_rowwise 0)  let VSplit₁_rowwise := Matrix.transpose (VSplit_rowwise 1)  let v_rowwise_finmap : WordStack A (Fin (2 ^ (ϑ + 1))) ι :=    mergeHalfRowWiseInterleavedWords VSplit₀_rowwise VSplit₁_rowwise  let v_IC := ⋈| v_rowwise_finmap  use v_IC  constructor  · -- v_IC ∈ ↑(C ^⋈ (Fin (2 ^ (ϑ + 1))))    -- rw [interleavedCode_eq_interleavedCodeSet]    -- simp only [SetLike.mem_coe, mem_interleavedCode_iff]    intro rowIdx    have h_vSplit_rows_mem : ∀ (i : Fin 2) (j : Fin (2 ^ ϑ)), (fun col ↦ vSplit col i j) ∈ C := by      intro i      specialize hvSplit_mem i      exact hvSplit_mem    dsimp only [v_IC]    change v_rowwise_finmap rowIdx ∈ C    unfold v_rowwise_finmap mergeHalfRowWiseInterleavedWords    by_cases hk : rowIdx.val < 2 ^ ϑ    · simp only [hk, ↓reduceDIte]      exact h_vSplit_rows_mem 0 ⟨rowIdx.val, hk⟩    · simp only [hk, ↓reduceDIte]      exact h_vSplit_rows_mem 1 ⟨rowIdx.val - 2 ^ ϑ, by omega⟩    -- END OF MODIFIED SECTION  · use D    constructor    · exact hD_card_le_e    · intro colIdx h_colIdx_notin_D      funext rowIdx      dsimp only [v_IC]      change u rowIdx colIdx = v_rowwise_finmap rowIdx colIdx      have hRes := h_agree_outside_D colIdx (h_colIdx_notin_D)      simp_rw [funext_iff] at hRes      unfold v_rowwise_finmap mergeHalfRowWiseInterleavedWords      by_cases hk : rowIdx.val < 2 ^ ϑ      · simp only [hk, ↓reduceDIte]        exact hRes 0 ⟨rowIdx, by omega⟩      · simp only [hk, ↓reduceDIte]        change u rowIdx colIdx = vSplit colIdx 1 ⟨↑rowIdx - 2 ^ ϑ, by omega⟩        have hRes₁ := hRes 1 ⟨rowIdx - 2 ^ ϑ, by omega⟩        dsimp only [splitHalfRowWiseInterleavedWords, Fin.isValue, U₁] at hRes₁        rw [←hRes₁]        simp only [Interleavable.interleave, interleaveWordStack, finMapTwoWords,          Matrix.transpose_apply]        rw! [Nat.sub_add_cancel (h := by omega)]        rfl