Porting note: `simp` cannot prove this

[pitmonticone]

Classifies porting notes claiming anything semantically equivalent to:

• "simp cannot prove this"
• "simp used to be able to close this goal"
• "simp can't handle this"
• "simp used to work here"

Examples

mathlib4/Mathlib/SetTheory/Ordinal/Arithmetic.lean

Lines 1158 to 1167 in ddd23d7

	@[simp, nolint simpNF] -- Porting note: simp cannot prove this
	theorem familyOfBFamily_enum (o : Ordinal) (f : ∀ a < o, α) (i hi) :
	familyOfBFamily o f
	(enum (· < ·) i
	(by
	convert hi
	exact type_lt _)) =
	f i hi :=
	familyOfBFamily'_enum _ (type_lt o) f _ _
	#align ordinal.family_of_bfamily_enum Ordinal.familyOfBFamily_enum

mathlib4/Mathlib/Analysis/Quaternion.lean

Lines 88 to 91 in ddd23d7

	@[simp, nolint simpNF] -- Porting note: simp cannot prove this
	theorem nnnorm_star (a : ℍ) : ‖star a‖₊ = ‖a‖₊ :=
	Subtype.ext <| norm_star a
	#align quaternion.nnnorm_star Quaternion.nnnorm_star

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

Lines 337 to 373 in ddd23d7

	@[simps]
	def lift (F : C ⥤ D) : Free R C ⥤ D where
	obj X := F.obj X
	map {X Y} f := f.sum fun f' r => r • F.map f'
	map_id := by dsimp [CategoryTheory.categoryFree]; simp
	map_comp {X Y Z} f g := by
	apply Finsupp.induction_linear f
	· -- Porting note: simp used to be able to close this goal
	dsimp
	rw [Limits.zero_comp, sum_zero_index, Limits.zero_comp]
	· intro f₁ f₂ w₁ w₂
	rw [add_comp]
	dsimp at *
	rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
	· simp only [w₁, w₂, add_comp]
	· intros; rw [zero_smul]
	· intros; simp only [add_smul]
	· intros; rw [zero_smul]
	· intros; simp only [add_smul]
	· intro f' r
	apply Finsupp.induction_linear g
	· -- Porting note: simp used to be able to close this goal
	dsimp
	rw [Limits.comp_zero, sum_zero_index, Limits.comp_zero]
	· intro f₁ f₂ w₁ w₂
	rw [comp_add]
	dsimp at *
	rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
	· simp only [w₁, w₂, comp_add]
	· intros; rw [zero_smul]
	· intros; simp only [add_smul]
	· intros; rw [zero_smul]
	· intros; simp only [add_smul]
	· intro g' s
	rw [single_comp_single _ _ f' g' r s]
	simp [mul_comm r s, mul_smul]
	#align category_theory.Free.lift CategoryTheory.Free.lift