Zmod eq of srs power eq

lemma zmod_eq_of_srs_power_eq {α τ : ZMod p}    (hn : 1 ≤ n) (srs : Vector G₁ (n + 1) × Vector G₂ 2)    (hsrs : srs = Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)    (hord : orderOf g₁ = p)    (hpow : srs.1[0] ^ α.val = srs.1[1]'(Nat.lt_add_of_pos_left hn)) :    α = τ := by  have h_srs0 : srs.1[0] = g₁ := by    rw [hsrs]    simp [Groups.PowerSrs.generate, Groups.PowerSrs.tower]  have h_srs1 : srs.1[1]'(Nat.lt_add_of_pos_left hn) = g₁ ^ τ.val := by    rw [hsrs]    simp [Groups.PowerSrs.generate, Groups.PowerSrs.tower]  have hpow' : g₁ ^ α.val = g₁ ^ τ.val := by    rw [h_srs0, h_srs1] at hpow    exact hpow  have hmod : α.val ≡ τ.val [MOD orderOf g₁] := pow_eq_pow_iff_modEq.mp hpow'  rw [hord] at hmod  have h_eq : α.val = τ.val := by    have hm : α.val % p = τ.val % p := hmod    rwa [Nat.mod_eq_of_lt (ZMod.val_lt α), Nat.mod_eq_of_lt (ZMod.val_lt τ)] at hm  exact ZMod.val_injective p h_eq