-- 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 : ℕ
⊢ (HMul.hMul (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X])
            ((C : (a : (∏ f ∈ s, (↑f : k[X])).SplittingField) → (∏ f ∈ s, (↑f : k[X])).SplittingField[X])
              (leadingCoeff (map (algebraMap k (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))) (↑f : k[X]))))
            (Multiset.prod
              (Multiset.map
                (fun (x : SplittingField (K := k) (∏ f ∈ s, (↑f : k[X]))) ↦
                  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]) x :
                      (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]))
                (roots (map (algebraMap k (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))) (↑f : k[X]))))) -
          Multiset.prod
            (Multiset.map
              (fun (x : SplittingField (K := k) (∏ f ∈ s, (↑f : k[X]))) ↦
                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]) x :
                    (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]))
              (roots (map (algebraMap k (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))) (↑f : k[X]))))).coeff
      n =
    0
have rw : (HMul.hMul (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]) (β :=
          (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X])
          ((C : (a : (∏ f ∈ s, (↑f : k[X])).SplittingField) → (∏ f ∈ s, (↑f : k[X])).SplittingField[X])
              (((algebraMap k (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X]))) :
                    k →+* SplittingField (K := k) (∏ f ∈ s, (↑f : k[X]))) :
                  (a : k) → (∏ f ∈ s, (↑f : k[X])).SplittingField)
                (↑f : k[X]).leadingCoeff) :
            (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X])
          (Multiset.prod
              (Multiset.map
                (fun (x : SplittingField (K := k) (∏ f ∈ s, (↑f : k[X]))) ↦
                  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]) x :
                      (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]))
                (roots (map (algebraMap k (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))) (↑f : k[X])))) :
            (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]) -
        Multiset.prod
          (Multiset.map
            (fun (x : SplittingField (K := k) (∏ f ∈ s, (↑f : k[X]))) ↦
              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]) x :
                  (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]))
            (roots (map (algebraMap k (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))) (↑f : k[X]))))).coeff
    n =
  0
Tactic: rw [leadingCoeff_map, f.2, map_one, C_1, one_mul, sub_self, coeff_zero]