-- 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 (α := 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
rw :
  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)
        (HMul.hMul (α := 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])))
rw₁ :
  HMul.hMul (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) (β :=
      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)
          ((v : (a : Monics k × ℕ) → MvPolynomial (Vars k) k) j) :
        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)
          ((subProdXSubC j.1).coeff j.2) :
        SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) =
    0
rw₂ :
  HMul.hMul (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) (β :=
      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)
          ((v : (a : Monics k × ℕ) → MvPolynomial (Vars k) k) j) :
        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]))) =
    0
⊢ 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])))
have rw₃ : Eq.{u + 1} (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) 0 0
Tactic: rw [smul_eq_mul, map_mul, toSplittingField_coeff (Finset.mem_image_of_mem _ hj), mul_zero]