/-
Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
Ported by: Frédéric Dupuis

! This file was ported from Lean 3 source module algebra.hom.equiv.type_tags
! leanprover-community/mathlib commit 3342d1b2178381196f818146ff79bc0e7ccd9e2d
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.Equiv.Basic
import Mathlib.Algebra.Group.TypeTags

/-!
# Additive and multiplicative equivalences associated to `Multiplicative` and `Additive`.
-/


variable {
G: Type ?u.7531
G 
H: Type ?u.11
H : 
Type _: Type (?u.5+1)
Type _}

/-- Reinterpret `G ≃+ H` as `Multiplicative G ≃* Multiplicative H`. -/
def 
AddEquiv.toMultiplicative: [inst : AddZeroClass G] → [inst_1 : AddZeroClass H] → G ≃+ H ≃ (Multiplicative G ≃* Multiplicative H)
AddEquiv.toMultiplicative [
AddZeroClass: Type ?u.14 → Type ?u.14
AddZeroClass 
G: Type ?u.8
G] [
AddZeroClass: Type ?u.17 → Type ?u.17
AddZeroClass 
H: Type ?u.11
H] :
    
G: Type ?u.8
G ≃+ 
H: Type ?u.11
H ≃ (
Multiplicative: Type ?u.50 → Type ?u.50
Multiplicative 
G: Type ?u.8
G ≃* 
Multiplicative: Type ?u.51 → Type ?u.51
Multiplicative 
H: Type ?u.11
H) where
  toFun 
f: ?m.94
f :=
    ⟨⟨
AddMonoidHom.toMultiplicative: {α : Type ?u.153} →
  {β : Type ?u.152} →
    [inst : AddZeroClass α] → [inst_1 : AddZeroClass β] → (α →+ β) ≃ (Multiplicative α →* Multiplicative β)
AddMonoidHom.toMultiplicative 
f: ?m.94
f.
toAddMonoidHom: {M : Type ?u.246} → {N : Type ?u.245} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M ≃+ N → M →+ N
toAddMonoidHom,
     
AddMonoidHom.toMultiplicative: {α : Type ?u.519} →
  {β : Type ?u.518} →
    [inst : AddZeroClass α] → [inst_1 : AddZeroClass β] → (α →+ β) ≃ (Multiplicative α →* Multiplicative β)
AddMonoidHom.toMultiplicative 
f: ?m.94
f.
symm: {M : Type ?u.612} → {N : Type ?u.611} → [inst : Add M] → [inst_1 : Add N] → M ≃+ N → N ≃+ M
symm.
toAddMonoidHom: {M : Type ?u.630} → {N : Type ?u.629} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M ≃+ N → M →+ N
toAddMonoidHom, 
f: ?m.94
f.
1: {A : Type ?u.897} → {B : Type ?u.896} → [inst : Add A] → [inst_1 : Add B] → A ≃+ B → A ≃ B
1.
3: ∀ {α : Sort ?u.903} {β : Sort ?u.902} (self : α ≃ β), Function.LeftInverse self.invFun self.toFun
3, 
f: ?m.94
f.
1: {A : Type ?u.922} → {B : Type ?u.921} → [inst : Add A] → [inst_1 : Add B] → A ≃+ B → A ≃ B
1.
4: ∀ {α : Sort ?u.928} {β : Sort ?u.927} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
4⟩, 
f: ?m.94
f.
2: ∀ {A : Type ?u.945} {B : Type ?u.944} [inst : Add A] [inst_1 : Add B] (self : A ≃+ B) (x y : A),
  Equiv.toFun self.toEquiv (x + y) = Equiv.toFun self.toEquiv x + Equiv.toFun self.toEquiv y
2⟩
  invFun 
f: ?m.990
f := ⟨⟨
f: ?m.990
f.
toMonoidHom: {M : Type ?u.1037} → {N : Type ?u.1036} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* N
toMonoidHom, 
f: ?m.990
f.
symm: {M : Type ?u.1281} → {N : Type ?u.1280} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N ≃* M
symm.
toMonoidHom: {M : Type ?u.1287} → {N : Type ?u.1286} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* N
toMonoidHom, 
f: ?m.990
f.
1: {M : Type ?u.1511} → {N : Type ?u.1510} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → M ≃ N
1.
3: ∀ {α : Sort ?u.1517} {β : Sort ?u.1516} (self : α ≃ β), Function.LeftInverse self.invFun self.toFun
3, 
f: ?m.990
f.
1: {M : Type ?u.1522} → {N : Type ?u.1521} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → M ≃ N
1.
4: ∀ {α : Sort ?u.1528} {β : Sort ?u.1527} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
4⟩, 
f: ?m.990
f.
2: ∀ {M : Type ?u.1533} {N : Type ?u.1532} [inst : Mul M] [inst_1 : Mul N] (self : M ≃* N) (x y : M),
  Equiv.toFun self.toEquiv (x * y) = Equiv.toFun self.toEquiv x * Equiv.toFun self.toEquiv y
