Classifies porting notes claiming anything semantically equivalent to:
- "
@[simp] removed [...]"
- "@[simp] removed [...]"
- "removed
simp attribute"
Related to: #10618
Examples
|
--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 |
|
-- 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 |
|
-- 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 |
Classifies porting notes claiming anything semantically equivalent to:
@[simp]removed [...]"simpattribute"Related to: #10618
Examples
mathlib4/Mathlib/Order/WellFounded.lean
Lines 230 to 234 in e6232b7
mathlib4/Mathlib/Data/Prod/Basic.lean
Lines 100 to 104 in e6232b7
mathlib4/Mathlib/Data/Multiset/Bind.lean
Lines 222 to 226 in e6232b7