Commit eq

theorem commit_eq {a : ZMod p} (hpG1 : Nat.card G₁ = p)    (poly : Polynomial.degreeLT (ZMod p) (n + 1)) :    commit (Groups.PowerSrs.tower g₁ a n) (Polynomial.degreeLTEquiv _ _ poly)      = g₁ ^ (poly.1.eval a).val := by  have {g₁ : G₁} (a b : ℕ) : g₁ ^ a = g₁ ^ b ↔ g₁ ^ (a : ℤ) = g₁ ^ (b : ℤ) := by    simp only [zpow_natCast]  simp only [commit, Groups.PowerSrs.tower, Fin.getElem_fin, Vector.getElem_ofFn]  simp_rw [← pow_mul, Finset.prod_pow_eq_pow_sum,    Polynomial.eval_eq_sum_degreeLTEquiv poly.property,      this,      ←orderOf_dvd_sub_iff_zpow_eq_zpow]  have hordg₁ : g₁ = 1 ∨ orderOf g₁ = p := by    have ord_g₁_dvd : orderOf g₁ ∣ p := by rw [← hpG1]; apply orderOf_dvd_natCard    rw [Nat.dvd_prime hp.out, orderOf_eq_one_iff] at ord_g₁_dvd    exact ord_g₁_dvd  rcases hordg₁ with ord1 | ordp  · simp [ord1]  · simp only [ordp, Nat.cast_sum, Nat.cast_mul, Nat.cast_pow, ZMod.natCast_val, Subtype.coe_eta,    ← ZMod.intCast_eq_intCast_iff_dvd_sub, ZMod.intCast_cast, ZMod.cast_id', id_eq, Int.cast_sum,    Int.cast_mul, Int.cast_pow]    apply Fintype.sum_congr    intro x    exact mul_comm _ _