Porting note: `dsimp` cannot prove this

[pitmonticone]

-- In Lean 3, `dsimp` would use theorems proved by `Iff.rfl`. 
-- If that were still the case, this would useful as a `@[simp]` lemma,
-- despite the fact that it is provable by `simp` (by not `dsimp`).

Examples

mathlib4/Mathlib/Algebra/Free.lean

Lines 168 to 171 in 5e53cc1

	-- Porting note: dsimp can not prove this
	@[to_additive (attr := simp, nolint simpNF)]
	theorem map_pure (f : α → β) (x) : (f <$> pure x : FreeMagma β) = pure (f x) := rfl
	#align free_magma.map_pure FreeMagma.map_pure

mathlib4/Mathlib/Algebra/Free.lean

Lines 177 to 180 in 5e53cc1

	-- Porting note: dsimp can not prove this
	@[to_additive (attr := simp, nolint simpNF)]
	theorem pure_bind (f : α → FreeMagma β) (x) : pure x >>= f = f x := rfl
	#align free_magma.pure_bind FreeMagma.pure_bind

mathlib4/Mathlib/Data/Multiset/FinsetOps.lean

Lines 39 to 42 in 5e53cc1

	@[simp, nolint simpNF] -- Porting note: dsimp can not prove this
	theorem ndinsert_zero (a : α) : ndinsert a 0 = {a} :=
	rfl
	#align multiset.ndinsert_zero Multiset.ndinsert_zero

mathlib4/Mathlib/GroupTheory/Subgroup/Basic.lean

Lines 418 to 422 in 5e53cc1

	@[to_additive (attr := simp, nolint simpNF)] -- Porting note: dsimp can not prove this
	theorem mem_carrier {s : Subgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s :=
	Iff.rfl
	#align subgroup.mem_carrier Subgroup.mem_carrier
	#align add_subgroup.mem_carrier AddSubgroup.mem_carrier

[eric-wieser]

leanprover/lean4#3973 would likely resolve this.

[eric-wieser]

And for more context, leanprover-community/lean#723 and leanprover-community/lean#736 implemented this in Lean 3.