Porting note: used to be `dsimp`

[pitmonticone]

Classifies porting notes claiming anything semantically equivalent to:

• "used to be dsimp"
• "was dsimp"

Examples

mathlib4/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

Lines 89 to 106 in 6af752e

	theorem μ_natural {X Y X' Y' : Type u} (f : X ⟶ Y) (g : X' ⟶ Y') :
	((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom = (μ R X X').hom ≫ (free R).map (f ⊗ g) := by
	intros
	-- Porting note: broken ext
	apply TensorProduct.ext
	apply Finsupp.lhom_ext'
	intro x
	apply LinearMap.ext_ring
	apply Finsupp.lhom_ext'
	intro x'
	apply LinearMap.ext_ring
	apply Finsupp.ext
	intro ⟨y, y'⟩
	-- Porting note: used to be dsimp [μ]
	change (finsuppTensorFinsupp' R Y Y')
	(Finsupp.mapDomain f (Finsupp.single x 1) ⊗ₜ[R] Finsupp.mapDomain g (Finsupp.single x' 1)) _
	= (Finsupp.mapDomain (f ⊗ g) (finsuppTensorFinsupp' R X X'
	(Finsupp.single x 1 ⊗ₜ[R] Finsupp.single x' 1))) _

mathlib4/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

Lines 179 to 191 in 6af752e

	theorem rightUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
	tensorHom f (𝟙 (ModuleCat.of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f := by
	-- Porting note: broken ext
	apply TensorProduct.ext
	apply LinearMap.ext; intro x
	apply LinearMap.ext_ring
	-- Porting note: used to be dsimp
	change ((rightUnitor N).hom) ((tensorHom f (𝟙 (of R R))) (x ⊗ₜ[R] (1 : R))) =
	f (((rightUnitor M).hom) (x ⊗ₜ[R] 1))
	erw [TensorProduct.rid_tmul, TensorProduct.rid_tmul]
	rw [LinearMap.map_smul]
	rfl
	#align Module.monoidal_category.right_unitor_naturality ModuleCat.MonoidalCategory.rightUnitor_naturality