-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
simp_rw :
  Eq (α := SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))
    (((↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField) :
          (a : MvPolynomial (Vars k) k) → (∏ f ∈ s, (↑f : k[X])).SplittingField)
        ((subProdXSubC f).coeff n) :
      SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))
    (0 : SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))
simp_rw₁ :
  coeff
      (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField) (subProdXSubC f))
      n =
    0
simp_rw₂ :
  coeff
      (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField)
        (HSub.hSub (α := (MvPolynomial (Vars k) k)[X]) (map (algebraMap k (MvPolynomial (Vars k) k)) (↑f : k[X]))
          (∏ i : Fin (↑f : k[X]).natDegree,
            HSub.hSub (α := (MvPolynomial (Vars k) k)[X]) (β := (MvPolynomial (Vars k) k)[X]) X
              ((C : (a : MvPolynomial (Vars k) k) → (MvPolynomial (Vars k) k)[X])
                  (MvPolynomial.X (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree) f i)) :
                (MvPolynomial (Vars k) k)[X]))))
      n =
    0
simp_rw₃ :
  (HSub.hSub (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X])
          (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField)
            (map (algebraMap k (MvPolynomial (Vars k) k)) (↑f : k[X])))
          (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField)
            (∏ i : Fin (↑f : k[X]).natDegree,
              HSub.hSub (α := (MvPolynomial (Vars k) k)[X]) (β := (MvPolynomial (Vars k) k)[X]) X
                ((C : (a : MvPolynomial (Vars k) k) → (MvPolynomial (Vars k) k)[X])
                    (MvPolynomial.X (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree) f i)) :
                  (MvPolynomial (Vars k) k)[X])))).coeff
      n =
    0
simp_rw₄ :
  (HSub.hSub (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X])
          (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField)
            (map (algebraMap k (MvPolynomial (Vars k) k)) (↑f : k[X])))
          (∏ i : Fin (↑f : k[X]).natDegree,
            map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField)
              (HSub.hSub (α := (MvPolynomial (Vars k) k)[X]) (β := (MvPolynomial (Vars k) k)[X]) X
                ((C : (a : MvPolynomial (Vars k) k) → (MvPolynomial (Vars k) k)[X])
                    (MvPolynomial.X (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree) f i)) :
                  (MvPolynomial (Vars k) k)[X])))).coeff
      n =
    0
simp_rw₅ :
  (HSub.hSub (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X])
          (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField)
            (map (algebraMap k (MvPolynomial (Vars k) k)) (↑f : k[X])))
          (∏ x : Fin (↑f : k[X]).natDegree,
            HSub.hSub (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X])
              (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField) X)
              (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField)
                ((C : (a : MvPolynomial (Vars k) k) → (MvPolynomial (Vars k) k)[X])
                  (MvPolynomial.X (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree) f x)))))).coeff
      n =
    0
simp_rw₆ :
  (HSub.hSub (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X])
          (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField)
            (map (algebraMap k (MvPolynomial (Vars k) k)) (↑f : k[X])))
          (∏ x : Fin (↑f : k[X]).natDegree,
            HSub.hSub (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]) X
              (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField)
                ((C : (a : MvPolynomial (Vars k) k) → (MvPolynomial (Vars k) k)[X])
                  (MvPolynomial.X (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree) f x)))))).coeff
      n =
    0
⊢ Eq (α := SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))
    ((toSplittingField s : (a : MvPolynomial (Vars k) k) → (∏ f ∈ s, (↑f : k[X])).SplittingField)
        ((subProdXSubC f).coeff n) :
      SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))
    (0 : SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))
have simp_rw₇ : (HSub.hSub (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X])
        (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField)
          (map (algebraMap k (MvPolynomial (Vars k) k)) (↑f : k[X])))
        (∏ x : Fin (↑f : k[X]).natDegree,
          HSub.hSub (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]) (β :=
            (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]) X
            ((C : (a : (∏ f ∈ s, (↑f : k[X])).SplittingField) → (∏ f ∈ s, (↑f : k[X])).SplittingField[X])
                (((↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField) :
                    (a : MvPolynomial (Vars k) k) → (∏ f ∈ s, (↑f : k[X])).SplittingField)
                  (MvPolynomial.X (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree) f x))) :
              (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]))).coeff
    n =
  0
Tactic: classical
  simp_rw [← AlgHom.coe_toRingHom, ← coeff_map, subProdXSubC, Polynomial.map_sub,
    Polynomial.map_prod, Polynomial.map_sub, map_X, map_C, toSplittingField,
    AlgHom.coe_toRingHom, MvPolynomial.aeval_X, dif_pos h,
    ← (finEquivRoots (Monics.splits_finsetProd h)).symm.prod_comp, Equiv.apply_symm_apply]
  rw [Finset.prod_coe_sort (f := fun x : _ × ℕ ↦ X - C x.1), (Multiset.toEnumFinset _)
    |>.prod_eq_multiset_prod, ← Function.comp_def (X - C ·) Prod.fst, ← Multiset.map_map,
    Multiset.map_toEnumFinset_fst, map_map, AlgHom.comp_algebraMap]
  conv in map _ _ => rw [Splits.eq_prod_roots (Monics.splits_finsetProd h)]
  rw [leadingCoeff_map, f.2, map_one, C_1, one_mul, sub_self, coeff_zero]