awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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)
      (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
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])))
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
⊢ 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 (↑(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
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
⊢ Ne (α := Ideal (MvPolynomial (Vars k) k)) (spanCoeffs k) ⊤
have 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)
Tactic: rw [Ideal.ne_top_iff_one, spanCoeffs, Ideal.span, ← Set.image_univ,
    Finsupp.mem_span_image_iff_linearCombination]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (hypothesis)
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)
⊢ False
have 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])))
Tactic: replace hv := congr_arg (toSplittingField <| v.support.image Prod.fst) hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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])))
⊢ False
have rw : ∀ (hv : Eq.{u + 1} (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) 0 1), False
Tactic: rw [map_one, Finsupp.linearCombination_apply, Finsupp.sum, map_sum, Finset.sum_eq_zero] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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
⊢ False
have 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])))
Tactic: rw [map_one, Finsupp.linearCombination_apply, Finsupp.sum, map_sum, Finset.sum_eq_zero] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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])))
    (∑ 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
j : Monics k × ℕ
hj : j ∈ 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) j : MvPolynomial (Vars k) k)
          ((subProdXSubC j.1).coeff j.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])))
have rw : 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)
      (HMul.hMul (α := MvPolynomial (Vars k) k)
        ((v : (a : Monics k × ℕ) → MvPolynomial (Vars k) k) j : MvPolynomial (Vars k) k)
        ((subProdXSubC j.1).coeff j.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])))
Tactic: rw [smul_eq_mul, map_mul, toSplittingField_coeff (Finset.mem_image_of_mem _ hj), mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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])))
    (∑ 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
j : Monics k × ℕ
hj : j ∈ v.support
rw :
  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)
        (HMul.hMul (α := MvPolynomial (Vars k) k)
          ((v : (a : Monics k × ℕ) → MvPolynomial (Vars k) k) j : MvPolynomial (Vars k) k)
          ((subProdXSubC j.1).coeff j.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])))
⊢ 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) j : MvPolynomial (Vars k) k)
          ((subProdXSubC j.1).coeff j.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])))
have rw₁ : HMul.hMul (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) (β :=
    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)
        ((v : (a : Monics k × ℕ) → MvPolynomial (Vars k) k) j) :
      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)
        ((subProdXSubC j.1).coeff j.2) :
      SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) =
  0
Tactic: rw [smul_eq_mul, map_mul, toSplittingField_coeff (Finset.mem_image_of_mem _ hj), mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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)
⊢ False
have replace : ∀
  (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])))),
  False
Tactic: classical
  replace hv := congr_arg (toSplittingField <| v.support.image Prod.fst) hv
  rw [map_one, Finsupp.linearCombination_apply, Finsupp.sum, map_sum, Finset.sum_eq_zero] at hv
  · exact zero_ne_one hv
  intro j hj
  rw [smul_eq_mul, map_mul, toSplittingField_coeff (Finset.mem_image_of_mem _ hj), mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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)
replace replace₁ replace₂ :
  ∀
    (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])))),
    False
⊢ False
have replace₃ : ∀ (hv : Eq.{u + 1} (α := SplittingField (K := k) (∏ f ∈ Finset.image Prod.fst v.support, (↑f : k[X]))) 0 1), False
Tactic: classical
  replace hv := congr_arg (toSplittingField <| v.support.image Prod.fst) hv
  rw [map_one, Finsupp.linearCombination_apply, Finsupp.sum, map_sum, Finset.sum_eq_zero] at hv
  · exact zero_ne_one hv
  intro j hj
  rw [smul_eq_mul, map_mul, toSplittingField_coeff (Finset.mem_image_of_mem _ hj), mul_zero]
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
q : ℚ≥0
⊢ (algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q : k) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
have 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)
Tactic: simp_rw [NNRat.cast_def, map_div₀, map_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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)
⊢ (algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q : k) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
have 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)
Tactic: simp_rw [NNRat.cast_def, map_div₀, map_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
q : ℚ≥0
x : AlgebraicClosure k
p : MvPolynomial (Vars k) k
⊢ 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)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
q : ℚ
⊢ (algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q : k) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
have 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)
Tactic: rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]