awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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)
⊢ (algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q : k) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
have 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: rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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)
⊢ (algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q : k) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
have 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)
Tactic: rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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)
⊢ (algebraMap k (AlgebraicClosure k) : (a : k) → AlgebraicClosure k) (↑q : k) =
    HDiv.hDiv (α := AlgebraicClosure k) (↑q.num : AlgebraicClosure k) (↑q.den : AlgebraicClosure k)
have 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)
Tactic: rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
q : ℚ
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
f : Monics k
⊢ 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])))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
f : Monics k
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)
have a : Membership.mem (γ := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k) ((subProdXSubC f).coeff 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]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
z : AlgebraicClosure k
⊢ IsIntegral k z
have 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
Tactic: let ⟨p, hp⟩ := Ideal.Quotient.mk_surjective z
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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
⊢ IsIntegral k z
have 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))
Tactic: rw [← hp]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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 (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))
have 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)))
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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)))
have 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)
Tactic: refine (ih _ rfl).mul ⟨_, fi.1.2, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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
⊢ 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)
have 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
Tactic: simp_rw [← eval_map, Monics.map_eq_prod, eval_prod, Polynomial.map_sub, eval_sub]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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
⊢ 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
have 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
Tactic: apply Finset.prod_eq_zero (Finset.mem_univ fi.2)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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)
      (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
have 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
Tactic: rw [map_C]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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)
      (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
have 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
Tactic: erw [eval_C]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
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
⊢ 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))
have C : ∀ (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: induction p using MvPolynomial.induction_on generalizing z with
        | C => exact isIntegral_algebraMap
        | add _ _ ha hb => exact (ha _ rfl).add (hb _ rfl)
        | mul_X p fi ih =>
          rw [map_mul]
          refine (ih _ rfl).mul ⟨_, fi.1.2, ?_⟩
          simp_rw [← eval_map, Monics.map_eq_prod, eval_prod, Polynomial.map_sub, eval_sub]
          apply Finset.prod_eq_zero (Finset.mem_univ fi.2)
          rw [map_C]
          -- The `erw` is needed here because the `R` in `eval` is `AlgebraicClosure k`,
          -- but this has been unfolded in the arguments of `eval`.
          erw [eval_C]
          simp
Cleared hypotheses: z, p, hp