mathlib

d065fd4a - feat(ring_theory/ideal): generalize `x mod I ∈ J mod I ↔ x ∈ J` (#13358)

feat(ring_theory/ideal): generalize `x mod I ∈ J mod I ↔ x ∈ J` (#13358) We already had a lemma like this assuming `I ≤ J`, and we can drop the assumption if we instead change the RHS to `x ∈ J \sup I`. This also golfs the proof of the original `mem_quotient_iff_mem`.