Multilinear Combine recursive form

lemma multilinearCombine_recursive_form    {ϑ : ℕ} (u : WordStack A (Fin (2 ^ (ϑ + 1))) ι) (r : Fin (ϑ + 1) → F) :  let U₀ := (splitHalfRowWiseInterleavedWords (ϑ := ϑ) u).1  let U₁ := (splitHalfRowWiseInterleavedWords (ϑ := ϑ) u).2  let r_init : Fin (ϑ) → F := Fin.init r  multilinearCombine (u:=u) (r:=r) = multilinearCombine (ϑ := ϑ) (u:=    affineLineEvaluation (F := F) (u₀ := U₀) (u₁ := U₁) (r := r (Fin.last ϑ))) (r:=r_init) := by  -- 1. Unfold definitions and prove equality component-wise for each column index.  funext colIdx  simp only [multilinearCombine]  have h_2_pow_ϑ_succ : 2 ^ (ϑ + 1) = 2 ^ (ϑ) + 2 ^ (ϑ) := by    exact Nat.two_pow_succ ϑ  rw! (castMode := .all) [h_2_pow_ϑ_succ]  conv_lhs => -- split the sum in LHS over (fin (2 ^ (ϑ + 1))) into two sums over (fin (2 ^ (ϑ)))    rw [Fin.sum_univ_add (a := 2 ^ (ϑ)) (b := 2 ^ (ϑ))]    simp only [Fin.natAdd_eq_addNat]    -- 2. Simplify LHS using definitions of U₀ and U₁  simp only [splitHalfRowWiseInterleavedWords]  -- We also need to unfold U₀ and U₁ on the RHS.  -- 3. Unfold RHS and distribute the sum  simp only [affineLineEvaluation, Pi.add_apply, Pi.smul_apply, smul_add, smul_smul,    sum_add_distrib]  -- 4. Combine sums on LHS & RHS  rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]  -- 5. Show equality inside the sum  apply Finset.sum_congr rfl  intro i _ -- `i` is the row index `Fin (2 ^ ϑ)`  simp_rw [eqRec_eq_cast]  rw! [←Fin.cast_eq_cast (h := by omega)]  -- 6. Prove the two core multilinearWeight identities  -- These are the key `Nat.getBit` facts.  let r_init := Fin.init r  -- 7. Apply the identities to finish the proof  -- The goal is now `... • U₀ i colIdx + ... • U₁ i colIdx = ... • U₀ i colIdx + ... • U₁ i colIdx`  have h_fin_cast_castAdd: Fin.cast (eq := by omega) (i := Fin.castAdd (n := 2 ^ ϑ)    (m := 2 ^ ϑ) i) = (⟨i, by omega⟩ : Fin (2 ^ (ϑ + 1))) := by rfl  have h_fin_cast_castAdd_2: Fin.cast (eq := by omega)    (i := i.addNat (2 ^ ϑ)) = (⟨i + 2 ^ ϑ, by omega⟩ : Fin (2 ^ (ϑ + 1))) := by rfl  rw [h_fin_cast_castAdd, h_fin_cast_castAdd_2]  have h_getLastBit : Nat.getBit (Fin.last ϑ) i = 0 := by    have h := Nat.getBit_of_lt_two_pow (a := i) (k := Fin.last ϑ)    simp only [Fin.val_last, lt_self_iff_false, ↓reduceIte] at h    exact h  have h_i_and_2_pow_ϑ : i.val &&& (2 ^ ϑ) = 0 := by    apply Nat.and_two_pow_eq_zero_of_getBit_0 (n := i) (i := ϑ)    exact h_getLastBit  have h_i_add_2_pow_ϑ := Nat.sum_of_and_eq_zero_is_xor (n := i.val)    (m := 2 ^ ϑ) (h_n_AND_m:=h_i_and_2_pow_ϑ)  have h_getLastBit_add_pow_2 : Nat.getBit (Fin.last ϑ) (i + 2 ^ ϑ) = 1 := by    rw [h_i_add_2_pow_ϑ]; rw [Nat.getBit_of_xor]    rw [h_getLastBit]; rw [Nat.getBit_two_pow]    simp only [Fin.val_last, BEq.rfl, ↓reduceIte, Nat.zero_xor]  have h_tensor_split_0 :    multilinearWeight r ⟨i, by omega⟩ = multilinearWeight r_init i * (1 - r (Fin.last ϑ)) := by    dsimp only [multilinearWeight]    rw [Fin.prod_univ_castSucc]    simp_rw [Nat.testBit_true_eq_getBit_eq_1]    simp_rw [h_getLastBit]    simp only [Fin.val_castSucc]    congr 1  have h_tensor_split_1 :    multilinearWeight r ⟨i + 2 ^ ϑ, by omega⟩ = multilinearWeight r_init i * (r (Fin.last ϑ)) := by    dsimp only [multilinearWeight]    rw [Fin.prod_univ_castSucc]    simp_rw [Nat.testBit_true_eq_getBit_eq_1]    simp_rw [h_getLastBit_add_pow_2]    simp only [Fin.val_castSucc, ↓reduceIte]    congr 1    apply Finset.prod_congr rfl    intro x hx_univ-- index of the product    rw [h_i_add_2_pow_ϑ]    simp_rw [Nat.getBit_of_xor, Nat.getBit_two_pow]    simp only [beq_iff_eq]    have h_x_ne_ϑ: ϑ ≠ x.val := by omega    simp only [h_x_ne_ϑ, ↓reduceIte, Nat.xor_zero]    rfl  rw [h_tensor_split_0, h_tensor_split_1]