awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
refine le_maxIdeal _ (Ideal.subset_span ⟨⟨f, _⟩, rfl⟩)

Premises used: Ideal.subset_span, Prod.mk, AlgebraicClosure.le_maxIdeal, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
z : AlgebraicClosure k
let :
  ∀ (p : MvPolynomial (Vars k) k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
    IsIntegral k z
⊢ IsIntegral k z

Tactic:
let ⟨p, hp⟩ := Ideal.Quotient.mk_surjective z
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
z : AlgebraicClosure k
p : MvPolynomial (Vars k) k
hp : (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z
rw :
  IsIntegral k (A := AlgebraicClosure k)
    ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
      HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
⊢ IsIntegral k z

Tactic:
rw [← hp]
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
a : k
z : AlgebraicClosure k
hp :
  (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
      ((MvPolynomial.C : (a : k) → MvPolynomial (Vars k) k) a) =
    z
⊢ IsIntegral k (A := AlgebraicClosure k)
    ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
        ((MvPolynomial.C : (a : k) → MvPolynomial (Vars k) k) a) :
      HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))

Tactic:
isIntegral_algebraMap

Premises used: Submodule.Quotient.mk, isIntegral_algebraMap
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
a : k
z : AlgebraicClosure k
hp :
  (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
      ((MvPolynomial.C : (a : k) → MvPolynomial (Vars k) k) a) =
    z
⊢ IsIntegral k (A := AlgebraicClosure k)
    ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
        ((MvPolynomial.C : (a : k) → MvPolynomial (Vars k) k) a) :
      HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))

Tactic:
exact isIntegral_algebraMap

Premises used: isIntegral_algebraMap
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
p q : MvPolynomial (Vars k) k
ha :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
hb :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) q = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) q :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) (p + q) = z
⊢ IsIntegral k (A := AlgebraicClosure k)
    ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) (p + q) :
      HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))

Tactic:
(ha _ rfl).add (hb _ rfl)

Premises used: Submodule.Quotient.mk, IsIntegral.add, Quotient.map₂, AddMonoidAlgebra, rfl
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
p q : MvPolynomial (Vars k) k
ha :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
hb :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) q = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) q :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) (p + q) = z
⊢ IsIntegral k (A := AlgebraicClosure k)
    ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) (p + q) :
      HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))

Tactic:
exact (ha _ rfl).add (hb _ rfl)

Premises used: IsIntegral.add, rfl
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
z : AlgebraicClosure k
hp :
  (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
      (p * MvPolynomial.X fi) =
    z
mul_X :
  IsIntegral k
    (HMul.hMul (α := HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
      (β := HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
          (MvPolynomial.X fi) :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k)))
⊢ IsIntegral k (A := AlgebraicClosure k)
    ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
        (p * MvPolynomial.X fi) :
      HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
z : AlgebraicClosure k
hp :
  (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
      (p * MvPolynomial.X fi) =
    z
⊢ IsIntegral k
    (HMul.hMul (α := HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
      (β := HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
          (MvPolynomial.X fi) :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k)))

Tactic:
(ih _ rfl).mul ⟨_, fi.1.2, ?_⟩

Premises used: IsIntegral.mul, Sigma.fst, And.intro, Exists.intro, rfl, Subtype.property
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
z : AlgebraicClosure k
hp :
  (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
      (p * MvPolynomial.X fi) =
    z
mul_X :
  Eq (α := AlgebraicClosure k)
    (eval₂ (algebraMap k (AlgebraicClosure k))
        ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
          (MvPolynomial.X fi))
        (↑(fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)) : k[X]) :
      AlgebraicClosure k)
    (0 : AlgebraicClosure k)
⊢ IsIntegral k
    (HMul.hMul (α := HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
      (β := HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
          (MvPolynomial.X fi) :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k)))

Tactic:
refine (ih _ rfl).mul ⟨_, fi.1.2, ?_⟩

Premises used: IsIntegral.mul, Sigma.fst, And.intro, Exists.intro, rfl, Subtype.property
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
z : AlgebraicClosure k
hp :
  (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
      (p * MvPolynomial.X fi) =
    z
mul_X :
  Eq.{u + 1} (α := AlgebraicClosure k)
    (∏ x : Fin (↑fi.fst : k[X]).natDegree,
      HSub.hSub (α := AlgebraicClosure k) (β := AlgebraicClosure k)
        (eval
            ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
              (MvPolynomial.X fi))
            (map (Ideal.Quotient.mk (maxIdeal k)) X) :
          AlgebraicClosure k)
        (eval
            ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
              (MvPolynomial.X fi))
            (map (Ideal.Quotient.mk (maxIdeal k))
              ((C : (a : MvPolynomial (Vars k) k) → (MvPolynomial (Vars k) k)[X])
                (MvPolynomial.X
                  (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)
                    (fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)) x)))) :
          AlgebraicClosure k))
    0
⊢ Eq (α := AlgebraicClosure k)
    (eval₂ (algebraMap k (AlgebraicClosure k))
        ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
          (MvPolynomial.X fi))
        (↑(fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)) : k[X]) :
      AlgebraicClosure k)
    (0 : AlgebraicClosure k)

Tactic:
simp_rw [← eval_map, Monics.map_eq_prod, eval_prod, Polynomial.map_sub, eval_sub]

