awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
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 ⋯ :
                              (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
⊢ 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])))

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]

Premises used: AlgHom.coe_toRingHom, Equiv.apply_symm_apply, Polynomial.coeff_map, AlgebraicClosure.finEquivRoots, MvPolynomial.aeval_X, dif_pos, Polynomial.map_X, AlgebraicClosure.Monics.splits_finsetProd, Polynomial.map_prod, Equiv.prod_comp, Polynomial.map_sub, AlgebraicClosure.toSplittingField, Polynomial.map_C, Equiv.symm, AlgebraicClosure.subProdXSubC
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
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
⊢ (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

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]

Premises used: Polynomial.C, AlgHom.comp_algebraMap, HSub.hSub, Finset.prod_coe_sort, Multiset.toEnumFinset, Prod.fst, Multiset.map_toEnumFinset_fst, Function.comp_def, Finset.prod_eq_multiset_prod, Multiset.map_map, Polynomial.map_map, Polynomial.X, DFunLike.coe
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
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])
    ((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])))))
| map (algebraMap k (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))) (↑f : k[X])

Tactic:
rw [Splits.eq_prod_roots (Monics.splits_finsetProd h)]

Premises used: Polynomial.Splits.eq_prod_roots, AlgebraicClosure.Monics.splits_finsetProd
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
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
⊢ (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:
conv in map _ _ => rw [Splits.eq_prod_roots (Monics.splits_finsetProd h)]

Premises used: Polynomial.Splits.eq_prod_roots, AlgebraicClosure.Monics.splits_finsetProd, Polynomial.map
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
rw :
  ¬∃ (l : Monics k × ℕ →₀ MvPolynomial (Vars k) k),
      Membership.mem (γ := Submodule (MvPolynomial (Vars k) k) (Monics k × ℕ →₀ MvPolynomial (Vars k) k))
          (Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ) l ∧
        Eq (α := MvPolynomial (Vars k) k)
          ((Finsupp.linearCombination (MvPolynomial (Vars k) k) fun (fn : Monics k × ℕ) ↦
                  (subProdXSubC fn.1).coeff fn.2 :
                (a : Monics k × ℕ →₀ MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k)
              l :
            MvPolynomial (Vars k) k)
          (1 : MvPolynomial (Vars k) k)
⊢ Ne (α := Ideal (MvPolynomial (Vars k) k)) (spanCoeffs k) ⊤

Tactic:
rw [Ideal.ne_top_iff_one, spanCoeffs, Ideal.span, ← Set.image_univ,
    Finsupp.mem_span_image_iff_linearCombination]

Premises used: Set.image_univ, Ideal.ne_top_iff_one, AlgebraicClosure.spanCoeffs, Ideal.span, Finsupp.mem_span_image_iff_linearCombination
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left :
  Membership.mem (γ := Submodule (MvPolynomial (Vars k) k) (Monics k × ℕ →₀ MvPolynomial (Vars k) k))
    (Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ) v
hv :
  Eq (α := MvPolynomial (Vars k) k)
    ((Finsupp.linearCombination (MvPolynomial (Vars k) k) fun (fn : Monics k × ℕ) ↦ (subProdXSubC fn.1).coeff fn.2 :
          (a : Monics k × ℕ →₀ MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k)
        v :
      MvPolynomial (Vars k) k)
    (1 : MvPolynomial (Vars k) k)
⊢ Eq (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
    ((toSplittingField (Finset.image Prod.fst v.support) :
          (a : MvPolynomial (Vars k) k) → (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])).SplittingField)
        ((Finsupp.linearCombination (MvPolynomial (Vars k) k) fun (fn : Monics k × ℕ) ↦ (subProdXSubC fn.1).coeff fn.2 :
            (a : Monics k × ℕ →₀ MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k)
          v) :
      SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
    ((toSplittingField (Finset.image Prod.fst v.support) :
          (a : MvPolynomial (Vars k) k) → (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])).SplittingField)
        1 :
      SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))

Tactic:
replace hv := congr_arg (toSplittingField <| v.support.image Prod.fst) hv
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left :
  Membership.mem (γ := Submodule (MvPolynomial (Vars k) k) (Monics k × ℕ →₀ MvPolynomial (Vars k) k))
    (Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ) v
hv :
  Eq (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
    ((toSplittingField (Finset.image Prod.fst v.support) :
          (a : MvPolynomial (Vars k) k) → (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])).SplittingField)
        ((Finsupp.linearCombination (MvPolynomial (Vars k) k) fun (fn : Monics k × ℕ) ↦ (subProdXSubC fn.1).coeff fn.2 :
            (a : Monics k × ℕ →₀ MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k)
          v) :
      SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
    ((toSplittingField (Finset.image Prod.fst v.support) :
          (a : MvPolynomial (Vars k) k) → (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])).SplittingField)
        1 :
      SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
rw : ∀ (hv : Eq.{u + 1} (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) 0 1), False
rw₁ :
  ∀
    (hv :
      Eq (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
        (∑ x ∈ v.support,
          (toSplittingField (Finset.image Prod.fst v.support) :
              (a : MvPolynomial (Vars k) k) → (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])).SplittingField)
            (HSMul.hSMul (α := MvPolynomial (Vars k) k)
              ((v : (a : Monics k × ℕ) → MvPolynomial (Vars k) k) x : MvPolynomial (Vars k) k)
              ((subProdXSubC x.1).coeff x.2)))
        1),
    ∀ x ∈ v.support,
      Eq (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
        ((toSplittingField (Finset.image Prod.fst v.support) :
              (a : MvPolynomial (Vars k) k) → (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])).SplittingField)
            (HSMul.hSMul (α := MvPolynomial (Vars k) k)
              ((v : (a : Monics k × ℕ) → MvPolynomial (Vars k) k) x : MvPolynomial (Vars k) k)
              ((subProdXSubC x.1).coeff x.2)) :
          SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
        (0 : SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X])))