2⟩
  left_inv 
x: ?m.1549
x := by
Goals accomplished! 🐙 
G: Type ?u.8

H: Type ?u.11

inst✝¹: AddZeroClass G

inst✝: AddZeroClass H

x: G ≃+ H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_add' :=
          (_ :
            ∀ (x y : Multiplicative G),
              Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
              invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      x) =   xext
G: Type ?u.8

H: Type ?u.11

inst✝¹: AddZeroClass G

inst✝: AddZeroClass H

x: G ≃+ H

x✝: G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ :
                ∀ (x y : Multiplicative G),
                  Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
                  invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝;
G: Type ?u.8

H: Type ?u.11

inst✝¹: AddZeroClass G

inst✝: AddZeroClass H

x: G ≃+ H

x✝: G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ :
                ∀ (x y : Multiplicative G),
                  Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
                  invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝ 
G: Type ?u.8

H: Type ?u.11

inst✝¹: AddZeroClass G

inst✝: AddZeroClass H

x: G ≃+ H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_add' :=
          (_ :
            ∀ (x y : Multiplicative G),
              Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
              invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      x) =   xrfl
Goals accomplished! 🐙
  right_inv 
x: ?m.1555
x := by
Goals accomplished! 🐙 
G: Type ?u.8

H: Type ?u.11

inst✝¹: AddZeroClass G

inst✝: AddZeroClass H

x: Multiplicative G ≃* Multiplicative H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
            invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_mul' :=
          (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ :
              ∀ (x y : Multiplicative G),
                Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      x) =   xext
G: Type ?u.8

H: Type ?u.11

inst✝¹: AddZeroClass G

inst✝: AddZeroClass H

x: Multiplicative G ≃* Multiplicative H

x✝: Multiplicative G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
                invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ :
                  ∀ (x y : Multiplicative G),
                    Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝;
G: Type ?u.8

H: Type ?u.11

inst✝¹: AddZeroClass G

inst✝: AddZeroClass H

x: Multiplicative G ≃* Multiplicative H

x✝: Multiplicative G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
                invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ :
                  ∀ (x y : Multiplicative G),
                    Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝ 
G: Type ?u.8

H: Type ?u.11

inst✝¹: AddZeroClass G

inst✝: AddZeroClass H

x: Multiplicative G ≃* Multiplicative H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
            invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_mul' :=
          (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ :
              ∀ (x y : Multiplicative G),
                Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      x) =   xrfl
Goals accomplished! 🐙
#align add_equiv.to_multiplicative 
AddEquiv.toMultiplicative: {G : Type u_1} →
  {H : Type u_2} → [inst : AddZeroClass G] → [inst_1 : AddZeroClass H] → G ≃+ H ≃ (Multiplicative G ≃* Multiplicative H)
AddEquiv.toMultiplicative

/-- Reinterpret `G ≃* H` as `Additive G ≃+ Additive H`. -/
def 
MulEquiv.toAdditive: {G : Type u_1} →
  {H : Type u_2} → [inst : MulOneClass G] → [inst_1 : MulOneClass H] → G ≃* H ≃ (Additive G ≃+ Additive H)
MulEquiv.toAdditive [
MulOneClass: Type ?u.1978 → Type ?u.1978
MulOneClass 
G: Type ?u.1972
G] [
MulOneClass: Type ?u.1981 → Type ?u.1981
MulOneClass 
H: Type ?u.1975
H] :
    
G: Type ?u.1972
G ≃* 
H: Type ?u.1975
H ≃ (
Additive: Type ?u.2116 → Type ?u.2116
Additive 
G: Type ?u.1972
G ≃+ 
Additive: Type ?u.2117 → Type ?u.2117
Additive 
H: Type ?u.1975
H) where
  toFun 
f: ?m.2232
f := ⟨⟨
MonoidHom.toAdditive: {α : Type ?u.2285} →
  {β : Type ?u.2284} → [inst : MulOneClass α] → [inst_1 : MulOneClass β] → (α →* β) ≃ (Additive α →+ Additive β)
