no goals
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3630
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : coeff p i = 0
⊢ coeffIntegerNormalization M p i = 0
simp only [coeffIntegerNormalization, h, mem_support_iff, eq_self_iff_true, not_true, Ne.def,
  dif_neg, not_false_iff]