-- 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
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
⊢ 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
          (↑(MvPolynomial.aeval fun (fi : Vars k) ↦
                if hf : fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree) ∈ s then
                  (↑((finEquivRoots sorry :
                            (a : Fin (↑fi.fst : k[X]).natDegree) →
                              ↥(map (algebraMap k (∏ f ∈ s, (↑f : k[X])).SplittingField)
                                      (↑fi.fst : k[X])).roots.toEnumFinset)
                          (fi.snd (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree))) :
                      (∏ f ∈ s, (↑f : k[X])).SplittingField × ℕ).1
                else 37) :
            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])
                (((↑(MvPolynomial.aeval fun (fi : Vars k) ↦
                          if hf : fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree) ∈ s then
                            (↑((finEquivRoots sorry :
                                      (a : Fin (↑fi.fst : k[X]).natDegree) →
                                        ↥(map (algebraMap k (∏ f ∈ s, (↑f : k[X])).SplittingField)
                                                (↑fi.fst : k[X])).roots.toEnumFinset)
                                    (fi.snd (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree))) :
                                (∏ f ∈ s, (↑f : k[X])).SplittingField × ℕ).1
                          else 37) :
                      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]