-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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
⊢ False
have 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),
  ∀ x ∈ 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) x : MvPolynomial (Vars k) k)
            ((subProdXSubC x.1).coeff x.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])))
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]
Cleared hypotheses: hv