chore: remove use of erw in Geometry.RingedSpace.OpenImmersion (#31856)

Author: euprunin

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

@@ -491,7 +491,8 @@ def lift (H : Set.range g.base ⊆ Set.range f.base) : Y ⟶ X :=
 
 @[simp, reassoc]
 theorem lift_fac (H : Set.range g.base ⊆ Set.range f.base) : lift f g H ≫ f = g := by
-  erw [Category.assoc]; rw [IsIso.inv_comp_eq]; exact pullback.condition
+  simp [AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift,
+    CategoryTheory.Limits.pullback.condition]
 
 theorem lift_uniq (H : Set.range g.base ⊆ Set.range f.base) (l : Y ⟶ X) (hl : l ≫ f = g) :
     l = lift f g H := by rw [← cancel_mono f, hl, lift_fac]