Premises used: Polynomial.eval_prod, Polynomial.eval_map, AlgebraicClosure.Monics.map_eq_prod, Polynomial.map_sub, Polynomial.eval_sub
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
z : AlgebraicClosure k
hp :
  (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
      (p * MvPolynomial.X fi) =
    z
mul_X :
  HSub.hSub (α := AlgebraicClosure k) (β := AlgebraicClosure k)
      (eval
          ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
            (MvPolynomial.X fi))
          (map (Ideal.Quotient.mk (maxIdeal k)) X) :
        AlgebraicClosure k)
      (eval
          ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
            (MvPolynomial.X fi))
          (map (Ideal.Quotient.mk (maxIdeal k))
            ((C : (a : MvPolynomial (Vars k) k) → (MvPolynomial (Vars k) k)[X])
              (MvPolynomial.X
                (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)
                  (fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree))
                  (fi.snd (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)))))) :
        AlgebraicClosure k) =
    0
⊢ Eq.{u + 1} (α := AlgebraicClosure k)
    (∏ x : Fin (↑fi.fst : k[X]).natDegree,
      HSub.hSub (α := AlgebraicClosure k) (β := AlgebraicClosure k)
        (eval
            ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
              (MvPolynomial.X fi))
            (map (Ideal.Quotient.mk (maxIdeal k)) X) :
          AlgebraicClosure k)
        (eval
            ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
              (MvPolynomial.X fi))
            (map (Ideal.Quotient.mk (maxIdeal k))
              ((C : (a : MvPolynomial (Vars k) k) → (MvPolynomial (Vars k) k)[X])
                (MvPolynomial.X
                  (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)
                    (fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)) x)))) :
          AlgebraicClosure k))
    0

Tactic:
apply Finset.prod_eq_zero (Finset.mem_univ fi.2)

Premises used: Finset.mem_univ, Finset.prod_eq_zero, Sigma.snd
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
z : AlgebraicClosure k
hp :
  (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
      (p * MvPolynomial.X fi) =
    z
mul_X :
  HSub.hSub (α := AlgebraicClosure k) (β := AlgebraicClosure k)
      (eval
          ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
            (MvPolynomial.X fi))
          (map (Ideal.Quotient.mk (maxIdeal k)) X) :
        AlgebraicClosure k)
      (eval
          ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
            (MvPolynomial.X fi))
          ((C : (a : MvPolynomial (Vars k) k ⧸ maxIdeal k) → (MvPolynomial (Vars k) k ⧸ maxIdeal k)[X])
            ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
              (MvPolynomial.X
                (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)
                  (fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree))
                  (fi.snd (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)))))) :
        AlgebraicClosure k) =
    0
⊢ HSub.hSub (α := AlgebraicClosure k) (β := AlgebraicClosure k)
      (eval
          ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
            (MvPolynomial.X fi))
          (map (Ideal.Quotient.mk (maxIdeal k)) X) :
        AlgebraicClosure k)
      (eval
          ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
            (MvPolynomial.X fi))
          (map (Ideal.Quotient.mk (maxIdeal k))
            ((C : (a : MvPolynomial (Vars k) k) → (MvPolynomial (Vars k) k)[X])
              (MvPolynomial.X
                (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)
                  (fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree))
                  (fi.snd (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)))))) :
        AlgebraicClosure k) =
    0

Tactic:
rw [map_C]

Premises used: Polynomial.map_C
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
z : AlgebraicClosure k
hp :
  (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
      (p * MvPolynomial.X fi) =
    z
mul_X :
  HSub.hSub (α := AlgebraicClosure k) (β := AlgebraicClosure k)
      (eval
          ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
            (MvPolynomial.X fi))
          (map (Ideal.Quotient.mk (maxIdeal k)) X) :
        AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
          (MvPolynomial.X
            (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)
              (fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree))
              (fi.snd (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)))) :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k)) =
    0
⊢ HSub.hSub (α := AlgebraicClosure k) (β := AlgebraicClosure k)
      (eval
          ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
            (MvPolynomial.X fi))
          (map (Ideal.Quotient.mk (maxIdeal k)) X) :
        AlgebraicClosure k)
      (eval
          ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
            (MvPolynomial.X fi))
          ((C : (a : MvPolynomial (Vars k) k ⧸ maxIdeal k) → (MvPolynomial (Vars k) k ⧸ maxIdeal k)[X])
            ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
              (MvPolynomial.X
                (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)
                  (fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree))
                  (fi.snd (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)))))) :
        AlgebraicClosure k) =
    0

Tactic:
erw [eval_C]

Premises used: Polynomial.eval_C
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
z : AlgebraicClosure k
hp :
  (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
      (p * MvPolynomial.X fi) =
    z
⊢ HSub.hSub (α := AlgebraicClosure k) (β := AlgebraicClosure k)
      (eval
          ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
            (MvPolynomial.X fi))
          (map (Ideal.Quotient.mk (maxIdeal k)) X) :
        AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
          (MvPolynomial.X
            (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)
              (fi.fst (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree))
              (fi.snd (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)))) :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k)) =
    0

Tactic:
simp
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
f : k[X]
hf : f.Monic
h : Irreducible f
rw :
  Splits.{u} (R := AlgebraicClosure k)
    (∏ i : Fin (↑⟨f, hf⟩ : 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)
                  (Subtype.mk (p := fun (f : k[X]) ↦ f.Monic) f hf) i)) :
            (MvPolynomial (Vars k) k)[X])))
⊢ Splits (R := AlgebraicClosure k) (map (algebraMap k (AlgebraicClosure k)) f)

Tactic:
rw [show f = (⟨f, hf⟩ : Monics k) from rfl, Monics.map_eq_prod]

Premises used: AlgebraicClosure.Monics.map_eq_prod, rfl