Porting note: `@[simp]` removed

[pitmonticone]

Classifies porting notes claiming anything semantically equivalent to:

• "@[simp] removed [...]"
• "@[simp] removed [...]"
• "removed simp attribute"

Related to: #10618

Examples

mathlib4/Mathlib/Order/WellFounded.lean

Lines 230 to 234 in e6232b7

	--Porting note: @[simp] removed as it will never apply
	theorem argminOn_le (s : Set α) {a : α} (ha : a ∈ s) (hs : s.Nonempty := Set.nonempty_of_mem ha) :
	f (argminOn f h s hs) ≤ f a :=
	not_lt.mp <| not_lt_argminOn f h s ha hs
	#align function.argmin_on_le Function.argminOn_le

mathlib4/Mathlib/Data/Prod/Basic.lean

Lines 100 to 104 in e6232b7

	-- Porting note: `@[simp]` tag removed because auto-generated `mk.injEq` simplifies LHS
	-- @[simp]
	theorem mk.inj_iff {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ :=
	Iff.of_eq (mk.injEq _ _ _ _)
	#align prod.mk.inj_iff Prod.mk.inj_iff

mathlib4/Mathlib/Data/Multiset/Bind.lean

Lines 222 to 226 in e6232b7

	-- Porting note: @[simp] removed because not in normal form
	theorem attach_bind_coe (s : Multiset α) (f : α → Multiset β) :
	(s.attach.bind fun i => f i) = s.bind f :=
	congr_arg join <| attach_map_val' _ _
	#align multiset.attach_bind_coe Multiset.attach_bind_coe