[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
⊢ ∀ (a b c : M →* N), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ b✝ c✝ : M →* N
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
ext
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ b✝ c✝ : M →* N
x✝ : M
⊢ ↑(a✝ * b✝ * c✝) x✝ = ↑(a✝ * (b✝ * c✝)) x✝
[PROOFSTEP]
apply mul_assoc
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
⊢ ∀ (a : M →* N), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ : M →* N
⊢ 1 * a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ : M →* N
x✝ : M
⊢ ↑(1 * a✝) x✝ = ↑a✝ x✝
[PROOFSTEP]
apply one_mul
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
⊢ ∀ (a : M →* N), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ : M →* N
⊢ a✝ * 1 = a✝
[PROOFSTEP]
ext
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ : M →* N
x✝ : M
⊢ ↑(a✝ * 1) x✝ = ↑a✝ x✝
[PROOFSTEP]
apply mul_one
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
n : ℕ
f : M →* N
⊢ (fun x => ↑f x ^ n) 1 = 1
[PROOFSTEP]
simp
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
n : ℕ
f : M →* N
x y : M
⊢ OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } (x * y) =
    OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } x *
      OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } y
[PROOFSTEP]
simp [mul_pow]
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f : M →* N
⊢ (fun n f =>
        { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
          map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
      0 f =
    1
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f : M →* N
x : M
⊢ ↑((fun n f =>
            { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
              map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
          0 f)
      x =
    ↑1 x
[PROOFSTEP]
simp
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
n : ℕ
f : M →* N
⊢ (fun n f =>
        { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
          map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
      (n + 1) f =
    f *
      (fun n f =>
          { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
            map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
        n f
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
n : ℕ
f : M →* N
x : M
⊢ ↑((fun n f =>
            { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
              map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
          (n + 1) f)
      x =
    ↑(f *
          (fun n f =>
              { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
                map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
            n f)
      x
[PROOFSTEP]
simp [pow_succ]
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
⊢ ∀ (a b : M →* N), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ b✝ : M →* N
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
ext
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ b✝ : M →* N
x✝ : M
⊢ ↑(a✝ * b✝) x✝ = ↑(b✝ * a✝) x✝
[PROOFSTEP]
apply mul_comm
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
⊢ ∀ (a b : M →* G), a / b = a * b⁻¹
[PROOFSTEP]
intros
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
a✝ b✝ : M →* G
⊢ a✝ / b✝ = a✝ * b✝⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
a✝ b✝ : M →* G
x✝ : M
⊢ ↑(a✝ / b✝) x✝ = ↑(a✝ * b✝⁻¹) x✝
[PROOFSTEP]
apply div_eq_mul_inv
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℤ
f : M →* G
⊢ (fun x => ↑f x ^ n) 1 = 1
[PROOFSTEP]
simp
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℤ
f : M →* G
x y : M
⊢ OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } (x * y) =
    OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } x *
      OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } y
[PROOFSTEP]
simp [mul_zpow]
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
f : M →* G
⊢ (fun n f =>
        { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
          map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
      0 f =
    1
[PROOFSTEP]
ext x
[GOAL]
case h
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
f : M →* G
x : M
⊢ ↑((fun n f =>
            { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
              map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
          0 f)
      x =
    ↑1 x
[PROOFSTEP]
simp
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℕ
f : M →* G
⊢ (fun n f =>
        { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
          map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
      (Int.ofNat (Nat.succ n)) f =
    f *
      (fun n f =>
          { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
            map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
        (Int.ofNat n) f
[PROOFSTEP]
ext x
[GOAL]
case h
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℕ
f : M →* G
x : M
⊢ ↑((fun n f =>
            { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
              map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
          (Int.ofNat (Nat.succ n)) f)
      x =
    ↑(f *
          (fun n f =>
              { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
                map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
            (Int.ofNat n) f)
      x
[PROOFSTEP]
simp [zpow_ofNat, pow_succ]
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℕ
f : M →* G
⊢ (fun n f =>
        { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
          map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
      (Int.negSucc n) f =
    ((fun n f =>
          { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
            map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
        (↑(Nat.succ n)) f)⁻¹
[PROOFSTEP]
ext x
[GOAL]
case h
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℕ
f : M →* G
x : M
⊢ ↑((fun n f =>
            { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
              map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
          (Int.negSucc n) f)
      x =
    ↑((fun n f =>
              { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
                map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
            (↑(Nat.succ n)) f)⁻¹
      x
[PROOFSTEP]
simp [Nat.succ_eq_add_one, zpow_ofNat]
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
⊢ ∀ (a : M →* G), a⁻¹ * a = 1
[PROOFSTEP]
intros
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
a✝ : M →* G
⊢ a✝⁻¹ * a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case h
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
a✝ : M →* G
x✝ : M
⊢ ↑(a✝⁻¹ * a✝) x✝ = ↑1 x✝
[PROOFSTEP]
apply mul_left_inv
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
mM : MulOneClass M
mN : MulOneClass N
mP : CommMonoid P
f : M →* N →* P
y : N
⊢ (fun x => ↑(↑f x) y) 1 = 1
[PROOFSTEP]
simp [f.map_one, one_apply]
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
mM : MulOneClass M
mN : MulOneClass N
mP : CommMonoid P
f : M →* N →* P
y : N
x₁ x₂ : M
⊢ OneHom.toFun { toFun := fun x => ↑(↑f x) y, map_one' := (_ : ↑(↑f 1) y = 1) } (x₁ * x₂) =
    OneHom.toFun { toFun := fun x => ↑(↑f x) y, map_one' := (_ : ↑(↑f 1) y = 1) } x₁ *
      OneHom.toFun { toFun := fun x => ↑(↑f x) y, map_one' := (_ : ↑(↑f 1) y = 1) } x₂
[PROOFSTEP]
simp [f.map_mul, mul_apply]
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
⊢ (fun g =>
        { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
          map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
      1 =
    1
[PROOFSTEP]
ext1 f
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
f : M →* N
⊢ ↑((fun g =>
            { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
              map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
          1)
      f =
    ↑1 f
[PROOFSTEP]
exact one_comp f
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g₁ g₂ : N →* P
⊢ OneHom.toFun
      {
        toFun := fun g =>
          { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
            map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
        map_one' :=
          (_ :
            (fun g =>
                  { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                    map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                1 =
              1) }
      (g₁ * g₂) =
    OneHom.toFun
        {
          toFun := fun g =>
            { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
              map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
          map_one' :=
            (_ :
              (fun g =>
                    { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                      map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                  1 =
                1) }
        g₁ *
      OneHom.toFun
        {
          toFun := fun g =>
            { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
              map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
          map_one' :=
            (_ :
              (fun g =>
                    { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                      map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                  1 =
                1) }
        g₂
[PROOFSTEP]
ext1 f
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g₁ g₂ : N →* P
f : M →* N
⊢ ↑(OneHom.toFun
          {
            toFun := fun g =>
              { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
            map_one' :=
              (_ :
                (fun g =>
                      { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                        map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                    1 =
                  1) }
          (g₁ * g₂))
      f =
    ↑(OneHom.toFun
            {
              toFun := fun g =>
                { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                  map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
              map_one' :=
                (_ :
                  (fun g =>
                        { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                          map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                      1 =
                    1) }
            g₁ *
          OneHom.toFun
            {
              toFun := fun g =>
                { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                  map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
              map_one' :=
                (_ :
                  (fun g =>
                        { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                          map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                      1 =
                    1) }
            g₂)
      f
[PROOFSTEP]
exact mul_comp g₁ g₂ f
