-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
mp : ∀ (H : IsIntegral (MvPolynomial σ R) f) (n : σ →₀ ℕ), IsIntegral R (coeff n f)
refine : ∀ (H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)), IsIntegral (MvPolynomial σ R) f
mp₁ : ∀ (H : IsIntegral (MvPolynomial σ R) f) (n : σ →₀ ℕ), IsIntegral R (coeff n f)
mp₂ :
  ∀ (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
have mp₃ : ∀ (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f) (n : σ →₀ ℕ)
  (this :
    ∀ {σ : Type w} {f : MvPolynomial σ S}
      (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
      (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f))
  (hσ : ¬Finite σ), IsIntegral R (coeff n f)
Tactic: classical
  refine ⟨fun H n ↦ ?mp, fun H ↦ ?mpr⟩
  case mpr =>
    rw [← f.support_sum_monomial_coeff]
    simp_rw [monomial_eq]
    refine IsIntegral.sum _ fun n _ ↦ .mul ((H n).map (Algebra.ofId _ _)).tower_top
      (.prod _ fun i _ ↦ .pow ?_ _)
    convert! isIntegral_algebraMap (x := MvPolynomial.X i)
    simp only [algebraMap_def, map_X]
  unfold IsIntegral at H
  wlog hσ : Finite σ generalizing σ
  · obtain ⟨g, hg⟩ := MvPolynomial.exists_rename_eq_of_vars_subset_range (τ := f.vars) f _
      Subtype.val_injective (by simp)
    by_cases hn : n ∈ Set.range (Finsupp.mapDomain ((↑) : f.vars → σ))
    · obtain ⟨n, rfl⟩ := hn
      simp_rw [← hg, coeff_rename_mapDomain _ Subtype.val_injective]
      exact this (f := g) (RingHom.IsIntegralElem.of_map
        (g := (rename ((↑) : f.vars → σ)).toRingHom) (rename_injective _ Subtype.val_injective)
        (.of_comp (f := (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective).toRingHom) <| by
        simp only [AlgHom.toRingHom_eq_coe, algebraMap_def, RingHom.coe_coe, hg]
        convert!
          H.map
            ((rename Subtype.val).comp
                (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom
        · exact RingHom.ext (by simp [MvPolynomial.killCompl_map])
        · nth_rw 1 12 [← hg]; simp)) n (.of_fintype _)
    · rw [← hg, coeff_rename_eq_zero _ _ _ (by grind)]
      exact isIntegral_zero
  revert f n
  apply Finite.induction_empty_option _ _ _ σ
  · intro α β e IH f H n
    have := @IH (rename e.symm f) (.of_map (g := (rename e).toRingHom)
      (rename_injective _ e.injective) <| .of_comp (f := (rename e.symm).toRingHom)
        (by convert! H <;> aesop)) (n.embDomain e.symm)
    simpa [Finsupp.embDomain_eq_mapDomain, coeff_rename_mapDomain _ e.symm.injective] using this
  · intro f H n
    refine .of_map (g := (isEmptyAlgEquiv _ PEmpty).symm.toRingHom)
      (isEmptyAlgEquiv _ PEmpty).symm.injective
      (.of_comp (f := (isEmptyAlgEquiv _ PEmpty).toRingHom) ?_)
    convert! H
    · aesop (add simp MvPolynomial.isEmptyAlgEquiv)
    · obtain rfl := Subsingleton.elim n 0
      have : constantCoeff = (isEmptyAlgEquiv S PEmpty).toRingHom := by aesop
      simpa [-EmbeddingLike.apply_eq_iff_eq, -isEmptyAlgEquiv_apply] using
        congr((isEmptyAlgEquiv S PEmpty.{w + 1}).symm ($this f))
  · intro α _ IH f H n
    have := IH (IsIntegral.coeff (R := MvPolynomial α R)
      (p := optionEquivLeft _ _ f) (.of_map
      (g := (optionEquivLeft _ _).symm.toRingHom) (optionEquivLeft _ _).symm.injective
      (.of_comp (f := (optionEquivLeft _ _).toRingHom) (by
        convert! H
        · ext i m
          · aesop
          · cases i <;> aesop
        · aesop))) (n .none)) n.some
    rwa [optionEquivLeft_coeff_some_coeff_none] at this