[GOAL]
G : Type u_1
H : Type u_2
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) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : AddZeroClass H
x : G ≃+ H
x✝ : G
⊢ ↑((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✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
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) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : AddZeroClass H
x : Multiplicative G ≃* Multiplicative H
x✝ : Multiplicative G
⊢ ↑((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✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
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) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : MulOneClass H
x : G ≃* H
x✝ : G
⊢ ↑((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✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
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) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : MulOneClass H
x : Additive G ≃+ Additive H
x✝ : Additive G
⊢ ↑((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✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
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) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : AddZeroClass H
x : Additive G ≃+ H
x✝ : Additive G
⊢ ↑((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✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
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) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : AddZeroClass H
x : G ≃* Multiplicative H
x✝ : G
⊢ ↑((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✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
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) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : MulOneClass H
x : G ≃+ Additive H
x✝ : G
⊢ ↑((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✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
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) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : MulOneClass H
x : Multiplicative G ≃* H
x✝ : Multiplicative G
⊢ ↑((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✝
[PROOFSTEP]
rfl
