-- 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
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
obtain :
  ∀ (m : Multiset S)
    (hm :
      p =
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
          (Multiset.prod
              (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m) :
            S[X])),
    IsIntegral R (p.coeff i)
obtain₁ :
  ∀ (m : Multiset S)
    (hm :
      p =
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
          (Multiset.prod
              (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m) :
            S[X])),
    IsIntegral R
      (p.leadingCoeff *
        coeff
          (∏ x : (Multiset.map (fun (x : S) ↦ X - (C : (a : S) → S[X]) x) m).ToType,
            x.fst (β := fun (x : S[X]) ↦
              Fin
                (Multiset.count x
                  (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                    m))))
          i)
obtain₂ :
  ∀ (m : Multiset S)
    (hm :
      p =
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
          (Multiset.prod
              (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m) :
            S[X]))
    (i :
      Multiset.ToType (α := S[X])
        (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)),
    Membership.mem (γ :=
        Finset
          (Multiset.ToType (α := S[X])
            (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
        Finset.univ i →
      ∀ (j : ℕ),
        IsIntegral R
          (i.fst (β := fun (x : S[X]) ↦
                Fin
                  (Multiset.count x
                    (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                      m))).coeff
            j)
obtain₃ :
  ∀ (m : Multiset S)
    (hm :
      p =
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
          (Multiset.prod
              (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m) :
            S[X]))
    (H : ∀ {x : S} (hx : x ∈ m), p.IsRoot x)
    (i :
      Multiset.ToType (α := S[X])
        (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)),
    Membership.mem (γ :=
        Finset
          (Multiset.ToType (α := S[X])
            (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
        Finset.univ i →
      ∀ (j : ℕ),
        IsIntegral R
          (i.fst (β := fun (x : S[X]) ↦
                Fin
                  (Multiset.count x
                    (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                      m))).coeff
            j)
obtain₄ :
  ∀ (m : Multiset S)
    (hm :
      p =
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
          (Multiset.prod
              (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m) :
            S[X]))
    (H : ∀ {x : S} (hx : x ∈ m), p.IsRoot x) (a : S[X]) (i : ℕ)
    (hi :
      i <
        Multiset.count a
          (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m))
    (j : ℕ),
    IsIntegral R
      ((Sigma.fst (β := fun (x : S[X]) ↦
            Fin
              (Multiset.count x
                (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
            (Sigma.mk (β := fun (x : S[X]) ↦
              Fin
                (Multiset.count x
                  (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
              a
              (⟨i, hi⟩ :
                Fin
                  (Multiset.count a
                    (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                      m))))).coeff
        j)
obtain₅ :
  ∀ (m : Multiset S)
    (hm :
      p =
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
          (Multiset.prod
              (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m) :
            S[X]))
    (H : ∀ {x : S} (hx : x ∈ m), p.IsRoot x) (i : ℕ) (x : S) (hx : x ∈ m)
    (hi :
      i <
        Multiset.count (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
          (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m))
    (j : ℕ),
    IsIntegral R
      ((Sigma.fst (β := fun (x : S[X]) ↦
            Fin
              (Multiset.count x
                (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
            (Sigma.mk (β := fun (x : S[X]) ↦
              Fin
                (Multiset.count x
                  (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
              (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
              (⟨i, hi⟩ :
                Fin
                  (Multiset.count (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                    (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                      m))))).coeff
        j)
⊢ IsIntegral R (p.coeff i)

Tactic:
classical
  obtain ⟨m, hm⟩ := Polynomial.splits_iff_exists_multiset.mp hp
  rw [hm, Multiset.prod_eq_prod_coe, coeff_C_mul]
  refine .mul hpmon (isIntegral_coeff_prod _ _ ?_ _)
  have H {x} (hx : x ∈ m) : p.IsRoot x := by
    rw [IsRoot, hm, eval_mul, eval_multiset_prod, Multiset.prod_eq_zero, mul_zero]
    simpa [sub_eq_zero]
  rintro ⟨a, ⟨i, hi⟩⟩ -
  obtain ⟨x, hx, rfl⟩ := Multiset.mem_map.mp (Multiset.count_pos.mp (i.zero_le.trans_lt hi))
  simp [coeff_X, coeff_C, IsIntegral.sub, apply_ite (IsIntegral R),
    isIntegral_one, isIntegral_zero, hpr x (H hx)]

Premises used: Polynomial.splits_iff_exists_multiset, Polynomial.coeff_C_mul, apply_ite, IsIntegral.sub, Multiset.prod_eq_prod_coe, Polynomial.coeff_C, IsIntegral, isIntegral_one, Iff.mp, isIntegral_zero, Polynomial.coeff_X, rfl