Commit 2025-07-11 14:29 d55d8271

fix(Order): fix simp lemma for with{Top/Bot}{Map/Congr} (#26787) This change includes the following in generated simp lemmas:

-@[simp] theorem OrderEmbedding.withBotMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : 
-  ⇑f.withBotMap = Option.map ⇑f
+@[simp] theorem OrderEmbedding.withBotMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) :
+  ⇑f.withBotMap = WithBot.map ⇑f
@[simp] theorem OrderEmbedding.withTopMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) :
  ⇑f.withTopMap = WithTop.map ⇑f -- unchanged
-@[simp] theorem OrderIso.withBotCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) (a✝ : Option α) : 
-  e.withBotCongr a✝ = Option.map (⇑e) a✝
+@[simp] theorem OrderIso.withBotCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
+  ⇑e.withBotCongr = WithBot.map ⇑e
-@[simp] theorem OrderIso.withTopCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) (a✝ : Option α) : 
-  e.withTopCongr a✝ = Option.map (⇑e) a✝
+@[simp] theorem OrderIso.withTopCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
+  ⇑e.withTopCongr = WithTop.map ⇑e