Commit eq c polynomial

theorem commit_eq_c_polynomial {a : ZMod p} (hpG1 : Nat.card G₁ = p)    (poly : CPolynomial (ZMod p)) (hn : poly.degree ≤ n) :    commit (Groups.PowerSrs.tower g₁ a n)      ((coeff poly) ∘ Fin.val)      = g₁ ^ (poly.eval a).val := by  have h_mem : poly.toPoly ∈ Polynomial.degreeLT (ZMod p) (n + 1) := by    rw [Polynomial.mem_degreeLT, ← degree_toPoly]    exact lt_of_le_of_lt hn (WithBot.coe_lt_coe.mpr (Nat.lt_succ_self n))  rw [show poly.eval a = poly.toPoly.eval a from eval_toPoly a poly]  rw [show ((coeff poly) ∘ Fin.val : Fin (n + 1) → ZMod p) =      Polynomial.degreeLTEquiv (ZMod p) (n + 1) ⟨poly.toPoly, h_mem⟩ from by    ext i; simp only [Function.comp_apply, Polynomial.degreeLTEquiv]; exact coeff_toPoly poly i]  exact commit_eq hpG1 ⟨poly.toPoly, h_mem⟩