awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
inst_12 : Algebra.{u_4, u_2} R ↥F
inst_13 : Algebra R M
inst_14 : IsScalarTower.{u_4, u_2, u_3} R (↥F) M
inst_15 : IsIntegralClosure.{u_5, u_4, u_2} S R ↥F
x : S
rw :
  Eq.{u_3 + 1} (α := M) (↑((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x) : M)
    (↑(((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
          ((algebraMap S ↥F : (a : S) → ↥F) x)) :
      M)
rw₁ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((↑(((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
            ((algebraMap S ↥F : (a : S) → ↥F) x)) :
        M) :
      M)
⊢ Eq.{u_3 + 1} (α := ↥(F.extendRight M))
    ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M))
    (((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
        ((algebraMap S ↥F : (a : S) → ↥F) x) :
      ↥(F.extendRight M))
have rw₂ : Eq (α := M)
  ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
      ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
    M)
  ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
      (((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
          ((algebraMap S ↥F : (a : S) → ↥F) x) :
        ↥(F.extendRight M)) :
    M)
Tactic: rw [Subtype.ext_iff, ← algebraMap_apply (F.extendRight M), ← algebraMap_apply (F.extendRight M),
    algebraMap_extendRightEquiv', ← IsScalarTower.algebraMap_apply,
    ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
inst_12 : Algebra.{u_4, u_2} R ↥F
inst_13 : Algebra R M
inst_14 : IsScalarTower.{u_4, u_2, u_3} R (↥F) M
inst_15 : IsIntegralClosure.{u_5, u_4, u_2} S R ↥F
x : S
rw :
  Eq.{u_3 + 1} (α := M) (↑((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x) : M)
    (↑(((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
          ((algebraMap S ↥F : (a : S) → ↥F) x)) :
      M)
rw₁ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((↑(((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
            ((algebraMap S ↥F : (a : S) → ↥F) x)) :
        M) :
      M)
rw₂ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        (((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
            ((algebraMap S ↥F : (a : S) → ↥F) x) :
          ↥(F.extendRight M)) :
      M)
⊢ Eq.{u_3 + 1} (α := ↥(F.extendRight M))
    ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M))
    (((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
        ((algebraMap S ↥F : (a : S) → ↥F) x) :
      ↥(F.extendRight M))
have rw₃ : Eq (α := M)
  ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
      ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
    M)
  ((algebraMap (↥F) M : (a : ↥F) → M) ((algebraMap S ↥F : (a : S) → ↥F) x : ↥F) : M)
Tactic: rw [Subtype.ext_iff, ← algebraMap_apply (F.extendRight M), ← algebraMap_apply (F.extendRight M),
    algebraMap_extendRightEquiv', ← IsScalarTower.algebraMap_apply,
    ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
inst_12 : Algebra.{u_4, u_2} R ↥F
inst_13 : Algebra R M
inst_14 : IsScalarTower.{u_4, u_2, u_3} R (↥F) M
inst_15 : IsIntegralClosure.{u_5, u_4, u_2} S R ↥F
x : S
rw :
  Eq.{u_3 + 1} (α := M) (↑((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x) : M)
    (↑(((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
          ((algebraMap S ↥F : (a : S) → ↥F) x)) :
      M)
rw₁ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((↑(((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
            ((algebraMap S ↥F : (a : S) → ↥F) x)) :
        M) :
      M)
rw₂ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        (((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
            ((algebraMap S ↥F : (a : S) → ↥F) x) :
          ↥(F.extendRight M)) :
      M)
rw₃ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((algebraMap (↥F) M : (a : ↥F) → M) ((algebraMap S ↥F : (a : S) → ↥F) x : ↥F) : M)
⊢ Eq.{u_3 + 1} (α := ↥(F.extendRight M))
    ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M))
    (((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
        ((algebraMap S ↥F : (a : S) → ↥F) x) :
      ↥(F.extendRight M))
have rw₄ : Eq.{u_3 + 1} (α := M) ((algebraMap S M : (a : S) → M) x : M)
  ((algebraMap (↥F) M : (a : ↥F) → M) ((algebraMap S ↥F : (a : S) → ↥F) x : ↥F) : M)
Tactic: rw [Subtype.ext_iff, ← algebraMap_apply (F.extendRight M), ← algebraMap_apply (F.extendRight M),
    algebraMap_extendRightEquiv', ← IsScalarTower.algebraMap_apply,
    ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
inst_12 : Algebra.{u_4, u_2} R ↥F
inst_13 : Algebra R M
inst_14 : IsScalarTower.{u_4, u_2, u_3} R (↥F) M
inst_15 : IsIntegralClosure.{u_5, u_4, u_2} S R ↥F
x : S
rw :
  Eq.{u_3 + 1} (α := M) (↑((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x) : M)
    (↑(((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
          ((algebraMap S ↥F : (a : S) → ↥F) x)) :
      M)
rw₁ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((↑(((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
            ((algebraMap S ↥F : (a : S) → ↥F) x)) :
        M) :
      M)
rw₂ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        (((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
            ((algebraMap S ↥F : (a : S) → ↥F) x) :
          ↥(F.extendRight M)) :
      M)
rw₃ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((algebraMap (↥F) M : (a : ↥F) → M) ((algebraMap S ↥F : (a : S) → ↥F) x : ↥F) : M)
rw₄ :
  Eq.{u_3 + 1} (α := M) ((algebraMap S M : (a : S) → M) x : M)
    ((algebraMap (↥F) M : (a : ↥F) → M) ((algebraMap S ↥F : (a : S) → ↥F) x : ↥F) : M)
⊢ Eq.{u_3 + 1} (α := ↥(F.extendRight M))
    ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M))
    (((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
        ((algebraMap S ↥F : (a : S) → ↥F) x) :
      ↥(F.extendRight M))
have rw₅ : Eq.{u_3 + 1} (α := M) ((algebraMap S M : (a : S) → M) x : M) ((algebraMap S M : (a : S) → M) x : M)
Tactic: rw [Subtype.ext_iff, ← algebraMap_apply (F.extendRight M), ← algebraMap_apply (F.extendRight M),
    algebraMap_extendRightEquiv', ← IsScalarTower.algebraMap_apply,
    ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
K : Type u_1
inst_1 : Field K
inst_2 : DecidableEq K
i : k →+* K
f : Monics k
hf : (map i (↑f : k[X])).Splits
⊢ (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
have rwa : ∀ (hf : (map i (↑f : k[X])).roots.card = (map i (↑f : k[X])).natDegree),
  (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
Tactic: rwa [splits_iff_card_roots,
      ← Multiset.card_toEnumFinset, f.2.natDegree_map] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
K : Type u_1
inst_1 : Field K
inst_2 : DecidableEq K
i : k →+* K
f : Monics k
hf : (map i (↑f : k[X])).Splits
rwa :
  ∀ (hf : (map i (↑f : k[X])).roots.card = (map i (↑f : k[X])).natDegree),
    (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
⊢ (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
have rwa₁ : ∀ (hf : (map i (↑f : k[X])).roots.toEnumFinset.card = (map i (↑f : k[X])).natDegree),
  (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
Tactic: rwa [splits_iff_card_roots,
      ← Multiset.card_toEnumFinset, f.2.natDegree_map] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
K : Type u_1
inst_1 : Field K
inst_2 : DecidableEq K
i : k →+* K
f : Monics k
hf : (map i (↑f : k[X])).Splits
rwa :
  ∀ (hf : (map i (↑f : k[X])).roots.card = (map i (↑f : k[X])).natDegree),
    (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
rwa₁ :
  ∀ (hf : (map i (↑f : k[X])).roots.toEnumFinset.card = (map i (↑f : k[X])).natDegree),
    (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
⊢ (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
have rwa₂ : ∀ (hf : (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree),
  (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
Tactic: rwa [splits_iff_card_roots,
      ← Multiset.card_toEnumFinset, f.2.natDegree_map] at hf
Cleared hypotheses: hf
-- 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 : ℕ
⊢ 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 : ↥(map (algebraMap k (∏ f ∈ s, (↑f : k[X])).SplittingField) (↑f : k[X])).roots.toEnumFinset,
          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 : (∏ f ∈ s, (↑f : k[X])).SplittingField × ℕ).1 :
              (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]))).coeff
    n =
  0
Tactic: 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]
-- 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 : ℕ
⊢ (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 ⋯ :
                              (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 : ↥(map (algebraMap k (∏ f ∈ s, (↑f : k[X])).SplittingField) (↑f : k[X])).roots.toEnumFinset,
            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 : (∏ f ∈ s, (↑f : k[X])).SplittingField × ℕ).1 :
                (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X]))).coeff
      n =
    0
have rw : (HSub.hSub (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X])
        (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
Tactic: 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]
-- 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 : ℕ
| map (algebraMap k (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))) (↑f : k[X])
have 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])
    (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])))))
Tactic: rw [Splits.eq_prod_roots (Monics.splits_finsetProd h)]
-- 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 : ℕ
⊢ (HSub.hSub (α := (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))[X])
          (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 conv : (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
Tactic: conv in map _ _ => rw [Splits.eq_prod_roots (Monics.splits_finsetProd h)]
-- 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 : ℕ
⊢ 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 : 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])))
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]
-- 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])))
⊢ 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₁ : coeff (map (↑(toSplittingField s) : MvPolynomial (Vars k) k →+* (∏ f ∈ s, (↑f : k[X])).SplittingField) (subProdXSubC f))
    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]