-- 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
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))
⊢ 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 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))
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