-- 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
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)
⊢ IsIntegral R (p.coeff i)
have 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)
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)]