Filter map conflict length

lemma filter_map_conflict_length (hp : p ≥ n + 2) (hn : 1 ≤ n)    (αᵢ : ZMod p) (srs : Vector G₁ (n + 1) × Vector G₂ 2) (hgen : srs.1[0] ≠ 1) :    ((Array.range p).filterMap fun i =>      if h : i < p then        let x : ZMod p := (⟨i, h⟩ : Fin p)        if srs.1[0] ^ x.val ≠ srs.1[1]'(Nat.lt_add_of_pos_left hn) ∧ x ≠ αᵢ then some x        else none      else none).size ≥ n := by  set arr := (Array.range p).filterMap fun i =>    if h : i < p then      let x : ZMod p := (⟨i, h⟩ : Fin p)      if srs.1[0] ^ x.val ≠ srs.1[1]'(Nat.lt_add_of_pos_left hn) ∧ x ≠ αᵢ then some x      else none    else none  -- Convert Array.size to Finset.card via Nodup  have hnodup : arr.toList.Nodup := filter_map_conflict_nodup αᵢ srs hn  rw [show arr.size = arr.toList.toFinset.card from by    rw [List.toFinset_card_of_nodup hnodup, Array.length_toList]]  set S := arr.toList.toFinset  -- Finset.univ (ZMod p) has card p  have hUnivCard : (Finset.univ : Finset (ZMod p)).card = p := by    rw [Finset.card_univ, ZMod.card]  -- The complement (univ \ S) contains only x where srs.1[0]^x.val = srs.1[1] ∨ x = αᵢ,  -- i.e., at most 2 elements (≤ 1 discrete log solution + αᵢ).  have hCompl : (Finset.univ \ S).card ≤ 2 := by    -- orderOf srs.1[0] = p (since srs.1[0] ≠ 1 in a group of prime order)    have hord : orderOf srs.1[0] = p := by      have hdvd : orderOf srs.1[0] ∣ p := by        have := orderOf_dvd_natCard (G := G₁) srs.1[0]        rwa [PrimeOrderWith.hCard] at this      rcases (Nat.dvd_prime Fact.out).1 hdvd with h1 | hp'      · exact absurd (orderOf_eq_one_iff.1 h1) hgen      · exact hp'    -- Injectivity of x ↦ g^x.val for x : ZMod p    have hinj : ∀ a b : ZMod p,        srs.1[0] ^ a.val = srs.1[0] ^ b.val → a = b := by      intro a b heq      rw [pow_eq_pow_iff_modEq, hord] at heq      have hval : a.val = b.val := by        rwa [Nat.ModEq, Nat.mod_eq_of_lt (ZMod.val_lt a),          Nat.mod_eq_of_lt (ZMod.val_lt b)] at heq      calc a = ↑a.val := (ZMod.natCast_zmod_val a).symm        _ = ↑b.val := congrArg Nat.cast hval        _ = b := ZMod.natCast_zmod_val b    -- Any x satisfying the condition is in S    have hmem : ∀ x : ZMod p,        srs.1[0] ^ x.val ≠ srs.1[1]'(Nat.lt_add_of_pos_left hn) → x ≠ αᵢ → x ∈ S := by      intro x hpow hneα      change x ∈ arr.toList.toFinset      simp only [List.mem_toFinset, arr, Array.toList_filterMap, Array.toList_range,        List.mem_filterMap, List.mem_range]      exact ⟨x.val, ZMod.val_lt x, by        simp only [ZMod.val_lt x, dite_true, ZMod.natCast_zmod_val]        exact if_pos ⟨hpow, hneα⟩⟩    -- The complement ⊆ {x | g^x.val = h} ∪ {αᵢ}    have hsub : Finset.univ \ S ⊆        Finset.univ.filter (fun x : ZMod p =>          srs.1[0] ^ x.val = srs.1[1]'(Nat.lt_add_of_pos_left hn)) ∪ {αᵢ} := by      intro x hx      simp only [Finset.mem_sdiff, Finset.mem_univ, true_and] at hx      simp only [Finset.mem_union, Finset.mem_filter, Finset.mem_univ, true_and,        Finset.mem_singleton]      by_contra h; push Not at h      exact hx (hmem x h.1 h.2)    -- The filter set has ≤ 1 element (injectivity of g^·)    have hfilt : (Finset.univ.filter (fun x : ZMod p =>        srs.1[0] ^ x.val = srs.1[1]'(Nat.lt_add_of_pos_left hn))).card ≤ 1 := by      rw [Finset.card_le_one]      intro a ha b hb      simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha hb      exact hinj a b (ha ▸ hb ▸ rfl)    calc (Finset.univ \ S).card        ≤ (Finset.univ.filter (fun x : ZMod p =>            srs.1[0] ^ x.val = srs.1[1]'(Nat.lt_add_of_pos_left hn)) ∪ {αᵢ}).card :=          Finset.card_le_card hsub      _ ≤ (Finset.univ.filter (fun x : ZMod p =>            srs.1[0] ^ x.val = srs.1[1]'(Nat.lt_add_of_pos_left hn))).card +          ({αᵢ} : Finset _).card := Finset.card_union_le _ _      _ ≤ 2 := by simp only [Finset.card_singleton]; omega  -- sdiff identity: (univ \ S).card + S.card = p  have hSdiff := Finset.card_sdiff_add_card_eq_card (Finset.subset_univ S)  omega