MonoidHom.toAdditive 
f: ?m.2232
f.
toMonoidHom: {M : Type ?u.2380} → {N : Type ?u.2379} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* N
toMonoidHom,
              
MonoidHom.toAdditive: {α : Type ?u.2908} →
  {β : Type ?u.2907} → [inst : MulOneClass α] → [inst_1 : MulOneClass β] → (α →* β) ≃ (Additive α →+ Additive β)
MonoidHom.toAdditive 
f: ?m.2232
f.
symm: {M : Type ?u.3003} → {N : Type ?u.3002} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N ≃* M
symm.
toMonoidHom: {M : Type ?u.3095} → {N : Type ?u.3094} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* N
toMonoidHom, 
f: ?m.2232
f.
1: {M : Type ?u.3615} → {N : Type ?u.3614} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → M ≃ N
1.
3: ∀ {α : Sort ?u.3621} {β : Sort ?u.3620} (self : α ≃ β), Function.LeftInverse self.invFun self.toFun
3, 
f: ?m.2232
f.
1: {M : Type ?u.3640} → {N : Type ?u.3639} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → M ≃ N
1.
4: ∀ {α : Sort ?u.3646} {β : Sort ?u.3645} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
4⟩, 
f: ?m.2232
f.
2: ∀ {M : Type ?u.3663} {N : Type ?u.3662} [inst : Mul M] [inst_1 : Mul N] (self : M ≃* N) (x y : M),
  Equiv.toFun self.toEquiv (x * y) = Equiv.toFun self.toEquiv x * Equiv.toFun self.toEquiv y
2⟩
  invFun 
f: ?m.3780
f := ⟨⟨
f: ?m.3780
f.
toAddMonoidHom: {M : Type ?u.3833} → {N : Type ?u.3832} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M ≃+ N → M →+ N
toAddMonoidHom, 
f: ?m.3780
f.
symm: {M : Type ?u.4322} → {N : Type ?u.4321} → [inst : Add M] → [inst_1 : Add N] → M ≃+ N → N ≃+ M
symm.
toAddMonoidHom: {M : Type ?u.4328} → {N : Type ?u.4327} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M ≃+ N → M →+ N
toAddMonoidHom, 
f: ?m.3780
f.
1: {A : Type ?u.4797} → {B : Type ?u.4796} → [inst : Add A] → [inst_1 : Add B] → A ≃+ B → A ≃ B
1.
3: ∀ {α : Sort ?u.4803} {β : Sort ?u.4802} (self : α ≃ β), Function.LeftInverse self.invFun self.toFun
3, 
f: ?m.3780
f.
1: {A : Type ?u.4808} → {B : Type ?u.4807} → [inst : Add A] → [inst_1 : Add B] → A ≃+ B → A ≃ B
1.
4: ∀ {α : Sort ?u.4814} {β : Sort ?u.4813} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
4⟩, 
f: ?m.3780
f.
2: ∀ {A : Type ?u.4819} {B : Type ?u.4818} [inst : Add A] [inst_1 : Add B] (self : A ≃+ B) (x y : A),
  Equiv.toFun self.toEquiv (x + y) = Equiv.toFun self.toEquiv x + Equiv.toFun self.toEquiv y
2⟩
  left_inv 
x: ?m.4835
x := by
Goals accomplished! 🐙 
G: Type ?u.1972

H: Type ?u.1975

inst✝¹: MulOneClass G

inst✝: MulOneClass H

