Porting note: dsimp can prove this

[pitmonticone]

Classifies porting notes claiming dsimp can prove this.

Examples

mathlib4/Mathlib/Computability/TuringMachine.lean

Lines 361 to 365 in 9a04ccc

	-- @[simp] -- Porting note: dsimp can prove this
	theorem PointedMap.mk_val {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : Γ → Γ') (pt) :
	(PointedMap.mk f pt : Γ → Γ') = f :=
	rfl
	#align turing.pointed_map.mk_val Turing.PointedMap.mk_val

mathlib4/Mathlib/Data/Nat/Digits.lean

Lines 113 to 116 in 9a04ccc

	-- @[simp] -- Porting note: dsimp can prove this
	theorem digits_one_succ (n : ℕ) : digits 1 (n + 1) = 1 :: digits 1 n :=
	rfl
	#align nat.digits_one_succ Nat.digits_one_succ

mathlib4/Mathlib/Order/JordanHolder.lean

Lines 160 to 164 in 9a04ccc

	-- @[simp] -- Porting note: dsimp can prove this
	theorem coeFn_mk (length : ℕ) (series step) :
	(@CompositionSeries.mk X _ _ length series step : Fin length.succ → X) = series :=
	rfl
	#align composition_series.coe_fn_mk CompositionSeries.coeFn_mk