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