x: G ≃* H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_mul' :=
          (_ :
            ∀ (x y : Additive G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
              invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      x) =   xext
G: Type ?u.1972

H: Type ?u.1975

inst✝¹: MulOneClass G

inst✝: MulOneClass H

x: G ≃* H

x✝: G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ :
                ∀ (x y : Additive G),
                  Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
                  invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝;
G: Type ?u.1972

H: Type ?u.1975

inst✝¹: MulOneClass G

inst✝: MulOneClass H

x: G ≃* H

x✝: G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ :
                ∀ (x y : Additive G),
                  Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
                  invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝ 
G: Type ?u.1972

H: Type ?u.1975

inst✝¹: MulOneClass G

inst✝: MulOneClass H

x: G ≃* H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_mul' :=
          (_ :
            ∀ (x y : Additive G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
              invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      x) =   xrfl
Goals accomplished! 🐙
  right_inv 
x: ?m.4841
x := by
Goals accomplished! 🐙 
G: Type ?u.1972

H: Type ?u.1975

inst✝¹: MulOneClass G

inst✝: MulOneClass H

x: Additive G ≃+ Additive H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
            invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_add' :=
          (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ :
              ∀ (x y : Additive G),
                Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      x) =   xext
G: Type ?u.1972

H: Type ?u.1975

inst✝¹: MulOneClass G

inst✝: MulOneClass H

x: Additive G ≃+ Additive H

x✝: Additive G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
                invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ :
                  ∀ (x y : Additive G),
                    Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝;
G: Type ?u.1972

H: Type ?u.1975

inst✝¹: MulOneClass G

inst✝: MulOneClass H

x: Additive G ≃+ Additive H

x✝: Additive G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
                invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ :
                  ∀ (x y : Additive G),
                    Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝ 
G: Type ?u.1972

H: Type ?u.1975

inst✝¹: MulOneClass G

inst✝: MulOneClass H

x: Additive G ≃+ Additive H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
            invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_add' :=
          (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ :
              ∀ (x y : Additive G),
                Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      x) =   xrfl
Goals accomplished! 🐙
#align mul_equiv.to_additive 
MulEquiv.toAdditive: {G : Type u_1} →
  {H : Type u_2} → [inst : MulOneClass G] → [inst_1 : MulOneClass H] → G ≃* H ≃ (Additive G ≃+ Additive H)
MulEquiv.toAdditive

/-- Reinterpret `Additive G ≃+ H` as `G ≃* Multiplicative H`. -/
def 
AddEquiv.toMultiplicative': [inst : MulOneClass G] → [inst_1 : AddZeroClass H] → Additive G ≃+ H ≃ (G ≃* Multiplicative H)
AddEquiv.toMultiplicative' [
MulOneClass: Type ?u.5253 → Type ?u.5253
MulOneClass 
G: Type ?u.5247
G] [
AddZeroClass: Type ?u.5256 → Type ?u.5256
AddZeroClass 
H: Type ?u.5250
H] :
    
Additive: Type ?u.5263 → Type ?u.5263
Additive 
G: Type ?u.5247
G ≃+ 
H: Type ?u.5250
H ≃ (
G: Type ?u.5247
G ≃* 
Multiplicative: Type ?u.5349 → Type ?u.5349
Multiplicative 
H: Type ?u.5250
H) where
  toFun 
f: ?m.5420
f :=
    ⟨⟨
AddMonoidHom.toMultiplicative': {α : Type ?u.5479} →
  {β : Type ?u.5478} → [inst : MulOneClass α] → [inst_1 : AddZeroClass β] → (Additive α →+ β) ≃ (α →* Multiplicative β)
AddMonoidHom.toMultiplicative' 
f: ?m.5420
f.
toAddMonoidHom: {M : Type ?u.5573} → {N : Type ?u.5572} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M ≃+ N → M →+ N
toAddMonoidHom,
     
AddMonoidHom.toMultiplicative'': {α : Type ?u.5865} →
  {β : Type ?u.5864} → [inst : AddZeroClass α] → [inst_1 : MulOneClass β] → (α →+ Additive β) ≃ (Multiplicative α →* β)
AddMonoidHom.toMultiplicative'' 
f: ?m.5420
f.
symm: {M : Type ?u.5959} → {N : Type ?u.5958} → [inst : Add M] → [inst_1 : Add N] → M ≃+ N → N ≃+ M
symm.
toAddMonoidHom: {M : Type ?u.6019} → {N : Type ?u.6018} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M ≃+ N → M →+ N
toAddMonoidHom, 
f: ?m.5420
f.
1: {A : Type ?u.6287} → {B : Type ?u.6286} → [inst : Add A] → [inst_1 : Add B] → A ≃+ B → A ≃ B
1.
3: ∀ {α : Sort ?u.6293} {β : Sort ?u.6292} (self : α ≃ β), Function.LeftInverse self.invFun self.toFun
3, 
f: ?m.5420
f.
1: {A : Type ?u.6312} → {B : Type ?u.6311} → [inst : Add A] → [inst_1 : Add B] → A ≃+ B → A ≃ B
1.
4: ∀ {α : Sort ?u.6318} {β : Sort ?u.6317} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
4⟩, 
f: ?m.5420
f.
2: ∀ {A : Type ?u.6335} {B : Type ?u.6334} [inst : Add A] [inst_1 : Add B] (self : A ≃+ B) (x y : A),
  Equiv.toFun self.toEquiv (x + y) = Equiv.toFun self.toEquiv x + Equiv.toFun self.toEquiv y
2⟩
  invFun 
f: ?m.6412
f := ⟨⟨
f: ?m.6412
f.
toMonoidHom: {M : Type ?u.6459} → {N : Type ?u.6458} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* N
toMonoidHom, 
f: ?m.6412
f.
symm: {M : Type ?u.6681} → {N : Type ?u.6680} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N ≃* M
symm.
toMonoidHom: {M : Type ?u.6687} → {N : Type ?u.6686} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* N
toMonoidHom, 
f: ?m.6412
f.
1: {M : Type ?u.6901} → {N : Type ?u.6900} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → M ≃ N
1.
3: ∀ {α : Sort ?u.6907} {β : Sort ?u.6906} (self : α ≃ β), Function.LeftInverse self.invFun self.toFun
3, 
f: ?m.6412
f.
1: {M : Type ?u.6912} → {N : Type ?u.6911} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → M ≃ N
1.
4: ∀ {α : Sort ?u.6918} {β : Sort ?u.6917} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
4⟩, 
f: ?m.6412
f.
2: ∀ {M : Type ?u.6923} {N : Type ?u.6922} [inst : Mul M] [inst_1 : Mul N] (self : M ≃* N) (x y : M),
  Equiv.toFun self.toEquiv (x * y) = Equiv.toFun self.toEquiv x * Equiv.toFun self.toEquiv y
2⟩
  left_inv 
x: ?m.6939
x := by
Goals accomplished! 🐙 
G: Type ?u.5247

H: Type ?u.5250

inst✝¹: MulOneClass G

inst✝: AddZeroClass H

x: Additive G ≃+ H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_add' :=
          (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
              invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ :
              ∀ (x y : Additive G),
                Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      x) =   xext
G: Type ?u.5247

H: Type ?u.5250

inst✝¹: MulOneClass G

inst✝: AddZeroClass H

x: Additive G ≃+ H

x✝: Additive G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
                  invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ :
                  ∀ (x y : Additive G),
                    Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝;
G: Type ?u.5247

H: Type ?u.5250

inst✝¹: MulOneClass G

inst✝: AddZeroClass H

x: Additive G ≃+ H

x✝: Additive G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
                  invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ :
                  ∀ (x y : Additive G),
                    Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝ 
G: Type ?u.5247

H: Type ?u.5250

inst✝¹: MulOneClass G

inst✝: AddZeroClass H

x: Additive G ≃+ H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_add' :=
          (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
              invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ :
              ∀ (x y : Additive G),
                Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      x) =   xrfl
Goals accomplished! 🐙
  right_inv 
x: ?m.6945
x := by
Goals accomplished! 🐙 
G: Type ?u.5247

H: Type ?u.5250

inst✝¹: MulOneClass G

inst✝: AddZeroClass H

x: G ≃* Multiplicative H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
            invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_mul' :=
          (_ :
            ∀ (x y : Additive G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      x) =   xext
G: Type ?u.5247

H: Type ?u.5250

inst✝¹: MulOneClass G

inst✝: AddZeroClass H

x: G ≃* Multiplicative H

x✝: G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
                invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ :
                ∀ (x y : Additive G),
                  Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝;
G: Type ?u.5247

H: Type ?u.5250

inst✝¹: MulOneClass G

inst✝: AddZeroClass H

x: G ≃* Multiplicative H

x✝: G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
                invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ :
                ∀ (x y : Additive G),
                  Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝ 
G: Type ?u.5247

H: Type ?u.5250

inst✝¹: MulOneClass G

inst✝: AddZeroClass H

x: G ≃* Multiplicative H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
            invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_mul' :=
          (_ :
            ∀ (x y : Additive G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      x) =   xrfl
Goals accomplished! 🐙
#align add_equiv.to_multiplicative' 
AddEquiv.toMultiplicative': {G : Type u_1} →
  {H : Type u_2} → [inst : MulOneClass G] → [inst_1 : AddZeroClass H] → Additive G ≃+ H ≃ (G ≃* Multiplicative H)
AddEquiv.toMultiplicative'

/-- Reinterpret `G ≃* Multiplicative H` as `Additive G ≃+ H` as. -/
def 
MulEquiv.toAdditive': [inst : MulOneClass G] → [inst_1 : AddZeroClass H] → G ≃* Multiplicative H ≃ (Additive G ≃+ H)
MulEquiv.toAdditive' [
MulOneClass: Type ?u.7293 → Type ?u.7293
MulOneClass 
G: Type ?u.7287
G] [
AddZeroClass: Type ?u.7296 → Type ?u.7296
AddZeroClass 
H: Type ?u.7290
H] :
    
G: Type ?u.7287
G ≃* 
Multiplicative: Type ?u.7303 → Type ?u.7303
Multiplicative 
H: Type ?u.7290
H ≃ (
Additive: Type ?u.7390 → Type ?u.7390
Additive 
G: Type ?u.7287
G ≃+ 
H: Type ?u.7290
H) :=
  
AddEquiv.toMultiplicative': {G : Type ?u.7454} →
  {H : Type ?u.7453} → [inst : MulOneClass G] → [inst_1 : AddZeroClass H] → Additive G ≃+ H ≃ (G ≃* Multiplicative H)
AddEquiv.toMultiplicative'.
symm: {α : Sort ?u.7469} → {β : Sort ?u.7468} → α ≃ β → β ≃ α
symm
#align mul_equiv.to_additive' 
MulEquiv.toAdditive': {G : Type u_1} →
  {H : Type u_2} → [inst : MulOneClass G] → [inst_1 : AddZeroClass H] → G ≃* Multiplicative H ≃ (Additive G ≃+ H)
MulEquiv.toAdditive'

/-- Reinterpret `G ≃+ Additive H` as `Multiplicative G ≃* H`. -/
def 
AddEquiv.toMultiplicative'': {G : Type u_1} →
  {H : Type u_2} → [inst : AddZeroClass G] → [inst_1 : MulOneClass H] → G ≃+ Additive H ≃ (Multiplicative G ≃* H)
AddEquiv.toMultiplicative'' [
AddZeroClass: Type ?u.7537 → Type ?u.7537
AddZeroClass 
G: Type ?u.7531
G] [
MulOneClass: Type ?u.7540 → Type ?u.7540
MulOneClass 
H: Type ?u.7534
H] :
    
G: Type ?u.7531
G ≃+ 
Additive: Type ?u.7547 → Type ?u.7547
Additive 
H: Type ?u.7534
H ≃ (
Multiplicative: Type ?u.7633 → Type ?u.7633
Multiplicative 
G: Type ?u.7531
G ≃* 
H: Type ?u.7534
H) where
  toFun 
f: ?m.7704
f :=
    ⟨⟨
AddMonoidHom.toMultiplicative'': {α : Type ?u.7763} →
  {β : Type ?u.7762} → [inst : AddZeroClass α] → [inst_1 : MulOneClass β] → (α →+ Additive β) ≃ (Multiplicative α →* β)
AddMonoidHom.toMultiplicative'' 
f: ?m.7704
f.
toAddMonoidHom: {M : Type ?u.7857} → {N : Type ?u.7856} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M ≃+ N → M →+ N
toAddMonoidHom,
     
AddMonoidHom.toMultiplicative': {α : Type ?u.8149} →
  {β : Type ?u.8148} → [inst : MulOneClass α] → [inst_1 : AddZeroClass β] → (Additive α →+ β) ≃ (α →* Multiplicative β)
AddMonoidHom.toMultiplicative' 
f: ?m.7704
f.
symm: {M : Type ?u.8243} → {N : Type ?u.8242} → [inst : Add M] → [inst_1 : Add N] → M ≃+ N → N ≃+ M
symm.
toAddMonoidHom: {M : Type ?u.8303} → {N : Type ?u.8302} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M ≃+ N → M →+ N
toAddMonoidHom, 
f: ?m.7704
f.
1: {A : Type ?u.8571} → {B : Type ?u.8570} → [inst : Add A] → [inst_1 : Add B] → A ≃+ B → A ≃ B
1.
3: ∀ {α : Sort ?u.8577} {β : Sort ?u.8576} (self : α ≃ β), Function.LeftInverse self.invFun self.toFun
3, 
f: ?m.7704
f.
1: {A : Type ?u.8596} → {B : Type ?u.8595} → [inst : Add A] → [inst_1 : Add B] → A ≃+ B → A ≃ B
1.
4: ∀ {α : Sort ?u.8602} {β : Sort ?u.8601} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
4⟩, 
f: ?m.7704
f.
2: ∀ {A : Type ?u.8619} {B : Type ?u.8618} [inst : Add A] [inst_1 : Add B] (self : A ≃+ B) (x y : A),
  Equiv.toFun self.toEquiv (x + y) = Equiv.toFun self.toEquiv x + Equiv.toFun self.toEquiv y
2⟩
  invFun 
f: ?m.8696
f := ⟨⟨
f: ?m.8696
f.
toMonoidHom: {M : Type ?u.8743} → {N : Type ?u.8742} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* N
toMonoidHom, 
f: ?m.8696
f.
symm: {M : Type ?u.8965} → {N : Type ?u.8964} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N ≃* M
symm.
toMonoidHom: {M : Type ?u.8971} → {N : Type ?u.8970} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* N
toMonoidHom, 
f: ?m.8696
f.
1: {M : Type ?u.9185} → {N : Type ?u.9184} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → M ≃ N
1.
3: ∀ {α : Sort ?u.9191} {β : Sort ?u.9190} (self : α ≃ β), Function.LeftInverse self.invFun self.toFun
3, 
f: ?m.8696
f.
1: {M : Type ?u.9196} → {N : Type ?u.9195} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → M ≃ N
1.
4: ∀ {α : Sort ?u.9202} {β : Sort ?u.9201} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
4⟩, 
f: ?m.8696
f.
2: ∀ {M : Type ?u.9207} {N : Type ?u.9206} [inst : Mul M] [inst_1 : Mul N] (self : M ≃* N) (x y : M),
  Equiv.toFun self.toEquiv (x * y) = Equiv.toFun self.toEquiv x * Equiv.toFun self.toEquiv y
2⟩
  left_inv 
x: ?m.9223
x := by
Goals accomplished! 🐙 
G: Type ?u.7531

H: Type ?u.7534

inst✝¹: AddZeroClass G

inst✝: MulOneClass H

x: G ≃+ Additive H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_add' :=
          (_ :
            ∀ (x y : Multiplicative G),
              Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
              invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      x) =   xext
G: Type ?u.7531

H: Type ?u.7534

inst✝¹: AddZeroClass G

inst✝: MulOneClass H

x: G ≃+ Additive H

x✝: G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ :
                ∀ (x y : Multiplicative G),
                  Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
                  invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝;
G: Type ?u.7531

H: Type ?u.7534

inst✝¹: AddZeroClass G

inst✝: MulOneClass H

x: G ≃+ Additive H

x✝: G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ :
                ∀ (x y : Multiplicative G),
                  Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
                  invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝ 
G: Type ?u.7531

H: Type ?u.7534

inst✝¹: AddZeroClass G

inst✝: MulOneClass H

x: G ≃+ Additive H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_add' :=
          (_ :
            ∀ (x y : Multiplicative G),
              Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
              invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      x) =   xrfl
Goals accomplished! 🐙
  right_inv 
x: ?m.9229
x := by
Goals accomplished! 🐙 
G: Type ?u.7531

H: Type ?u.7534

inst✝¹: AddZeroClass G

inst✝: MulOneClass H

x: Multiplicative G ≃* H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
            invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_mul' :=
          (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ :
              ∀ (x y : Multiplicative G),
                Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      x) =   xext
G: Type ?u.7531

H: Type ?u.7534

inst✝¹: AddZeroClass G

inst✝: MulOneClass H

x: Multiplicative G ≃* H

x✝: Multiplicative G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
                invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ :
                  ∀ (x y : Multiplicative G),
                    Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝;
G: Type ?u.7531

H: Type ?u.7534

inst✝¹: AddZeroClass G

inst✝: MulOneClass H

x: Multiplicative G ≃* H

x✝: Multiplicative G

h
↑((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
                invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        ((fun f =>
            {
              toEquiv :=
                { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ :
                  ∀ (x y : Multiplicative G),
                    Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          x))
    x✝ =   ↑x x✝ 
G: Type ?u.7531

H: Type ?u.7534

inst✝¹: AddZeroClass G

inst✝: MulOneClass H

x: Multiplicative G ≃* H

(fun f =>
      {
        toEquiv :=
          { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
            invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
            left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
            right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
        map_mul' :=
          (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
    ((fun f =>
        {
          toEquiv :=
            { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ :
              ∀ (x y : Multiplicative G),
                Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      x) =   xrfl
Goals accomplished! 🐙
#align add_equiv.to_multiplicative'' 
AddEquiv.toMultiplicative'': {G : Type u_1} →
  {H : Type u_2} → [inst : AddZeroClass G] → [inst_1 : MulOneClass H] → G ≃+ Additive H ≃ (Multiplicative G ≃* H)
AddEquiv.toMultiplicative''

/-- Reinterpret `Multiplicative G ≃* H` as `G ≃+ Additive H` as. -/
def 
MulEquiv.toAdditive'': {G : Type u_1} →
  {H : Type u_2} → [inst : AddZeroClass G] → [inst_1 : MulOneClass H] → Multiplicative G ≃* H ≃ (G ≃+ Additive H)
MulEquiv.toAdditive'' [
AddZeroClass: Type ?u.9577 → Type ?u.9577
AddZeroClass 
G: Type ?u.9571
G] [
MulOneClass: Type ?u.9580 → Type ?u.9580
MulOneClass 
H: Type ?u.9574
H] :
    
Multiplicative: Type ?u.9587 → Type ?u.9587
Multiplicative 
G: Type ?u.9571
G ≃* 
H: Type ?u.9574
H ≃ (
G: Type ?u.9571
G ≃+ 
Additive: Type ?u.9674 → Type ?u.9674
Additive 
H: Type ?u.9574
H) :=
  
AddEquiv.toMultiplicative'': {G : Type ?u.9738} →
  {H : Type ?u.9737} → [inst : AddZeroClass G] → [inst_1 : MulOneClass H] → G ≃+ Additive H ≃ (Multiplicative G ≃* H)
AddEquiv.toMultiplicative''.
symm: {α : Sort ?u.9753} → {β : Sort ?u.9752} → α ≃ β → β ≃ α
symm
#align mul_equiv.to_additive'' 
MulEquiv.toAdditive'': {G : Type u_1} →
  {H : Type u_2} → [inst : AddZeroClass G] → [inst_1 : MulOneClass H] → Multiplicative G ≃* H ≃ (G ≃+ Additive H)
MulEquiv.toAdditive''

section

variable (
G: ?m.9821
G) (
H: ?m.9824
H)

/-- `Additive (Multiplicative G)` is just `G`. -/
def 
AddEquiv.additiveMultiplicative: (G : Type u_1) → [inst : AddZeroClass G] → Additive (Multiplicative G) ≃+ G
AddEquiv.additiveMultiplicative [
AddZeroClass: Type ?u.9833 → Type ?u.9833
AddZeroClass 
G: Type ?u.9827
G] : 
Additive: Type ?u.9838 → Type ?u.9838
Additive (
Multiplicative: Type ?u.9839 → Type ?u.9839
Multiplicative 
G: Type ?u.9827
G) ≃+ 
G: Type ?u.9827
G :=
  
MulEquiv.toAdditive': {G : Type ?u.9877} →
  {H : Type ?u.9876} → [inst : MulOneClass G] → [inst_1 : AddZeroClass H] → G ≃* Multiplicative H ≃ (Additive G ≃+ H)
MulEquiv.toAdditive' (
MulEquiv.refl: (M : Type ?u.9972) → [inst : Mul M] → M ≃* M
MulEquiv.refl (
Multiplicative: Type ?u.9973 → Type ?u.9973
Multiplicative 
G: Type ?u.9827
G))
#align add_equiv.additive_multiplicative 
AddEquiv.additiveMultiplicative: (G : Type u_1) → [inst : AddZeroClass G] → Additive (Multiplicative G) ≃+ G
AddEquiv.additiveMultiplicative

/-- `Multiplicative (Additive H)` is just `H`. -/
def 
MulEquiv.multiplicativeAdditive: [inst : MulOneClass H] → Multiplicative (Additive H) ≃* H
MulEquiv.multiplicativeAdditive [
MulOneClass: Type ?u.10086 → Type ?u.10086
MulOneClass 
H: Type ?u.10083
H] : 
Multiplicative: Type ?u.10091 → Type ?u.10091
Multiplicative (
Additive: Type ?u.10092 → Type ?u.10092
Additive 
H: Type ?u.10083
H) ≃* 
H: Type ?u.10083
H :=
  
AddEquiv.toMultiplicative'': {G : Type ?u.10218} →
  {H : Type ?u.10217} → [inst : AddZeroClass G] → [inst_1 : MulOneClass H] → G ≃+ Additive H ≃ (Multiplicative G ≃* H)
AddEquiv.toMultiplicative'' (
AddEquiv.refl: (M : Type ?u.10313) → [inst : Add M] → M ≃+ M
AddEquiv.refl (
Additive: Type ?u.10314 → Type ?u.10314
Additive 
H: Type ?u.10083
H))
#align mul_equiv.multiplicative_additive 
MulEquiv.multiplicativeAdditive: (H : Type u_1) → [inst : MulOneClass H] → Multiplicative (Additive H) ≃* H
MulEquiv.multiplicativeAdditive

end