-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
Let Let₁ Let₂ : ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
Let₃ :
  let N :=
    Fintype.card.{u_1}
      { x : ↥s → ZMod p //
        Eq (α := ZMod p)
            (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
              ZMod p)
            (0 : ZMod p) ∧
          Eq (α := ZMod p)
            (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
              ZMod p)
            (0 : ZMod p) };
  ∀ (hN₀ : 0 < N), ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
have Let₄ : let N :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) };
∀ (hN₀ : 0 < N) (hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s), ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
Tactic: classical
  -- Let `N` be the number of common roots of our polynomials `f₁` and `f₂` (`f s ff` and `f s tt`).
  set N := Fintype.card {x // eval x (f₁ s a) = 0 ∧ eval x (f₂ s a) = 0}
  -- Zero is a common root to `f₁` and `f₂`, so `N` is nonzero
  let zero_sol : {x // eval x (f₁ s a) = 0 ∧ eval x (f₂ s a) = 0} :=
    ⟨0, by simp [f₁, f₂, map_sum, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]⟩
  have hN₀ : 0 < N := @Fintype.card_pos _ _ ⟨zero_sol⟩
  have hs' : 2 * p - 1 = Fintype.card s := by simp [hs]
  -- Chevalley-Warning gives us that `p ∣ n` because the total degrees of `f₁` and `f₂` are at most
  -- `p - 1`, and we have `2 * p - 1 > 2 * (p - 1)` variables.
  have hpN : p ∣ N := char_dvd_card_solutions_of_add_lt p
    (totalDegree_f₁_add_totalDegree_f₂.trans_eq hs')
  -- Hence, `2 ≤ p ≤ N` and we can make a common root `x ≠ 0`.
  obtain ⟨x, hx⟩ := Fintype.exists_ne_of_one_lt_card ((Fact.out : p.Prime).one_lt.trans_le <|
    Nat.le_of_dvd hN₀ hpN) zero_sol
  -- This common root gives us the required subsequence, namely the `i ∈ s` such that `x i ≠ 0`.
  refine ⟨({a | x.1 a ≠ 0} : Finset _).map ⟨(↑), Subtype.val_injective⟩, ?_, ?_, ?_⟩
  · simp +contextual [subset_iff]
  -- From `f₁ x = 0`, we get that `p` divides the number of `a` such that `x a ≠ 0`.
  · rw [card_map]
    refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ <|
      (Finset.card_filter_le _ _).trans_lt ?_
    -- This number is nonzero because `x ≠ 0`.
    · rw [← Subtype.coe_ne_coe, Function.ne_iff] at hx
      exact hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩)
    · rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]
      simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1
    -- And it is at most `2 * p - 1`, so it must be `p`.
    · rw [univ_eq_attach, card_attach, hs]
      exact tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one
  -- From `f₂ x = 0`, we get that `p` divides the sum of the `a ∈ s` such that `x a ≠ 0`.
  · simpa [f₂, ZMod.pow_card_sub_one, Finset.sum_filter] using x.2.2