Find s successful

lemma find_s_successful {L : ℕ} (n : ℕ) (τ : ZMod p) (c : G₁) (A : Finset (Fin L))    (query : Fin L → ZMod p) (response : Fin L → ZMod p)    (srs : Vector G₁ (n + 1) × Vector G₂ 2)    (hsrs : srs = Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)    (hgen : srs.1[0] ≠ 1)    (hA : (CLagrange.interpolate A query response).degree = n + 1)    (hquery : Set.InjOn query ↑A) (hn : 1 ≤ n) :    (findS n A c srs query response).isSome := by  by_contra h_not  have h_none : findS n A c srs query response = none := by    match hc : findS n A c srs query response with    | none => rfl    | some _ => simp [hc] at h_not  unfold findS at h_none  rw [List.find?_eq_none] at h_none  simp only [decide_eq_true_eq, not_not] at h_none  have hg₁ : g₁ ≠ 1 :=    Groups.PowerSrs.generator_ne_one_of_generate (g₁ := g₁) (g₂ := g₂) hsrs hgen  have hpG1 : Nat.card G₁ = p := PrimeOrderWith.hCard  have hord : orderOf g₁ = p := Groups.orderOf_eq_prime_of_ne_one g₁ hg₁  obtain ⟨c', hc_eq⟩ := Groups.exists_zmod_power_of_generator hpG1 hg₁ hord c  -- For every candidate S, commit = c means eval τ = c'  have h_all_eq : ∀ S ⊆ A, S.card = n + 1 →      (CLagrange.interpolate S query response).eval τ = c' := by    intro S hSA hScard    -- S is in the candidate list    have hS_mem := finset_subset_mem_sublists_len_map S A hSA hScard    -- The hypothesis says commit = c for S    have hcommit_eq := h_none S hS_mem    -- Degree bound for interpolation over S    have hdeg : (CLagrange.interpolate S query response).degree ≤ ↑n :=      interp_degree_le_of_card S query response (hquery.mono hSA) hScard    -- Rewrite commit using commit_eq_c_polynomial    have hcommit_rw : commit srs.1 ((CLagrange.interpolate S query response).val.coeff ∘ Fin.val)        = g₁ ^ ((CLagrange.interpolate S query response).eval τ).val := by      conv_lhs => rw [hsrs, Groups.PowerSrs.generate]      exact commit_eq_c_polynomial (g₁ := g₁) hpG1        (CLagrange.interpolate S query response) hdeg    -- So g₁ ^ (eval τ ...).val = g₁ ^ c'.val    rw [hcommit_rw, hc_eq] at hcommit_eq    -- Injectivity: g₁ ^ a = g₁ ^ b with a, b < orderOf g₁ implies a = b    have hinj : ((CLagrange.interpolate S query response).eval τ).val = c'.val :=      pow_injOn_Iio_orderOf        (show ((CLagrange.interpolate S query response).eval τ).val ∈ Set.Iio (orderOf g₁)          from by rw [hord]; exact ZMod.val_lt _)        (show c'.val ∈ Set.Iio (orderOf g₁)          from by rw [hord]; exact ZMod.val_lt _)        hcommit_eq    exact ZMod.val_injective p hinj  -- But find_s_existence gives an S with eval τ ≠ c'  obtain ⟨S₀, hS₀_sub, hS₀_card, hS₀_ne⟩ :=    find_s_existence n τ c' A query response hA hquery hn  exact hS₀_ne (h_all_eq S₀ hS₀_sub hS₀_card)