Theorem: Ideal.mem_quotSubmodule_iff (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
i : ι
g : A ⧸ I
⊢ g ∈ quotSubmodule R 𝒜 I i ↔ ∃ a ∈ 𝒜 i, (Quotient.mk I) a = g
Tactic:
rw [Ideal.quotSubmodule, Submodule.mem_map, Ideal.Quotient.mkₐ_eq_mk]
State after:
no goals