H1 zs eq h2 prime

lemma h1_zs_eq_h2_prime {L : ℕ} (n : ℕ) (τ : ZMod p) (cm : G₁) (S : Finset (Fin L))    (query : Fin L → ZMod p) (response : Fin L → ZMod p) (proofs : Fin L → G₁)    (srs : Vector G₁ (n + 1) × Vector G₂ 2) (hn : 1 ≤ n)    (hsrs : srs = Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)    (hτ : ∀ i ∈ S, (query i) ≠ τ)    (hVerify : ∀ i ∈ S, verifyOpening (pairing := pairing) (g₁ := g₁) (g₂ := g₂)      srs.2 cm (proofs i) (query i) (response i))    (hgen : srs.1[0] ≠ 1) (hpair : pairing g₁ g₂ ≠ 0)    (hS : (CLagrange.interpolate S query response).degree ≤ n) (hS_ne : S.Nonempty)    (hquery : Set.InjOn query ↑S) :    let Zₛ := ∏ s ∈ S.image query, (X - C s)    let c' : G₁ := commit srs.1 ((CLagrange.interpolate S query response).val.coeff ∘ Fin.val)    let h₁ := cm / c'    let d := fun α => 1 / eval α (divByMonic Zₛ (X - C α))      -- 1/(Z_{S \ {α}}(α))    let h₂ : G₁ := ∏ i ∈ S, (proofs i) ^ (d (query i)).val    h₂ = h₁ ^ (1 / Zₛ.eval τ).val := by    letI := Classical.decEq G₁    intro Zₛ c' h₁ d h₂    unfold h₁ h₂    -- rewrite the equation to g₁^{*equation*} (expose the field values)    have hpG1 : Nat.card G₁ = p := PrimeOrderWith.hCard    have hcommit_rw : c' = g₁ ^ ((CLagrange.interpolate S query response).eval τ).val := by      unfold c'      conv_lhs => rw [hsrs, Groups.PowerSrs.generate]      exact commit_eq_c_polynomial (g₁ := g₁) hpG1        (CLagrange.interpolate S query response) hS    rw [hcommit_rw]    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', hcm⟩ := Groups.exists_zmod_power_of_generator hpG1 hg₁ hord cm    have hproofs_pow : ∀ i, ∃ prf : ZMod p, proofs i = g₁ ^ prf.val := by      intro i      exact Groups.exists_zmod_power_of_generator hpG1 hg₁ hord (proofs i)    choose prf hprf using hproofs_pow    rw [hcm]    simp_rw [hprf]    have hprf_eq : ∀ i ∈ S, prf i = (cm' - response i) / (τ - query i) := by      intro i hi      exact verify_opening_prf_equation pairing (query i) (response i) τ cm' (prf i)        cm (proofs i) srs hsrs hpair (hVerify i hi) hcm (hprf i) (Ne.symm (hτ i hi))    rw [show ∏ x ∈ S, (g₁ ^ (prf x).val) ^ (d (query x)).val        = ∏ x ∈ S, (g₁ ^ ((cm' - response x) / (τ - query x)).val) ^ (d (query x)).val from      Finset.prod_congr rfl (fun i hi => by rw [hprf_eq i hi])]    -- move prod up to sum    unfold d    simp_rw [← pow_mul]    rw [Finset.prod_pow_eq_pow_sum]    have hlhs_rw : g₁ ^ (∑ x ∈ S,        ((cm' - response x) / (τ - query x)).val *        (1 / eval (query x) (Zₛ.divByMonic (X - C (query x)))).val)      = g₁ ^ (∑ x ∈ S,        (cm' - response x) /        (eval (query x) (Zₛ.divByMonic (X - C (query x))) * (τ - query x))).val := by      conv_lhs => rw [← pow_mod_orderOf g₁, hord]      congr 1      have hcast : ((∑ x ∈ S,          ((cm' - response x) / (τ - query x)).val *          (1 / eval (query x) (Zₛ.divByMonic (X - C (query x)))).val : ℕ) : ZMod p)        = (∑ x ∈ S,          (cm' - response x) /          (eval (query x) (Zₛ.divByMonic (X - C (query x))) * (τ - query x))) := by        push_cast [ZMod.natCast_zmod_val]        congr 1; ext x        rw [div_mul_div_comm, _root_.mul_one, mul_comm (τ - query x)]      have := congr_arg ZMod.val hcast      rw [ZMod.val_natCast] at this      exact this    rw [hlhs_rw]    -- split sum: (cm' - response x) / ... = cm' / ... - response x / ...    have hsplit : (∑ x ∈ S,        (cm' - response x) /        (eval (query x) (Zₛ.divByMonic (X - C (query x))) * (τ - query x)))      = (∑ x ∈ S,        cm' / (eval (query x) (Zₛ.divByMonic (X - C (query x))) * (τ - query x)))      - (∑ x ∈ S,        response x / (eval (query x) (Zₛ.divByMonic (X - C (query x))) * (τ - query x))) := by      simp only [sub_div, Finset.sum_sub_distrib]    rw [hsplit]    -- Rewrite the response sum using lagrange_zs_conversion    rw [← lagrange_zs_conversion τ S query response hτ hquery]    -- Factor cm' from the first sum and simplify to cm' / Zₛ.eval τ    have hcm_sum : (∑ x ∈ S,        cm' / (eval (query x) (Zₛ.divByMonic (X - C (query x))) * (τ - query x)))      = cm' / Zₛ.eval τ := by      have h1 : ∀ x ∈ S,          cm' / (eval (query x) (Zₛ.divByMonic (X - C (query x))) * (τ - query x))        = cm' * (1 / (eval (query x) (Zₛ.divByMonic (X - C (query x))) * (τ - query x))) :=        fun _ _ => by ring      rw [Finset.sum_congr rfl h1, ← Finset.mul_sum,        ← lagrange_zs_conversion τ S query (fun _ => 1) hτ hquery,        CLagrange.interpolation_of_constants S query (fun _ => 1) 1 (fun _ _ => rfl)          hquery hS_ne]      simp only [eval_toPoly, C_toPoly, Polynomial.eval_C]      ring    rw [hcm_sum]    -- Abbreviate    set r := (CLagrange.interpolate S query response).eval τ    set z := Zₛ.eval τ    -- LHS: cm'/z - r/z = (cm' - r) * (1/z)    conv_lhs => rw [show cm' / z - r / z = (cm' - r) * (1 / z) from by ring]    -- RHS: use div_pow (CommGroup) and pow_mul    rw [div_pow, ← pow_mul, ← pow_mul]    -- Expand powers over the difference of the scaled exponents.    rw [Groups.gpow_val_mul_eq hord cm' (1 / z),      Groups.gpow_val_mul_eq hord r (1 / z), Groups.gpow_div_eq hord]    congr 1    exact congr_arg ZMod.val (by ring : (cm' - r) * (1 / z) = cm' * (1 / z) - r * (1 / z))