chore: missing simps lemmas for Multiplicative defs (#7016)

This also fixes the definitions to not include any defeq abuse, which is required in order to not produce a bad simp lemma.
leanprover-community · Sep 8, 2023 · bce8378 · bce8378
1 parent db154ca
commit bce8378
Showing 1 changed file with 53 additions and 14 deletions.
diff --git a/Mathlib/Algebra/Hom/Equiv/TypeTags.lean b/Mathlib/Algebra/Hom/Equiv/TypeTags.lean
@@ -16,56 +16,93 @@ import Mathlib.Algebra.Group.TypeTags
 variable {G H : Type*}
 
 /-- Reinterpret `G ≃+ H` as `Multiplicative G ≃* Multiplicative H`. -/
+@[simps]
 def AddEquiv.toMultiplicative [AddZeroClass G] [AddZeroClass H] :
     G ≃+ H ≃ (Multiplicative G ≃* Multiplicative H) where
   toFun f :=
-    ⟨⟨AddMonoidHom.toMultiplicative f.toAddMonoidHom,
-     AddMonoidHom.toMultiplicative f.symm.toAddMonoidHom, f.1.3, f.1.4⟩, f.2⟩
-  invFun f := ⟨⟨f.toMonoidHom, f.symm.toMonoidHom, f.1.3, f.1.4⟩, f.2⟩
+  { toFun := AddMonoidHom.toMultiplicative f.toAddMonoidHom
+    invFun := AddMonoidHom.toMultiplicative f.symm.toAddMonoidHom
+    left_inv := f.left_inv
+    right_inv := f.right_inv
+    map_mul' := f.map_add }
+  invFun f :=
+  { toFun := AddMonoidHom.toMultiplicative.symm f.toMonoidHom
+    invFun := AddMonoidHom.toMultiplicative.symm f.symm.toMonoidHom
+    left_inv := f.left_inv
+    right_inv := f.right_inv
+    map_add' := f.map_mul }
   left_inv x := by ext; rfl
   right_inv x := by ext; rfl
 #align add_equiv.to_multiplicative AddEquiv.toMultiplicative
 
 /-- Reinterpret `G ≃* H` as `Additive G ≃+ Additive H`. -/
+@[simps]
 def MulEquiv.toAdditive [MulOneClass G] [MulOneClass H] :
     G ≃* H ≃ (Additive G ≃+ Additive H) where
-  toFun f := ⟨⟨MonoidHom.toAdditive f.toMonoidHom,
-              MonoidHom.toAdditive f.symm.toMonoidHom, f.1.3, f.1.4⟩, f.2⟩
-  invFun f := ⟨⟨f.toAddMonoidHom, f.symm.toAddMonoidHom, f.1.3, f.1.4⟩, f.2⟩
+  toFun f :=
+  { toFun := MonoidHom.toAdditive f.toMonoidHom
+    invFun := MonoidHom.toAdditive f.symm.toMonoidHom
+    left_inv := f.left_inv
+    right_inv := f.right_inv
+    map_add' := f.map_mul }
+  invFun f :=
+  { toFun := MonoidHom.toAdditive.symm f.toAddMonoidHom
+    invFun := MonoidHom.toAdditive.symm f.symm.toAddMonoidHom
+    left_inv := f.left_inv
+    right_inv := f.right_inv
+    map_mul' := f.map_add }
   left_inv x := by ext; rfl
   right_inv x := by ext; rfl
 #align mul_equiv.to_additive MulEquiv.toAdditive
 
 /-- Reinterpret `Additive G ≃+ H` as `G ≃* Multiplicative H`. -/
+@[simps]
 def AddEquiv.toMultiplicative' [MulOneClass G] [AddZeroClass H] :
     Additive G ≃+ H ≃ (G ≃* Multiplicative H) where
   toFun f :=
-    ⟨⟨AddMonoidHom.toMultiplicative' f.toAddMonoidHom,
-     AddMonoidHom.toMultiplicative'' f.symm.toAddMonoidHom, f.1.3, f.1.4⟩, f.2⟩
-  invFun f := ⟨⟨f.toMonoidHom, f.symm.toMonoidHom, f.1.3, f.1.4⟩, f.2⟩
+  { toFun := AddMonoidHom.toMultiplicative' f.toAddMonoidHom
+    invFun := AddMonoidHom.toMultiplicative'' f.symm.toAddMonoidHom
+    left_inv := f.left_inv
+    right_inv := f.right_inv
+    map_mul' := f.map_add }
+  invFun f :=
+  { toFun := AddMonoidHom.toMultiplicative'.symm f.toMonoidHom
+    invFun := AddMonoidHom.toMultiplicative''.symm f.symm.toMonoidHom
+    left_inv := f.left_inv
+    right_inv := f.right_inv
+    map_add' := f.map_mul }
   left_inv x := by ext; rfl
   right_inv x := by ext; rfl
 #align add_equiv.to_multiplicative' AddEquiv.toMultiplicative'
 
 /-- Reinterpret `G ≃* Multiplicative H` as `Additive G ≃+ H` as. -/
-def MulEquiv.toAdditive' [MulOneClass G] [AddZeroClass H] :
+abbrev MulEquiv.toAdditive' [MulOneClass G] [AddZeroClass H] :
     G ≃* Multiplicative H ≃ (Additive G ≃+ H) :=
   AddEquiv.toMultiplicative'.symm
 #align mul_equiv.to_additive' MulEquiv.toAdditive'
 
 /-- Reinterpret `G ≃+ Additive H` as `Multiplicative G ≃* H`. -/
+@[simps]
 def AddEquiv.toMultiplicative'' [AddZeroClass G] [MulOneClass H] :
     G ≃+ Additive H ≃ (Multiplicative G ≃* H) where
   toFun f :=
-    ⟨⟨AddMonoidHom.toMultiplicative'' f.toAddMonoidHom,
-     AddMonoidHom.toMultiplicative' f.symm.toAddMonoidHom, f.1.3, f.1.4⟩, f.2⟩
-  invFun f := ⟨⟨f.toMonoidHom, f.symm.toMonoidHom, f.1.3, f.1.4⟩, f.2⟩
+  { toFun := AddMonoidHom.toMultiplicative'' f.toAddMonoidHom
+    invFun := AddMonoidHom.toMultiplicative' f.symm.toAddMonoidHom
+    left_inv := f.left_inv
+    right_inv := f.right_inv
+    map_mul' := f.map_add }
+  invFun f :=
+  { toFun := AddMonoidHom.toMultiplicative''.symm f.toMonoidHom
+    invFun := AddMonoidHom.toMultiplicative'.symm f.symm.toMonoidHom
+    left_inv := f.left_inv
+    right_inv := f.right_inv
+    map_add' := f.map_mul }
   left_inv x := by ext; rfl
   right_inv x := by ext; rfl
 #align add_equiv.to_multiplicative'' AddEquiv.toMultiplicative''
 
 /-- Reinterpret `Multiplicative G ≃* H` as `G ≃+ Additive H` as. -/
-def MulEquiv.toAdditive'' [AddZeroClass G] [MulOneClass H] :
+abbrev MulEquiv.toAdditive'' [AddZeroClass G] [MulOneClass H] :
     Multiplicative G ≃* H ≃ (G ≃+ Additive H) :=
   AddEquiv.toMultiplicative''.symm
 #align mul_equiv.to_additive'' MulEquiv.toAdditive''
@@ -75,11 +112,13 @@ section
 variable (G) (H)
 
 /-- `Additive (Multiplicative G)` is just `G`. -/
+@[simps!]
 def AddEquiv.additiveMultiplicative [AddZeroClass G] : Additive (Multiplicative G) ≃+ G :=
   MulEquiv.toAdditive' (MulEquiv.refl (Multiplicative G))
 #align add_equiv.additive_multiplicative AddEquiv.additiveMultiplicative
 
 /-- `Multiplicative (Additive H)` is just `H`. -/
+@[simps!]
 def MulEquiv.multiplicativeAdditive [MulOneClass H] : Multiplicative (Additive H) ≃* H :=
   AddEquiv.toMultiplicative'' (AddEquiv.refl (Additive H))
 #align mul_equiv.multiplicative_additive MulEquiv.multiplicativeAdditive