T sdh cond of two valid openings

lemma t_sdh_cond_of_two_valid_openings    (τ query resp₁ resp₂ : ZMod p) (cm proof₁ proof₂ : G₁)    (srs : Vector G₁ (n + 1) × Vector G₂ 2)    (hsrs : srs = Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)    (hresp : resp₁ ≠ resp₂) (hg₁ : g₁ ≠ 1) (hpair : pairing g₁ g₂ ≠ 0)    (hverify₁ : KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)      srs.2 cm proof₁ query resp₁)    (hverify₂ : KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)      srs.2 cm proof₂ query resp₂) :    Groups.tSdhCondition (p := p) (g₁ := g₁)      (τ, -query, (proof₁ / proof₂) ^ (1 / (resp₂ - resp₁)).val) := by  have hpG1 : Nat.card G₁ = p := PrimeOrderWith.hCard  have hord : orderOf g₁ = p := binding_order_of_eq_prime_of_ne_one g₁ hg₁  obtain ⟨cm', hcm⟩ := binding_exists_zmod_power_of_generator hpG1 hg₁ hord cm  obtain ⟨prf₁, hprf₁⟩ :=    binding_exists_zmod_power_of_generator hpG1 hg₁ hord proof₁  obtain ⟨prf₂, hprf₂⟩ :=    binding_exists_zmod_power_of_generator hpG1 hg₁ hord proof₂  have hEq₁ : cm' - resp₁ = prf₁ * (τ - query) :=    verify_opening_equation pairing query resp₁ τ cm' prf₁ cm proof₁ srs hsrs hpair hcm      hprf₁ hverify₁  have hEq₂ : cm' - resp₂ = prf₂ * (τ - query) :=    verify_opening_equation pairing query resp₂ τ cm' prf₂ cm proof₂ srs hsrs hpair hcm      hprf₂ hverify₂  have hdenom : τ + -query ≠ 0 :=    t_sdh_denominator_ne_zero_of_opening_equations τ query resp₁ resp₂ cm' prf₁ prf₂      hresp hEq₁ hEq₂  refine ⟨hdenom, ?_⟩  have hfield_conflict : prf₁ * (τ - query) + resp₁ = prf₂ * (τ - query) + resp₂ := by    linear_combination hEq₂ - hEq₁  have hfield_solution : (prf₁ - prf₂) / (resp₂ - resp₁) = 1 / (τ - query) := by    have hresp_ne : resp₂ - resp₁ ≠ 0 := sub_ne_zero.mpr (Ne.symm hresp)    have hτq_ne : τ - query ≠ 0 := by simpa [sub_eq_add_neg] using hdenom    rw [div_eq_div_iff hresp_ne hτq_ne]    linear_combination hfield_conflict  rw [hprf₁, hprf₂, Groups.gpow_div_eq hord, ← pow_mul, pow_eq_pow_iff_modEq, hord]  change (prf₁ - prf₂).val * (1 / (resp₂ - resp₁)).val % p =    (1 / (τ + -query)).val % p  rw [Nat.mod_eq_of_lt (ZMod.val_lt _)]  have hcast : (((prf₁ - prf₂).val * (1 / (resp₂ - resp₁)).val : ℕ) : ZMod p)      = (1 / (τ + -query) : ZMod p) := by    push_cast [ZMod.natCast_zmod_val]    rw [mul_one_div, hfield_solution]    ring  have := congr_arg ZMod.val hcast  rwa [ZMod.val_natCast] at this