Porting note: added dsimp only

[pitmonticone]

Classifies porting notes claiming added dsimp only.

Examples

mathlib4/Mathlib/RingTheory/IsAdjoinRoot.lean

Lines 212 to 231 in 4c3321a

	-- To match `AdjoinRoot.lift`
	/-- Lift a ring homomorphism `R →+* T` to `S →+* T` by specifying a root `x` of `f` in `T`,
	where `S` is given by adjoining a root of `f` to `R`. -/
	def lift (h : IsAdjoinRoot S f) : S →+* T where
	toFun z := (h.repr z).eval₂ i x
	map_zero' := by
	dsimp only -- Porting note: added
	rw [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ (map_zero _), eval₂_zero]
	map_add' z w := by
	dsimp only -- Porting note: added
	rw [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z + h.repr w), eval₂_add]
	· rw [map_add, map_repr, map_repr]
	map_one' := by
	dsimp only -- Porting note: added
	rw [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ (map_one _), eval₂_one]
	map_mul' z w := by
	dsimp only -- Porting note: added
	rw [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z * h.repr w), eval₂_mul]
	· rw [map_mul, map_repr, map_repr]
	#align is_adjoin_root.lift IsAdjoinRoot.lift

[grunweg]

Some of these turn out to be #12129; I'm re-classifying these in #12130.