-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) :=
  (finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p
hp' : p' = (finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
simp :
  Finset.card (α := R × ((i : Fin n) → R))
      ({x ∈ piFinset (δ := fun (i : Fin n) ↦ R) (tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S) |
            ¬Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)}.biUnion
        fun (a : (i : Fin n) → R) ↦
        image (fun (a_1 : R) ↦ (a_1, a))
          ({a_1 ∈ S 0 |
            Eq (α := R)
              ((eval
                      (((consEquiv.{u_1} (n := n) fun (i : Fin (n + 1)) ↦ R :
                            R × ((i : Fin n) → R) ≃ ((i : Fin (n + 1)) → R)) :
                          (a : R × ((i : Fin n) → R)) → (i : Fin (n + 1)) → R)
                        (a_1, a)) :
                    (a : MvPolynomial (Fin (n + 1)) R) → R)
                  p :
                R)
              (0 : R)})) =
    Finset.card.{u_1} (α := R × (Fin n → R))
      (Finset.biUnion
        ({x ∈ piFinset (δ := fun (a : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i |
          ¬Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)})
        fun (xₜ : Fin n → R) ↦
        image (fun (x₀ : R) ↦ (x₀, xₜ))
          ({x₀ ∈ S 0 |
            Eq (α := R)
              ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ xₜ) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
              (0 : R)}))
⊢ Finset.card (α := R × ((i : Fin n) → R))
      ({r ∈ piFinset (δ := fun (i : Fin n) ↦ R) (tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S) |
            Ne (α := R) ((eval r : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)}.biUnion
        fun (a : (i : Fin n) → R) ↦
        filter
          ((fun (x : (i : Fin (n + 1)) → R) ↦
              Eq (α := R) ((eval x : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R)) ∘
            (⇑(Equiv.toEmbedding (consEquiv.{u_1} (n := n) fun (i : Fin (n + 1)) ↦ R) :
                  R × ((i : Fin n) → R) ↪ (i : Fin (n + 1)) → R) :
              (a : R × ((i : Fin n) → R)) → (i : Fin (n + 1)) → R))
          (image (fun (a_1 : R) ↦ (a_1, a)) (S 0))) =
    Finset.card.{u_1} (α := R × (Fin n → R))
      (Finset.biUnion
        ({xₜ ∈ piFinset (δ := fun (a : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i |
          Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)})
        fun (xₜ : Fin n → R) ↦
        image (fun (x₀ : R) ↦ (x₀, xₜ))
          ({x₀ ∈ S 0 |
            Eq (α := R)
              ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ xₜ) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
              (0 : R)}))

Tactic:
simp [filter_image]

Premises used: Finset.filter_image