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.9366
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ coeff (integerNormalization M p) i = coeffIntegerNormalization M p i
simp (config := { contextual := true }) [integerNormalization, coeff_monomial,
  coeffIntegerNormalization_of_not_mem_support]