Porting note: added simp

[pitmonticone]

Classifies porting notes claiming anything equivalent to:

• "added dsimp"
• "dsimp added"
• "dsimp now needed"

Examples

mathlib4/Mathlib/RepresentationTheory/Basic.lean

Lines 449 to 465 in ee3a8f2

	/-- Given representations of `G` on `V` and `W`, there is a natural representation of `G` on the
	module `V →ₗ[k] W`, where `G` acts by conjugation.
	-/
	def linHom : Representation k G (V →ₗ[k] W) where
	toFun g :=
	{ toFun := fun f => ρW g ∘ₗ f ∘ₗ ρV g⁻¹
	map_add' := fun f₁ f₂ => by simp_rw [add_comp, comp_add]
	map_smul' := fun r f => by simp_rw [RingHom.id_apply, smul_comp, comp_smul] }
	map_one' :=
	LinearMap.ext fun x => by
	dsimp -- Porting note: now needed
	simp_rw [inv_one, map_one, one_eq_id, comp_id, id_comp]
	map_mul' g h :=
	LinearMap.ext fun x => by
	dsimp -- Porting note: now needed
	simp_rw [mul_inv_rev, map_mul, mul_eq_comp, comp_assoc]
	#align representation.lin_hom Representation.linHom

mathlib4/Mathlib/Topology/Sheaves/Skyscraper.lean

Lines 185 to 206 in ee3a8f2

	/--
	The cocone at `*` for the stalk functor of `skyscraperPresheaf p₀ A` when `y ∉ closure {p₀}` is a
	colimit
	-/
	noncomputable def skyscraperPresheafCoconeIsColimitOfNotSpecializes {y : X} (h : ¬p₀ ⤳ y) :
	IsColimit (skyscraperPresheafCocone p₀ A y) :=
	let h1 : ∃ U : OpenNhds y, p₀ ∉ U.1 :=
	let ⟨U, ho, h₀, hy⟩ := not_specializes_iff_exists_open.mp h
	⟨⟨⟨U, ho⟩, h₀⟩, hy⟩
	{ desc := fun c => eqToHom (if_neg h1.choose_spec).symm ≫ c.ι.app (op h1.choose)
	fac := fun c U => by
	change _ = c.ι.app (op U.unop)
	simp only [← c.w (homOfLE <| @inf_le_left _ _ h1.choose U.unop).op, ←
	c.w (homOfLE <| @inf_le_right _ _ h1.choose U.unop).op, ← Category.assoc]
	congr 1
	refine' ((if_neg _).symm.ndrec terminalIsTerminal).hom_ext _ _
	exact fun h => h1.choose_spec h.1
	uniq := fun c f H => by
	dsimp -- Porting note: added a `dsimp`
	rw [← Category.id_comp f, ← H, ← Category.assoc]
	congr 1; apply terminalIsTerminal.hom_ext }
	#align skyscraper_presheaf_cocone_is_colimit_of_not_specializes skyscraperPresheafCoconeIsColimitOfNotSpecializes