Porting note: change rw to erw

[pitmonticone]

Classifies porting notes claiming:

change rw to erw

Examples

mathlib4/Mathlib/AlgebraicGeometry/Pullbacks.lean

Lines 269 to 282 in ee3a8f2

	/-- The first projection from the glued scheme into `X`. -/
	def p1 : (gluing 𝒰 f g).glued ⟶ X := by
	fapply Multicoequalizer.desc
	exact fun i => pullback.fst ≫ 𝒰.map i
	rintro ⟨i, j⟩
	change pullback.fst ≫ _ ≫ 𝒰.map i = (_ ≫ _) ≫ _ ≫ 𝒰.map j
	-- Porting note: change `rw` to `erw`
	erw [pullback.condition]
	rw [← Category.assoc]
	congr 1
	rw [Category.assoc]
	exact (t_fst_fst _ _ _ _ _).symm
	#align algebraic_geometry.Scheme.pullback.p1 AlgebraicGeometry.Scheme.Pullback.p1

mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Lines 216 to 227 in ee3a8f2

	theorem imageBasicOpen_image_open :
	IsOpen ((coequalizer.π f.1 g.1).base '' (imageBasicOpen f g U s).1) := by
	rw [← (TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget _) f.1
	g.1)).isOpen_preimage, TopCat.coequalizer_isOpen_iff, ← Set.preimage_comp]
	erw [← coe_comp]
	rw [PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison]
	dsimp only [SheafedSpace.forget]
	-- Porting note: change `rw` to `erw`
	erw [imageBasicOpen_image_preimage]
	exact (imageBasicOpen f g U s).2
	#align algebraic_geometry.LocallyRingedSpace.has_coequalizer.image_basic_open_image_open AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open