feat(Algebra/Order/Monoid/Unbundled/WithTop): AddEquiv between WithBot (#34756)

It is like `Equiv.withBotCongr` but preserving also addition (`AddEquiv`), for a variant of degree of `MvPolynomial` that maps `0` to `⊥` submitted in #34759.

Author: Hagb

Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.CharZero.Defs
 public import Mathlib.Algebra.Group.Hom.Defs
+public import Mathlib.Algebra.Group.Equiv.Defs
 public import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 public import Mathlib.Algebra.Order.ZeroLEOne
 public import Mathlib.Order.WithBot
@@ -708,3 +709,37 @@ protected def _root_.AddMonoidHom.withBotMap {M N : Type*} [AddZeroClass M] [Add
   { ZeroHom.withBotMap f.toZeroHom, AddHom.withBotMap f.toAddHom with toFun := WithBot.map f }
 
 end WithBot
+
+namespace AddEquiv
+
+variable {γ : Type*} [Add α] [Add β] [Add γ] (e e₁ : α ≃+ β) (e₂ : β ≃+ γ)
+
+/-- A `AddEquiv` version of `Equiv.withBotCongr`. -/
+@[to_dual (attr := simps!) /-- A `AddEquiv` version of `Equiv.withTopCongr`. -/]
+def withBotCongr : WithBot α ≃+ WithBot β where
+  __ := e.toEquiv.withBotCongr
+  map_add' := e.toAddHom.withBotMap.map_add'
+
+@[to_dual (attr := simp)]
+lemma coe_withBotCongr : e.withBotCongr = WithBot.map e := rfl
+
+@[to_dual (attr := simp)]
+lemma withBotCongr_toEquiv : e.withBotCongr = (e : α ≃ β).withBotCongr := rfl
+
+@[to_dual (attr := simp)]
+lemma withBotCongr_toAddHom : e.withBotCongr = (e : AddHom α β).withBotMap := rfl
+
+@[to_dual (attr := simp)]
+lemma withBotCongr_refl : (AddEquiv.refl α).withBotCongr = AddEquiv.refl _ :=
+  AddEquiv.ext <| congr_fun WithBot.map_id
+
+@[to_dual (attr := simp)]
+theorem withBotCongr_symm : e.withBotCongr.symm = e.symm.withBotCongr := rfl
+
+@[to_dual (attr := simp)]
+theorem withBotCongr_trans :
+    (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr := by
+  ext x
+  simp
+
+end AddEquiv