-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left :
  Membership.mem (γ := Submodule (MvPolynomial (Vars k) k) (Monics k × ℕ →₀ MvPolynomial (Vars k) k))
    (Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ) v
hv :
  Eq (α := MvPolynomial (Vars k) k)
    ((Finsupp.linearCombination (MvPolynomial (Vars k) k) fun (fn : Monics k × ℕ) ↦ (subProdXSubC fn.1).coeff fn.2 :
          (a : Monics k × ℕ →₀ MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k)
        v :
      MvPolynomial (Vars k) k)
    (1 : MvPolynomial (Vars k) k)
replace replace₁ replace₂ :
  ∀
    (hv :
      Eq (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
        ((toSplittingField (Finset.image Prod.fst v.support) :
              (a : MvPolynomial (Vars k) k) → (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])).SplittingField)
            ((Finsupp.linearCombination (MvPolynomial (Vars k) k) fun (fn : Monics k × ℕ) ↦
                  (subProdXSubC fn.1).coeff fn.2 :
                (a : Monics k × ℕ →₀ MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k)
              v) :
          SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
        ((toSplittingField (Finset.image Prod.fst v.support) :
              (a : MvPolynomial (Vars k) k) → (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])).SplittingField)
            1 :
          SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))),
    False
replace₃ :
  ∀ (hv : Eq.{u + 1} (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) 0 1), False
replace₄ replace₅ replace₆ :
  ∀
    (hv :
      Eq (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
        (∑ x ∈ v.support,
          (toSplittingField (Finset.image Prod.fst v.support) :
              (a : MvPolynomial (Vars k) k) → (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])).SplittingField)
            (HSMul.hSMul (α := MvPolynomial (Vars k) k)
              ((v : (a : Monics k × ℕ) → MvPolynomial (Vars k) k) x : MvPolynomial (Vars k) k)
              ((subProdXSubC x.1).coeff x.2)))
        1)
    (j : Monics k × ℕ) (hj : j ∈ v.support),
    Eq (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
      ((toSplittingField (Finset.image Prod.fst v.support) :
            (a : MvPolynomial (Vars k) k) → (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])).SplittingField)
          (HSMul.hSMul (α := MvPolynomial (Vars k) k)
            ((v : (a : Monics k × ℕ) → MvPolynomial (Vars k) k) j : MvPolynomial (Vars k) k)
            ((subProdXSubC j.1).coeff j.2)) :
        SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
      (0 : SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
⊢ False

Tactic:
classical
  replace hv := congr_arg (toSplittingField <| v.support.image Prod.fst) hv
  rw [map_one, Finsupp.linearCombination_apply, Finsupp.sum, map_sum, Finset.sum_eq_zero] at hv
  · exact zero_ne_one hv
  intro j hj
  rw [smul_eq_mul, map_mul, toSplittingField_coeff (Finset.mem_image_of_mem _ hj), mul_zero]

Premises used: Finset.sum_eq_zero, Finsupp.sum, zero_ne_one, Finsupp.linearCombination_apply, map_sum, MulZeroClass.mul_zero, map_mul, map_one, smul_eq_mul