[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
g : N → M
h₁ : Function.LeftInverse g ↑f
⊢ g 1 = 1
[PROOFSTEP]
rw [← f.map_one, h₁]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
g : N → M
h₁ : Function.LeftInverse g ↑f
h₂ : Function.RightInverse g ↑f
x y : N
⊢ g (x * y) = g (↑f (g x) * ↑f (g y))
[PROOFSTEP]
rw [h₂ x, h₂ y]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
g : N → M
h₁ : Function.LeftInverse g ↑f
h₂ : Function.RightInverse g ↑f
x y : N
⊢ g (↑f (g x) * ↑f (g y)) = g (↑f (g x * g y))
[PROOFSTEP]
rw [f.map_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulEquivClass F M N
src✝ : MulHomClass F M N := instMulHomClass F
e : F
⊢ ↑e 1 * ↑e (EquivLike.inv e 1) = ↑e (EquivLike.inv e 1)
[PROOFSTEP]
rw [← map_mul, one_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝² : MulZeroClass α
inst✝¹ : MulZeroClass β
inst✝ : MulEquivClass F α β
e : F
⊢ ↑e 0 = ↑e 0 * ↑e (EquivLike.inv e 0)
[PROOFSTEP]
rw [← map_mul, zero_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝² : MulZeroClass α
inst✝¹ : MulZeroClass β
inst✝ : MulEquivClass F α β
e : F
⊢ ↑e 0 * ↑e (EquivLike.inv e 0) = 0
[PROOFSTEP]
simp
  -- See note [lower instance priority]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
f g : M ≃* N
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
g : M ≃* N
toEquiv✝ : M ≃ N
map_mul'✝ : ∀ (x y : M), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
h₁ : (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ } = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ } = (fun f => f.invFun) g
⊢ { toEquiv := toEquiv✝, map_mul' := map_mul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
toEquiv✝¹ : M ≃ N
map_mul'✝¹ : ∀ (x y : M), Equiv.toFun toEquiv✝¹ (x * y) = Equiv.toFun toEquiv✝¹ x * Equiv.toFun toEquiv✝¹ y
toEquiv✝ : M ≃ N
map_mul'✝ : ∀ (x y : M), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
h₁ :
  (fun f => f.toFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }
h₂ :
  (fun f => f.invFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }
⊢ { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } = { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toEquiv
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
toEquiv✝¹ : M ≃ N
map_mul'✝¹ : ∀ (x y : M), Equiv.toFun toEquiv✝¹ (x * y) = Equiv.toFun toEquiv✝¹ x * Equiv.toFun toEquiv✝¹ y
toEquiv✝ : M ≃ N
map_mul'✝ : ∀ (x y : M), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
h₁ :
  (fun f => f.toFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }
h₂ :
  (fun f => f.invFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }
⊢ toEquiv✝¹ = toEquiv✝
[PROOFSTEP]
apply Equiv.coe_fn_injective h₁
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : Mul P
inst✝ : Mul Q
h1 : M ≃* N
h2 : N ≃* P
src✝ : M ≃ P := h1.trans h2.toEquiv
x y : M
⊢ ↑h2 (↑h1 (x * y)) = ↑h2 (↑h1 x) * ↑h2 (↑h1 y)
[PROOFSTEP]
rw [h1.map_mul, h2.map_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h : M → P
⊢ (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h : M → P
x✝ : M
⊢ (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) x✝ = h x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
k : N → Q
⊢ (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
k : N → Q
x✝ : N
⊢ (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) x✝ = k x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h k : M → P
⊢ Equiv.toFun
      { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
        left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
        right_inv := (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
      (h * k) =
    Equiv.toFun
        { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
          left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
          right_inv := (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
        h *
      Equiv.toFun
        { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
          left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
          right_inv := (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
        k
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h k : M → P
x✝ : N
⊢ Equiv.toFun
      { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
        left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
        right_inv := (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
      (h * k) x✝ =
    (Equiv.toFun
          { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
            left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
            right_inv :=
              (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
          h *
        Equiv.toFun
          { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
            left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
            right_inv :=
              (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
          k)
      x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
h : M →* P
⊢ (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
      ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
    h
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
h : M →* P
x✝ : M
⊢ ↑((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
          ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h))
      x✝ =
    ↑h x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
k : N →* Q
⊢ (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
      ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
    k
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
k : N →* Q
x✝ : N
⊢ ↑((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
          ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k))
      x✝ =
    ↑k x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
h k : M →* P
⊢ Equiv.toFun
      { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
        invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
        left_inv :=
          (_ :
            ∀ (h : M →* P),
              (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                  ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                h),
        right_inv :=
          (_ :
            ∀ (k : N →* Q),
              (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                  ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                k) }
      (h * k) =
    Equiv.toFun
        { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
          invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
          left_inv :=
            (_ :
              ∀ (h : M →* P),
                (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                    ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                  h),
          right_inv :=
            (_ :
              ∀ (k : N →* Q),
                (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                    ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                  k) }
        h *
      Equiv.toFun
        { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
          invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
          left_inv :=
            (_ :
              ∀ (h : M →* P),
                (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                    ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                  h),
          right_inv :=
            (_ :
              ∀ (k : N →* Q),
                (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                    ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                  k) }
        k
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
h k : M →* P
x✝ : N
⊢ ↑(Equiv.toFun
          { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
            invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
            left_inv :=
              (_ :
                ∀ (h : M →* P),
                  (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                      ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                    h),
            right_inv :=
              (_ :
                ∀ (k : N →* Q),
                  (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                      ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                    k) }
          (h * k))
      x✝ =
    ↑(Equiv.toFun
            { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
              invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
              left_inv :=
                (_ :
                  ∀ (h : M →* P),
                    (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                        ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                      h),
              right_inv :=
                (_ :
                  ∀ (k : N →* Q),
                    (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                        ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                      k) }
            h *
          Equiv.toFun
            { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
              invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
              left_inv :=
                (_ :
                  ∀ (h : M →* P),
                    (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                        ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                      h),
              right_inv :=
                (_ :
                  ∀ (k : N →* Q),
                    (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                        ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                      k) }
            k)
      x✝
[PROOFSTEP]
simp
