chore: add missing mem lemmas (#33801)

* Add missing `simp` lemmas `mem_foo` where a `simp` lemma `coe_foo` already exists

Author: artie2000

Mathlib/AlgebraicGeometry/OpenImmersion.lean

@@ -81,6 +81,10 @@ theorem isOpenEmbedding : IsOpenEmbedding f :=
 def opensRange : Y.Opens :=
   ⟨_, f.isOpenEmbedding.isOpen_range⟩
 
+@[simp]
+theorem mem_opensRange {X Y : Scheme} {f : X ⟶ Y} [H : IsOpenImmersion f] {y : Y} :
+    y ∈ opensRange f ↔ ∃ x, (ConcreteCategory.hom f.base) x = y := .rfl
+
 /-- The functor `opens X ⥤ opens Y` associated with an open immersion `f : X ⟶ Y`. -/
 def opensFunctor : X.Opens ⥤ Y.Opens :=
   LocallyRingedSpace.IsOpenImmersion.opensFunctor f.toLRSHom

Mathlib/AlgebraicGeometry/Scheme.lean

@@ -216,7 +216,6 @@ protected lemma ext {f g : X ⟶ Y} (h_base : f.base = g.base)
 protected lemma ext' {f g : X ⟶ Y} (h : f.toLRSHom = g.toLRSHom) : f = g := by
   cases f; cases g; congr 1
 
-@[simp]
 lemma mem_preimage {x : X} {U : Opens Y} : x ∈ f ⁻¹ᵁ U ↔ f x ∈ U := .rfl
 
 lemma coe_preimage {U : Opens Y} : f ⁻¹ᵁ U = f ⁻¹' U := rfl

Mathlib/RingTheory/FractionalIdeal/Basic.lean

@@ -380,11 +380,11 @@ variable (S)
 theorem coeIdeal_top : ((⊤ : Ideal R) : FractionalIdeal S P) = 1 :=
   rfl
 
+@[simp]
 theorem mem_one_iff {x : P} : x ∈ (1 : FractionalIdeal S P) ↔ ∃ x' : R, algebraMap R P x' = x :=
   Iff.intro (fun ⟨x', _, h⟩ => ⟨x', h⟩) fun ⟨x', h⟩ => ⟨x', ⟨⟩, h⟩
 
-theorem coe_mem_one (x : R) : algebraMap R P x ∈ (1 : FractionalIdeal S P) :=
-  (mem_one_iff S).mpr ⟨x, rfl⟩
+theorem coe_mem_one (x : R) : algebraMap R P x ∈ (1 : FractionalIdeal S P) := by simp
 
 theorem one_mem_one : (1 : P) ∈ (1 : FractionalIdeal S P) :=
   (mem_one_iff S).mpr ⟨1, map_one _⟩

Mathlib/RingTheory/FractionalIdeal/Extended.lean

@@ -103,7 +103,7 @@ theorem extended_one : extended L hf (1 : FractionalIdeal M K) = 1 := by
     ?_ (zero_mem _) (fun y z _ _ hy hz ↦ add_mem hy hz) (fun b y _ hy ↦ smul_mem _ b hy) hx, ?_⟩
   · rintro ⟨b, _, rfl⟩
     rw [Algebra.linearMap_apply, Algebra.algebraMap_eq_smul_one]
-    exact smul_mem _ _ <| subset_span ⟨1, by simp [one_mem_one]⟩
+    exact smul_mem _ _ <| subset_span ⟨1, by simpa using one_mem_one⟩
   · rintro _ ⟨_, ⟨a, ha, rfl⟩, rfl⟩
     exact ⟨f a, ha, by rw [Algebra.linearMap_apply, Algebra.linearMap_apply, map_eq]⟩
 

Mathlib/Topology/Category/TopCat/Opens.lean

@@ -154,6 +154,10 @@ def map (f : X ⟶ Y) : Opens Y ⥤ Opens X where
 theorem map_coe (f : X ⟶ Y) (U : Opens Y) : ((map f).obj U : Set X) = f ⁻¹' (U : Set Y) :=
   rfl
 
+@[simp]
+theorem mem_map {f : X ⟶ Y} {U : Opens Y} {x : X} :
+    x ∈ (map f).obj U ↔ f.hom x ∈ U := .rfl
+
 @[simp]
 theorem map_obj (f : X ⟶ Y) (U) (p) : (map f).obj ⟨U, p⟩ = ⟨f ⁻¹' U, p.preimage f.hom.continuous⟩ :=
   rfl

Mathlib/Topology/Sets/Opens.lean

@@ -171,6 +171,10 @@ lemma mem_inf {s t : Opens α} {x : α} : x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t
 theorem coe_sup (s t : Opens α) : (↑(s ⊔ t) : Set α) = ↑s ∪ ↑t :=
   rfl
 
+@[simp]
+theorem mem_sup {s t : Opens α} {x : α} : x ∈ (s ⊔ t) ↔ x ∈ s ∨ x ∈ t :=
+  .rfl
+
 @[simp, norm_cast]
 theorem coe_bot : ((⊥ : Opens α) : Set α) = ∅ :=
   rfl