chore(Geometry/RingedSpace): remove use of erw in isUnit_of_isUnit_germ (#27660)

Author: euprunin

Mathlib/Geometry/RingedSpace/Basic.lean

@@ -102,9 +102,8 @@ theorem isUnit_of_isUnit_germ (U : Opens X) (f : X.presheaf.obj (op U))
   choose V iVU m h_unit using fun x : U => X.isUnit_res_of_isUnit_germ U f x x.2 (h x.1 x.2)
   have hcover : U ≤ iSup V := by
     intro x hxU
-    -- Porting note: in Lean3 `rw` is sufficient
-    erw [Opens.mem_iSup]
-    exact ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩
+    simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe, Subtype.exists]
+    tauto
   -- Let `g x` denote the inverse of `f` in `U x`.
   choose g hg using fun x : U => IsUnit.exists_right_inv (h_unit x)
   have ic : IsCompatible (sheaf X).val V g := by