-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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)
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)
refine₁ refine₂ :
  ∀ {σ : 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)
refine₃ :
  ∀ {σ : Type w} (hσ : Finite σ) {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ), IsIntegral R (coeff n f)
refine₄ :
  ∀ {σ : Type w} (hσ : Finite σ) {α β : Type w} (a : α ≃ β),
    (∀ {f : MvPolynomial α S}
        (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
        (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial β S}
        (H : RingHom.IsIntegralElem (R := MvPolynomial β R) (algebraMap (MvPolynomial β R) (MvPolynomial β S)) f)
        (n : β →₀ ℕ), IsIntegral R (coeff n f)
refine₅ :
  ∀ {σ : Type w} (hσ : Finite σ) {f : MvPolynomial PEmpty.{w + 1} S}
    (H :
      RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R)
        (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) f)
    (n : PEmpty.{w + 1} →₀ ℕ), IsIntegral R (coeff n f)
refine₆ :
  ∀ {σ : Type w} (hσ : Finite σ) {α : Type w} [Fintype α],
    (∀ {f : MvPolynomial α S}
        (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
        (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial.{w, u_2} (Option α) S}
        (H :
          RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
            (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f)
        (n : Option α →₀ ℕ), IsIntegral R (coeff n f)
refine₇ :
  ∀ {σ : Type w} (hσ : Finite σ) {f : MvPolynomial PEmpty.{w + 1} S}
    (H :
      RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R)
        (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) f)
    (n : PEmpty.{w + 1} →₀ ℕ), IsIntegral R (coeff n f)
refine₈ refine₉ :
  ∀ {σ : Type w} (hσ : Finite σ) {α : Type w} [Fintype α],
    (∀ {f : MvPolynomial α S}
        (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
        (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial.{w, u_2} (Option α) S}
        (H :
          RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
            (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f)
        (n : Option α →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), 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

Premises used: Subtype.val_injective, Finite, Finsupp.mapDomain, MvPolynomial.exists_rename_eq_of_vars_subset_range, MvPolynomial.coeff_rename_mapDomain, EmbeddingLike.apply_eq_iff_eq, MvPolynomial.isEmptyAlgEquiv, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, MvPolynomial.isEmptyAlgEquiv_apply, IsIntegral, MvPolynomial.support_sum_monomial_coeff, MvPolynomial.monomial_eq, Finsupp.embDomain_eq_mapDomain, Set.range, isIntegral_zero, MvPolynomial.coeff_rename_eq_zero, Subtype.val, MvPolynomial.map_X, rfl, MvPolynomial.algebraMap_def