-- 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 : ℕ
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
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)
                  1) :
              (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
rw₂ :
  (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]) 1)
            (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
rw₃ :
  (HMul.hMul (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]) 1
            (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
rw₄ :
  (HSub.hSub (α := (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])))))
          (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
⊢ (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₅ : Eq.{u + 1} (α := SplittingField (K := k) (∏ f ∈ s, (↑f : k[X]))) (coeff 0 n) 0
Tactic: rw [leadingCoeff_map, f.2, map_one, C_1, one_mul, sub_self, coeff_zero]