Porting note: was `rw`

[pitmonticone]

Classifies porting notes claiming was rw.

Examples

mathlib4/Mathlib/AlgebraicGeometry/OpenImmersion.lean

Lines 556 to 572 in 9a04ccc

	theorem range_pullback_snd_of_left :
	Set.range (pullback.snd : pullback f g ⟶ Y).1.base =
	((Opens.map g.1.base).obj ⟨Set.range f.1.base, H.base_open.open_range⟩).1 := by
	rw [←
	show _ = (pullback.snd : pullback f g ⟶ _).1.base from
	PreservesPullback.iso_hom_snd Scheme.forgetToTop f g]
	-- Porting note : was `rw`
	erw [coe_comp]
	rw [Set.range_comp, Set.range_iff_surjective.mpr, ←
	@Set.preimage_univ _ _ (pullback.fst : pullback f.1.base g.1.base ⟶ _)]
	-- Porting note : was `rw`
	erw [TopCat.pullback_snd_image_fst_preimage]
	rw [Set.image_univ]
	rfl
	rw [← TopCat.epi_iff_surjective]
	infer_instance
	#align algebraic_geometry.IsOpenImmersion.range_pullback_snd_of_left AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left

mathlib4/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

Lines 139 to 145 in 9a04ccc

	@[simp]
	theorem toEven_ι (m : M) : (toEven Q (ι Q m) : CliffordAlgebra (Q' Q)) = e0 Q * v Q m := by
	rw [toEven, CliffordAlgebra.lift_ι_apply]
	-- porting note: was `rw`
	erw [LinearMap.codRestrict_apply]
	rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]
	#align clifford_algebra.to_even_ι CliffordAlgebra.toEven_ι