⊢ False

Tactic:
rw [map_one, Finsupp.linearCombination_apply, Finsupp.sum, map_sum, Finset.sum_eq_zero] at hv

Premises used: Finset.sum_eq_zero, Finsupp.sum, Finsupp.linearCombination_apply, map_sum, map_one
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left :
  Membership.mem (γ := Submodule (MvPolynomial (Vars k) k) (Monics k × ℕ →₀ MvPolynomial (Vars k) k))
    (Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ) v
hv : Eq.{u + 1} (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) 0 1
⊢ False

Tactic:
zero_ne_one hv

Premises used: zero_ne_one
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left :
  Membership.mem (γ := Submodule (MvPolynomial (Vars k) k) (Monics k × ℕ →₀ MvPolynomial (Vars k) k))
    (Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ) v
hv : Eq.{u + 1} (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) 0 1
⊢ False

Tactic:
exact zero_ne_one hv

Premises used: zero_ne_one
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
⊢ Ideal.IsMaximal (α := MvPolynomial (Vars k) k) (maxIdeal k)

Tactic:
(Classical.choose_spec <| Ideal.exists_le_maximal _ <| spanCoeffs_ne_top k).1

Premises used: Classical.choose_spec, And.left, AlgebraicClosure.spanCoeffs_ne_top, AlgebraicClosure.maxIdeal, Ideal.exists_le_maximal
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
⊢ LE.le (α := Ideal (MvPolynomial (Vars k) k)) (spanCoeffs k) (maxIdeal k)

Tactic:
(Classical.choose_spec <| Ideal.exists_le_maximal _ <| spanCoeffs_ne_top k).2

Premises used: Set.Mem, Classical.choose_spec, And.right, AlgebraicClosure.spanCoeffs_ne_top, Ideal.exists_le_maximal
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
R : Type u_1
S : Type u_2
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Algebra S k
inst_5 : Algebra R k
inst_6 : IsScalarTower R S k
⊢ IsScalarTower.{u_1, u_2, u} R S (AlgebraicClosure k)

Tactic:
inferInstanceAs <| IsScalarTower R S (_ ⧸ _)

Premises used: _private.0.AlgebraicClosure.instIsScalarTower._proof_1
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
q : ℚ≥0
simp_rw :
  (algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (HDiv.hDiv (α := k) (↑q.num : k) (↑q.den : k)) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
simp_rw₁ :
  HDiv.hDiv (α := AlgebraicClosure k) ((algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q.num : k))
      ((algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q.den : k)) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
⊢ (algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q : k) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)

Tactic:
simp_rw [NNRat.cast_def, map_div₀, map_natCast]

Premises used: NNRat.cast_def, map_div₀, map_natCast
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
q : ℚ≥0
x : AlgebraicClosure k
p : MvPolynomial (Vars k) k
a :
  ∀ (m : Vars k →₀ ℕ),
    Eq (α := k) (MvPolynomial.coeff m ((fun (x : MvPolynomial (Vars k) k) ↦ q • x) p))
      (MvPolynomial.coeff m
        ((fun (x1 x2 : MvPolynomial (Vars k) k) ↦ x1 * x2)
          ((algebraMap k (MvPolynomial (Vars k) k) : (a : k) → MvPolynomial (Vars k) k) (↑q : k)) p))
⊢ Eq.{u + 1} (α := MvPolynomial (Vars k) k) ((fun (x : MvPolynomial (Vars k) k) ↦ q • x) p)
    ((fun (x1 x2 : MvPolynomial (Vars k) k) ↦ x1 * x2)
      ((algebraMap k (MvPolynomial (Vars k) k) : (a : k) → MvPolynomial (Vars k) k) (↑q : k)) p)

