Conflict query ne tau

lemma conflict_query_ne_tau (hpG1 : Nat.card G₁ = p) (hn : 1 ≤ n)    (α₁ α₂ β₁ β₂ τ : ZMod p) (c pf₁ pf₂ : G₁) (hα : α₁ = α₂)    (hβ : β₁ ≠ β₂) (srs : Vector G₁ (n + 1) × Vector G₂ 2)    (hsrs : srs = Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)    (hgen : srs.1[0] ≠ 1) (hpair : pairing g₁ g₂ ≠ 0)    (hverify₁ : KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)      srs.2 c pf₁ α₁ β₁)    (hverify₂ : KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)      srs.2 c pf₂ α₂ β₂) :    α₁ ≠ τ := by  intro hατ  have hg₁ : g₁ ≠ 1 :=    Groups.PowerSrs.generator_ne_one_of_generate (g₁ := g₁) (g₂ := g₂) hsrs hgen  have hord : orderOf g₁ = p := Groups.orderOf_eq_prime_of_ne_one g₁ hg₁  obtain ⟨cm, hc⟩ := Groups.exists_zmod_power_of_generator hpG1 hg₁ hord c  obtain ⟨prf₁, hprf₁⟩ := Groups.exists_zmod_power_of_generator hpG1 hg₁ hord pf₁  obtain ⟨prf₂, hprf₂⟩ := Groups.exists_zmod_power_of_generator hpG1 hg₁ hord pf₂  have hfield_verify₁ : cm = prf₁ * (τ - α₁) + β₁ := by    grind [verify_opening_equation pairing α₁ β₁ τ cm prf₁ c pf₁ srs hsrs hpair      hc hprf₁ hverify₁]  have hfield_verify₂ : cm = prf₂ * (τ - α₁) + β₂ := by    rw [← hα] at hverify₂    grind [verify_opening_equation pairing α₁ β₂ τ cm prf₂ c pf₂ srs hsrs hpair      hc hprf₂ hverify₂]  have hfield_conflict : prf₁ * (τ - α₁) + β₁ = prf₂ * (τ - α₁) + β₂ := by    simp_all  apply hβ  have hzero : τ - α₁ = 0 := by simp [hατ]  simpa [hzero] using hfield_conflict