-- 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
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))
add :
  ∀ (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))
mul_X :
  ∀ (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))
⊢ 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:
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

Premises used: Polynomial.C, Polynomial.eval_prod, Polynomial.eval_map, Polynomial.eval_C, isIntegral_algebraMap, MvPolynomial.induction_on, map_mul, AlgebraicClosure.Monics.map_eq_prod, Polynomial.map_sub, Polynomial.map_C, Polynomial.eval_sub