Tactic:
ext
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
q : ℚ≥0
x : AlgebraicClosure k
p : MvPolynomial (Vars k) k
m : Vars k →₀ ℕ
⊢ Eq (α := k) (MvPolynomial.coeff m ((fun (x : MvPolynomial (Vars k) k) ↦ q • x) p))
    (MvPolynomial.coeff m
      ((fun (x1 x2 : MvPolynomial (Vars k) k) ↦ x1 * x2)
        ((algebraMap k (MvPolynomial (Vars k) k) : (a : k) → MvPolynomial (Vars k) k) (↑q : k)) p))

Tactic:
simp [MvPolynomial.algebraMap_eq, NNRat.smul_def]

Premises used: MvPolynomial.algebraMap_eq, NNRat.smul_def
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
q : ℚ
rw :
  (algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (HDiv.hDiv (α := k) (↑q.num : k) (↑q.den : k)) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
rw₁ :
  HDiv.hDiv (α := AlgebraicClosure k) ((algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q.num : k))
      ((algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q.den : k)) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
rw₂ :
  HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k)
      ((algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q.den : k)) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
rw₃ rw₄ :
  HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
⊢ (algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q : k) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)

Tactic:
rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]

Premises used: map_intCast, Rat.cast_def, map_div₀, map_natCast
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
q : ℚ
x : AlgebraicClosure k
p : MvPolynomial (Vars k) k
a :
  ∀ (m : Vars k →₀ ℕ),
    Eq (α := k) (MvPolynomial.coeff m ((fun (x : MvPolynomial (Vars k) k) ↦ q • x) p))
      (MvPolynomial.coeff m
        ((fun (x1 x2 : MvPolynomial (Vars k) k) ↦ x1 * x2)
          ((algebraMap k (MvPolynomial (Vars k) k) : (a : k) → MvPolynomial (Vars k) k) (↑q : k)) p))
⊢ Eq.{u + 1} (α := MvPolynomial (Vars k) k) ((fun (x : MvPolynomial (Vars k) k) ↦ q • x) p)
    ((fun (x1 x2 : MvPolynomial (Vars k) k) ↦ x1 * x2)
      ((algebraMap k (MvPolynomial (Vars k) k) : (a : k) → MvPolynomial (Vars k) k) (↑q : k)) p)

Tactic:
ext
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
q : ℚ
x : AlgebraicClosure k
p : MvPolynomial (Vars k) k
m : Vars k →₀ ℕ
⊢ Eq (α := k) (MvPolynomial.coeff m ((fun (x : MvPolynomial (Vars k) k) ↦ q • x) p))
    (MvPolynomial.coeff m
      ((fun (x1 x2 : MvPolynomial (Vars k) k) ↦ x1 * x2)
        ((algebraMap k (MvPolynomial (Vars k) k) : (a : k) → MvPolynomial (Vars k) k) (↑q : k)) p))

Tactic:
simp [MvPolynomial.algebraMap_eq, Rat.smul_def]

Premises used: MvPolynomial.algebraMap_eq, Rat.smul_def
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
f : Monics k
a :
  ∀ (n : ℕ),
    Eq (α := AlgebraicClosure k) (coeff (map (algebraMap k (AlgebraicClosure k)) (↑f : k[X])) n)
      (coeff
        (∏ i : Fin (↑f : k[X]).natDegree,
          map (Ideal.Quotient.mk (maxIdeal k))
            (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)
⊢ Eq (α := (AlgebraicClosure k)[X]) (map (algebraMap k (AlgebraicClosure k)) (↑f : k[X]))
    (∏ i : Fin (↑f : k[X]).natDegree,
      map (Ideal.Quotient.mk (maxIdeal k))
        (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])))

Tactic:
ext
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
f : Monics k
n : ℕ
a : Membership.mem (γ := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k) ((subProdXSubC f).coeff n)
⊢ Eq (α := HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
    (coeff
      (map
        (algebraMap k
          (HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k)))
        (↑f : k[X]))
      n)
    (coeff
      (∏ i : Fin (↑f : k[X]).natDegree,
        map (Ideal.Quotient.mk (maxIdeal k))
          (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)

Tactic:
rw [← Ideal.Quotient.mk_comp_algebraMap, ← map_map, ← Polynomial.map_prod, ← sub_eq_zero,
    ← coeff_sub, ← Polynomial.map_sub, ← subProdXSubC, coeff_map, Ideal.Quotient.eq_zero_iff_mem]

Premises used: Polynomial.coeff_map, sub_eq_zero, Ideal.Quotient.eq_zero_iff_mem, Polynomial.map_prod, Polynomial.coeff_sub, Polynomial.map_sub, Ideal.Quotient.mk_comp_algebraMap, Polynomial.map_map, AlgebraicClosure.subProdXSubC
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
f : Monics k
n : ℕ
⊢ Membership.mem (γ := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k) ((subProdXSubC f).coeff n)

Tactic:
le_maxIdeal _ (Ideal.subset_span ⟨⟨f, _⟩, rfl⟩)

Premises used: Ideal.subset_span, Set.Mem, Prod.mk, AlgebraicClosure.le_maxIdeal, Exists.intro, rfl