Gadget Decompose lawful

theorem gadgetDecompose_lawful {rows digits : Nat} (hd : 0 < digits) (h1 : 1 ≤ Φ.φ.natDegree)    (dd : DigitDecomposition base digits) :    IsLawfulGadgetDecomposition Φ base (gadgetDecompose Φ dd (rows := rows)) := by  intro x  funext i  rw [gadgetMul_apply Φ base hd]  simp_rw [gadgetDecompose_apply Φ dd x i]  apply Subtype.ext  rw [CompPoly.CPolynomial.eq_iff_coeff]  intro k  have hsum : (∑ e : Fin digits,        Rq.constRq Φ (base ^ (e : ℕ)) * Rq.ofFinCoeff Φ Φ.φ.natDegree          (fun k' => dd.digit ((x i).1.coeff k') e)).1.coeff k      = ∑ e : Fin digits,        (Rq.constRq Φ (base ^ (e : ℕ)) * Rq.ofFinCoeff Φ Φ.φ.natDegree          (fun k' => dd.digit ((x i).1.coeff k') e)).1.coeff k := by    rw [← Rq.coeffHom_apply Φ k, map_sum]    simp only [Rq.coeffHom_apply]  have hterm : ∀ e : Fin digits,      (Rq.constRq Φ (base ^ (e : ℕ)) * Rq.ofFinCoeff Φ Φ.φ.natDegree          (fun k' => dd.digit ((x i).1.coeff k') e)).1.coeff k        = base ^ (e : ℕ) * (if k < Φ.φ.natDegree then dd.digit ((x i).1.coeff k) e else 0) := by    intro e    rw [Rq.constRq_mul_coeff Φ h1, Rq.ofFinCoeff_coeff Φ _ (Rq.phi_natDegree_le_degree Φ)]  rw [hsum]  simp_rw [hterm]  by_cases hk : k < Φ.φ.natDegree  · simp only [if_pos hk]    exact dd.reconstruct ((x i).1.coeff k)  · simp only [if_neg hk, mul_zero, Finset.sum_const_zero]    exact (Rq.coeff_eq_zero_of_natDegree_le Φ (x i) (not_lt.mp hk)).symm