no goals
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
i : ℕ
r : R
⊢ ↑(monomial i) r ∈ reesAlgebra I ↔ r ∈ I ^ i
simp (config := { contextual := true }) [mem_reesAlgebra_iff_support, coeff_monomial, ←
  imp_iff_not_or]