/-
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov

! This file was ported from Lean 3 source module algebra.hom.iterate
! leanprover-community/mathlib commit 792a2a264169d64986541c6f8f7e3bbb6acb6295
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.GroupPower.Lemmas
import Mathlib.GroupTheory.GroupAction.Opposite

/-!
# Iterates of monoid and ring homomorphisms

Iterate of a monoid/ring homomorphism is a monoid/ring homomorphism but it has a wrong type, so Lean
can't apply lemmas like `MonoidHom.map_one` to `f^[n] 1`. Though it is possible to define
a monoid structure on the endomorphisms, quite often we do not want to convert from
`M →* M` to `Monoid.End M` and from `f^[n]` to `f^n` just to apply a simple lemma.

So, we restate standard `*Hom.map_*` lemmas under names `*Hom.iterate_map_*`.

We also prove formulas for iterates of add/mul left/right.

## Tags

homomorphism, iterate
-/


open Function

variable {
M: Type ?u.46544
M : 
Type _: Type (?u.2+1)
Type _} {
N: Type ?u.17
N : 
Type _: Type (?u.17+1)
Type _} {
G: Type ?u.34788
G : 
Type _: Type (?u.8+1)
Type _} {
H: Type ?u.32619
H : 
Type _: Type (?u.51637+1)
Type _}

/-- An auxiliary lemma that can be used to prove `⇑(f ^ n) = (⇑f^[n])`. -/
theorem 
hom_coe_pow: ∀ {F : Type u_1} [inst : Monoid F] (c : F → M → M),
  c 1 = id → (∀ (f g : F), c (f * g) = c f ∘ c g) → ∀ (f : F) (n : ℕ), c (f ^ n) = c f^[n]
hom_coe_pow {
F: Type ?u.26
F : 
Type _: Type (?u.26+1)
Type _} [
Monoid: Type ?u.29 → Type ?u.29
Monoid 
F: Type ?u.26
F] (
c: F → M → M
c : 
F: Type ?u.26
F → 
M: Type ?u.14
M → 
M: Type ?u.14
M) (
h1: c 1 = id
h1 : 
c: F → M → M
c 
1: ?m.40
1 = 
id: {α : Sort ?u.370} → α → α
id)
    (
hmul: ∀ (f g : F), c (f * g) = c f ∘ c g
hmul : ∀ 
f: ?m.413
f 
g: ?m.416
g, 
c: F → M → M
c (
f: ?m.413
f * 
g: ?m.416
g) = 
c: F → M → M
c 
f: ?m.413
f ∘ 
c: F → M → M
c 
g: ?m.416
g) (
f: F
f : 
F: Type ?u.26
F) : ∀ 
n: ?m.1010
n, 
c: F → M → M
c (
f: F
f ^ 
n: ?m.1010
n) = 
c: F → M → M
c 
f: F
f^[
n: ?m.1010
n]
  | 
0: ℕ
0 => by
Goals accomplished! 🐙
    
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

c (f ^ 0) = c f^[0]rw [
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

c (f ^ 0) = c f^[0]
pow_zero: ∀ {M : Type ?u.1287} [inst : Monoid M] (a : M), a ^ 0 = 1
pow_zero,
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

c 1 = c f^[0] 
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

c (f ^ 0) = c f^[0]
h1: c 1 = id
h1
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

id = c f^[0]]
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

id = c f^[0]
    
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

c (f ^ 0) = c f^[0]rfl
Goals accomplished! 🐙
  | 
n: ℕ
n + 1 => by
Goals accomplished! 🐙 
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

n: ℕ

c (f ^ (n + 1)) = c f^[n + 1]rw [
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

n: ℕ

c (f ^ (n + 1)) = c f^[n + 1]
pow_succ: ∀ {M : Type ?u.1382} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
pow_succ,
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

n: ℕ

c (f * f ^ n) = c f^[n + 1] 
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

n: ℕ

c (f ^ (n + 1)) = c f^[n + 1]
iterate_succ': ∀ {α : Type ?u.1426} (f : α → α) (n : ℕ), f^[Nat.succ n] = f ∘ f^[n]
iterate_succ',
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

n: ℕ

c (f * f ^ n) = c f ∘ c f^[n] 
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

n: ℕ

c (f ^ (n + 1)) = c f^[n + 1]
hmul: ∀ (f g : F), c (f * g) = c f ∘ c g
hmul,
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

n: ℕ

c f ∘ c (f ^ n) = c f ∘ c f^[n] 
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

n: ℕ

c (f ^ (n + 1)) = c f^[n + 1]
hom_coe_pow: ∀ {F : Type u_1} [inst : Monoid F] (c : F → M → M),
  c 1 = id → (∀ (f g : F), c (f * g) = c f ∘ c g) → ∀ (f : F) (n : ℕ), c (f ^ n) = c f^[n]
hom_coe_pow 
c: F → M → M
c 
h1: c 1 = id
h1 
hmul: ∀ (f g : F), c (f * g) = c f ∘ c g
hmul 
f: F
f 
n: ℕ
n
M: Type u_2

N: Type ?u.17

G: Type ?u.20

H: Type ?u.23

F: Type u_1

inst✝: Monoid F

c: F → M → M

h1: c 1 = id

hmul: ∀ (f g : F), c (f * g) = c f ∘ c g

f: F

n: ℕ

c f ∘ c f^[n] = c f ∘ c f^[n]]
Goals accomplished! 🐙
#align hom_coe_pow 
hom_coe_pow: ∀ {M : Type u_2} {F : Type u_1} [inst : Monoid F] (c : F → M → M),
  c 1 = id → (∀ (f g : F), c (f * g) = c f ∘ c g) → ∀ (f : F) (n : ℕ), c (f ^ n) = c f^[n]
hom_coe_pow

namespace MonoidHom

section

variable [
MulOneClass: Type ?u.2631 → Type ?u.2631
MulOneClass 
M: Type ?u.1575
M] [
MulOneClass: Type ?u.1590 → Type ?u.1590
MulOneClass 
N: Type ?u.1578
N]

@[
to_additive: ∀ {M : Type u_1} [inst : AddZeroClass M] (f : M →+ M) (n : ℕ), (↑f^[n]) 0 = 0
to_additive (attr := simp)]
theorem 
iterate_map_one: ∀ {M : Type u_1} [inst : MulOneClass M] (f : M →* M) (n : ℕ), (↑f^[n]) 1 = 1
iterate_map_one (
f: M →* M
f : 
M: Type ?u.1593
M →* 
M: Type ?u.1593
M) (
n: ℕ
n : 
ℕ: Type
ℕ) : (
f: M →* M
f^[
n: ℕ
n]) 
1: ?m.2020
1 = 
1: ?m.2482
1 :=
  
iterate_fixed: ∀ {α : Type ?u.2501} {f : α → α} {x : α}, f x = x → ∀ (n : ℕ), (f^[n]) x = x
iterate_fixed 
f: M →* M
f.
map_one: ∀ {M : Type ?u.2505} {N : Type ?u.2506} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N), ↑f 1 = 1
map_one 
n: ℕ
n
#align monoid_hom.iterate_map_one 
MonoidHom.iterate_map_one: ∀ {M : Type u_1} [inst : MulOneClass M] (f : M →* M) (n : ℕ), (↑f^[n]) 1 = 1
MonoidHom.iterate_map_one
#align add_monoid_hom.iterate_map_zero 
AddMonoidHom.iterate_map_zero: ∀ {M : Type u_1} [inst : AddZeroClass M] (f : M →+ M) (n : ℕ), (↑f^[n]) 0 = 0
AddMonoidHom.iterate_map_zero

@[
to_additive: ∀ {M : Type u_1} [inst : AddZeroClass M] (f : M →+ M) (n : ℕ) (x y : M), (↑f^[n]) (x + y) = (↑f^[n]) x + (↑f^[n]) y
to_additive (attr := simp)]
theorem 
iterate_map_mul: ∀ (f : M →* M) (n : ℕ) (x y : M), (↑f^[n]) (x * y) = (↑f^[n]) x * (↑f^[n]) y
iterate_map_mul (
f: M →* M
f : 
M: Type ?u.2619
M →* 
M: Type ?u.2619
M) (
n: ℕ
n : 
ℕ: Type
ℕ) (
x: M
x 
y: M
y) : (
f: M →* M
f^[
n: ℕ
n]) (
x: ?m.2650
x * 
y: ?m.2653
y) = (
f: M →* M
f^[
n: ℕ
n]) 
x: ?m.2650
x * (
f: M →* M
f^[
n: ℕ
n]) 
y: ?m.2653
y :=
  
Semiconj₂.iterate: ∀ {α : Type ?u.4657} {f : α → α} {op : α → α → α}, Semiconj₂ f op op → ∀ (n : ℕ), Semiconj₂ (f^[n]) op op
Semiconj₂.iterate 
f: M →* M
f.
map_mul: ∀ {M : Type ?u.4661} {N : Type ?u.4662} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (a b : M),
  ↑f (a * b) = ↑f a * ↑f b
map_mul 
n: ℕ
n 
x: M
x 
y: M
y
#align monoid_hom.iterate_map_mul 
MonoidHom.iterate_map_mul: ∀ {M : Type u_1} [inst : MulOneClass M] (f : M →* M) (n : ℕ) (x y : M), (↑f^[n]) (x * y) = (↑f^[n]) x * (↑f^[n]) y
MonoidHom.iterate_map_mul
#align add_monoid_hom.iterate_map_add 
AddMonoidHom.iterate_map_add: ∀ {M : Type u_1} [inst : AddZeroClass M] (f : M →+ M) (n : ℕ) (x y : M), (↑f^[n]) (x + y) = (↑f^[n]) x + (↑f^[n]) y
AddMonoidHom.iterate_map_add

end

variable [
Monoid: Type ?u.7992 → Type ?u.7992
Monoid 
M: Type ?u.4835
M] [
Monoid: Type ?u.6192 → Type ?u.6192
Monoid 
N: Type ?u.4838
N] [
Group: Type ?u.4829 → Type ?u.4829
Group 
G: Type ?u.4841
G] [
Group: Type ?u.4832 → Type ?u.4832
Group 
H: Type ?u.7989
H]

@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (x : G), (↑f^[n]) (-x) = -(↑f^[n]) x
to_additive (attr := simp)]
theorem 
iterate_map_inv: ∀ (f : G →* G) (n : ℕ) (x : G), (↑f^[n]) x⁻¹ = ((↑f^[n]) x)⁻¹
iterate_map_inv (
f: G →* G
f : 
G: Type ?u.4841
G →* 
G: Type ?u.4841
G) (
n: ℕ
n : 
ℕ: Type
ℕ) (
x: G
x) : (
f: G →* G
f^[
n: ℕ
n]) 
x: ?m.5113
x⁻¹ = ((
f: G →* G
f^[
n: ℕ
n]) 
x: ?m.5113
x)⁻¹ :=
  
Commute.iterate_left: ∀ {α : Type ?u.6001} {f g : α → α}, Function.Commute f g → ∀ (n : ℕ), Function.Commute (f^[n]) g
Commute.iterate_left 
f: G →* G
f.
map_inv: ∀ {α : Type ?u.6005} {β : Type ?u.6006} [inst : Group α] [inst_1 : DivisionMonoid β] (f : α →* β) (a : α),
  ↑f a⁻¹ = (↑f a)⁻¹
map_inv 
n: ℕ
n 
x: G
x
#align monoid_hom.iterate_map_inv 
MonoidHom.iterate_map_inv: ∀ {G : Type u_1} [inst : Group G] (f : G →* G) (n : ℕ) (x : G), (↑f^[n]) x⁻¹ = ((↑f^[n]) x)⁻¹
MonoidHom.iterate_map_inv
#align add_monoid_hom.iterate_map_neg 
AddMonoidHom.iterate_map_neg: ∀ {G : Type u_1} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (x : G), (↑f^[n]) (-x) = -(↑f^[n]) x
AddMonoidHom.iterate_map_neg

@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (x y : G), (↑f^[n]) (x - y) = (↑f^[n]) x - (↑f^[n]) y
to_additive (attr := simp)]
theorem 
iterate_map_div: ∀ (f : G →* G) (n : ℕ) (x y : G), (↑f^[n]) (x / y) = (↑f^[n]) x / (↑f^[n]) y
iterate_map_div (
f: G →* G
f : 
G: Type ?u.6183
G →* 
G: Type ?u.6183
G) (
n: ℕ
n : 
ℕ: Type
ℕ) (
x: G
x 
y: G
y) : (
f: G →* G
f^[
n: ℕ
n]) (
x: ?m.6455
x / 
y: ?m.6458
y) = (
f: G →* G
f^[
n: ℕ
n]) 
x: ?m.6455
x / (
f: G →* G
f^[
n: ℕ
n]) 
y: ?m.6458
y :=
  
Semiconj₂.iterate: ∀ {α : Type ?u.7779} {f : α → α} {op : α → α → α}, Semiconj₂ f op op → ∀ (n : ℕ), Semiconj₂ (f^[n]) op op
Semiconj₂.iterate 
f: G →* G
f.
map_div: ∀ {α : Type ?u.7783} {β : Type ?u.7784} [inst : Group α] [inst_1 : DivisionMonoid β] (f : α →* β) (g h : α),
  ↑f (g / h) = ↑f g / ↑f h
map_div 
n: ℕ
n 
x: G
x 
y: G
y
#align monoid_hom.iterate_map_div 
MonoidHom.iterate_map_div: ∀ {G : Type u_1} [inst : Group G] (f : G →* G) (n : ℕ) (x y : G), (↑f^[n]) (x / y) = (↑f^[n]) x / (↑f^[n]) y
MonoidHom.iterate_map_div
#align add_monoid_hom.iterate_map_sub 
AddMonoidHom.iterate_map_sub: ∀ {G : Type u_1} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (x y : G), (↑f^[n]) (x - y) = (↑f^[n]) x - (↑f^[n]) y
AddMonoidHom.iterate_map_sub

theorem 
iterate_map_pow: ∀ (f : M →* M) (n : ℕ) (a : M) (m : ℕ), (↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
iterate_map_pow (
f: M →* M
f : 
M: Type ?u.7980
M →* 
M: Type ?u.7980
M) (
n: ℕ
n : 
ℕ: Type
ℕ) (
a: M
a) (
m: ℕ
m : 
ℕ: Type
ℕ) : (
f: M →* M
f^[
n: ℕ
n]) (
a: ?m.8241
a ^ 
m: ℕ
m) = (
f: M →* M
f^[
n: ℕ
n]) 
a: ?m.8241
a ^ 
m: ℕ
m :=
  
Commute.iterate_left: ∀ {α : Type ?u.14012} {f g : α → α}, Function.Commute f g → ∀ (n : ℕ), Function.Commute (f^[n]) g
Commute.iterate_left (fun 
x: ?m.14017
x => 
f: M →* M
f.
map_pow: ∀ {M : Type ?u.14019} {N : Type ?u.14020} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (a : M) (n : ℕ),
  ↑f (a ^ n) = ↑f a ^ n
map_pow 
x: ?m.14017
x 
m: ℕ
m) 
n: ℕ
n 
a: M
a
#align monoid_hom.iterate_map_pow 
MonoidHom.iterate_map_pow: ∀ {M : Type u_1} [inst : Monoid M] (f : M →* M) (n : ℕ) (a : M) (m : ℕ), (↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
MonoidHom.iterate_map_pow

theorem 
iterate_map_zpow: ∀ (f : G →* G) (n : ℕ) (a : G) (m : ℤ), (↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
iterate_map_zpow (
f: G →* G
f : 
G: Type ?u.14072
G →* 
G: Type ?u.14072
G) (
n: ℕ
n : 
ℕ: Type
ℕ) (
a: ?m.14344
a) (
m: ℤ
m : 
ℤ: Type
ℤ) : (
f: G →* G
f^[
n: ℕ
n]) (
a: ?m.14344
a ^ 
m: ℤ
m) = (
f: G →* G
f^[
n: ℕ
n]) 
a: ?m.14344
a ^ 
m: ℤ
m :=
  
Commute.iterate_left: ∀ {α : Type ?u.20274} {f g : α → α}, Function.Commute f g → ∀ (n : ℕ), Function.Commute (f^[n]) g
Commute.iterate_left (fun 
x: ?m.20279
x => 
f: G →* G
f.
map_zpow: ∀ {α : Type ?u.20281} {β : Type ?u.20282} [inst : Group α] [inst_1 : DivisionMonoid β] (f : α →* β) (g : α) (n : ℤ),
  ↑f (g ^ n) = ↑f g ^ n
map_zpow 
x: ?m.20279
x 
m: ℤ
m) 
n: ℕ
n 
a: G
a
#align monoid_hom.iterate_map_zpow 
MonoidHom.iterate_map_zpow: ∀ {G : Type u_1} [inst : Group G] (f : G →* G) (n : ℕ) (a : G) (m : ℤ), (↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
MonoidHom.iterate_map_zpow

theorem 
coe_pow: ∀ {M : Type u_1} [inst : CommMonoid M] (f : Monoid.End M) (n : ℕ), ↑(f ^ n) = ↑f^[n]
coe_pow {
M: Type u_1
M} [
CommMonoid: Type ?u.20403 → Type ?u.20403
CommMonoid 
M: ?m.20400
M] (
f: Monoid.End M
f : 
Monoid.End: (M : Type ?u.20406) → [inst : MulOneClass M] → Type ?u.20406
Monoid.End 
M: ?m.20400
M) (
n: ℕ
n : 
ℕ: Type
ℕ) : ⇑(
f: Monoid.End M
f ^ 
n: ℕ
n) = 
f: Monoid.End M
f^[
n: ℕ
n] :=
  
hom_coe_pow: ∀ {M : Type ?u.25127} {F : Type ?u.25126} [inst : Monoid F] (c : F → M → M),
  c 1 = _root_.id → (∀ (f g : F), c (f * g) = c f ∘ c g) → ∀ (f : F) (n : ℕ), c (f ^ n) = c f^[n]
hom_coe_pow 
_: ?m.25129 → ?m.25128 → ?m.25128
_ 
rfl: ∀ {α : Sort ?u.25132} {a : α}, a = a
rfl (fun 
_: ?m.25542
_ 
_: ?m.25545
_ => 
rfl: ∀ {α : Sort ?u.25547} {a : α}, a = a
rfl) 
_: ?m.25129
_ 
_: ℕ
_
#align monoid_hom.coe_pow 
MonoidHom.coe_pow: ∀ {M : Type u_1} [inst : CommMonoid M] (f : Monoid.End M) (n : ℕ), ↑(f ^ n) = ↑f^[n]
MonoidHom.coe_pow

end MonoidHom

theorem 
Monoid.End.coe_pow: ∀ {M : Type u_1} [inst : Monoid M] (f : Monoid.End M) (n : ℕ), ↑(f ^ n) = ↑f^[n]
Monoid.End.coe_pow {
M: ?m.25658
M} [
Monoid: Type ?u.25661 → Type ?u.25661
Monoid 
M: ?m.25658
M] (
f: Monoid.End M
f : 
Monoid.End: (M : Type ?u.25664) → [inst : MulOneClass M] → Type ?u.25664
Monoid.End 
M: ?m.25658
M) (
n: ℕ
n : 
ℕ: Type
ℕ) : ⇑(
f: Monoid.End M
f ^ 
n: ℕ
n) = 
f: Monoid.End M
f^[
n: ℕ
n] :=
  
hom_coe_pow: ∀ {M : Type ?u.30268} {F : Type ?u.30267} [inst : Monoid F] (c : F → M → M),
  c 1 = id → (∀ (f g : F), c (f * g) = c f ∘ c g) → ∀ (f : F) (n : ℕ), c (f ^ n) = c f^[n]
hom_coe_pow 
_: ?m.30270 → ?m.30269 → ?m.30269
_ 
rfl: ∀ {α : Sort ?u.30273} {a : α}, a = a
rfl (fun 
_: ?m.30683
_ 
_: ?m.30686
_ => 
rfl: ∀ {α : Sort ?u.30688} {a : α}, a = a
rfl) 
_: ?m.30270
_ 
_: ℕ
_
#align monoid.End.coe_pow 
Monoid.End.coe_pow: ∀ {M : Type u_1} [inst : Monoid M] (f : Monoid.End M) (n : ℕ), ↑(f ^ n) = ↑f^[n]
Monoid.End.coe_pow

-- we define these manually so that we can pick a better argument order
namespace AddMonoidHom

variable [
AddMonoid: Type ?u.32622 → Type ?u.32622
AddMonoid 
M: Type ?u.30805
M] [
AddGroup: Type ?u.32625 → Type ?u.32625
AddGroup 
G: Type ?u.30793
G]

theorem 
iterate_map_smul: ∀ (f : M →+ M) (n m : ℕ) (x : M), (↑f^[n]) (m • x) = m • (↑f^[n]) x
iterate_map_smul (
f: M →+ M
f : 
M: Type ?u.30805
M →+ 
M: Type ?u.30805
M) (
n: ℕ
n 
m: ℕ
m : 
ℕ: Type
ℕ) (
x: M
x : 
M: Type ?u.30805
M) : (
f: M →+ M
f^[
n: ℕ
n]) (
m: ℕ
m • 
x: M
x) = 
m: ℕ
m • (
f: M →+ M
f^[
n: ℕ
n]) 
x: M
x :=
  
f: M →+ M
f.
toMultiplicative: {α : Type ?u.32368} →
  {β : Type ?u.32367} →
    [inst : AddZeroClass α] → [inst_1 : AddZeroClass β] → (α →+ β) ≃ (Multiplicative α →* Multiplicative β)
toMultiplicative.
iterate_map_pow: ∀ {M : Type ?u.32501} [inst : Monoid M] (f : M →* M) (n : ℕ) (a : M) (m : ℕ), (↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
iterate_map_pow 
n: ℕ
n 
x: M
x 
m: ℕ
m
#align add_monoid_hom.iterate_map_smul 
AddMonoidHom.iterate_map_smul: ∀ {M : Type u_1} [inst : AddMonoid M] (f : M →+ M) (n m : ℕ) (x : M), (↑f^[n]) (m • x) = m • (↑f^[n]) x
AddMonoidHom.iterate_map_smul

attribute [
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] (f : M →+ M) (n m : ℕ) (a : M), (↑f^[n]) (m • a) = m • (↑f^[n]) a
to_additive (reorder := 5 6)] 
MonoidHom.iterate_map_pow: ∀ {M : Type u_1} [inst : Monoid M] (f : M →* M) (n : ℕ) (a : M) (m : ℕ), (↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
MonoidHom.iterate_map_pow
#align add_monoid_hom.iterate_map_nsmul 
AddMonoidHom.iterate_map_nsmul: ∀ {M : Type u_1} [inst : AddMonoid M] (f : M →+ M) (n m : ℕ) (a : M), (↑f^[n]) (m • a) = m • (↑f^[n]) a
AddMonoidHom.iterate_map_nsmul

theorem 
iterate_map_zsmul: ∀ (f : G →+ G) (n : ℕ) (m : ℤ) (x : G), (↑f^[n]) (m • x) = m • (↑f^[n]) x
iterate_map_zsmul (
f: G →+ G
f : 
G: Type ?u.32616
G →+ 
G: Type ?u.32616
G) (
n: ℕ
n : 
ℕ: Type
ℕ) (
m: ℤ
m : 
ℤ: Type
ℤ) (
x: G
x : 
G: Type ?u.32616
G) : (
f: G →+ G
f^[
n: ℕ
n]) (
m: ℤ
m • 
x: G
x) = 
m: ℤ
m • (
f: G →+ G
f^[
n: ℕ
n]) 
x: G
x :=
  
f: G →+ G
f.
toMultiplicative: {α : Type ?u.34381} →
  {β : Type ?u.34380} →
    [inst : AddZeroClass α] → [inst_1 : AddZeroClass β] → (α →+ β) ≃ (Multiplicative α →* Multiplicative β)
toMultiplicative.
iterate_map_zpow: ∀ {G : Type ?u.34712} [inst : Group G] (f : G →* G) (n : ℕ) (a : G) (m : ℤ), (↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
iterate_map_zpow 
n: ℕ
n 
x: G
x 
m: ℤ
m
#align add_monoid_hom.iterate_map_zsmul 
AddMonoidHom.iterate_map_zsmul: ∀ {G : Type u_1} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (m : ℤ) (x : G), (↑f^[n]) (m • x) = m • (↑f^[n]) x
AddMonoidHom.iterate_map_zsmul

attribute [
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (m : ℤ) (x : G), (↑f^[n]) (m • x) = m • (↑f^[n]) x
to_additive existing (reorder := 5 6)] 
MonoidHom.iterate_map_zpow: ∀ {G : Type u_1} [inst : Group G] (f : G →* G) (n : ℕ) (a : G) (m : ℤ), (↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
MonoidHom.iterate_map_zpow

end AddMonoidHom

theorem 
AddMonoid.End.coe_pow: ∀ {A : Type u_1} [inst : AddMonoid A] (f : AddMonoid.End A) (n : ℕ), ↑(f ^ n) = ↑f^[n]
AddMonoid.End.coe_pow {
A: Type u_1
A} [
AddMonoid: Type ?u.34797 → Type ?u.34797
AddMonoid 
A: ?m.34794
A] (
f: AddMonoid.End A
f : 
AddMonoid.End: (A : Type ?u.34800) → [inst : AddZeroClass A] → Type ?u.34800
AddMonoid.End 
A: ?m.34794
A) (
n: ℕ
n : 
ℕ: Type
ℕ) : ⇑(
f: AddMonoid.End A
f ^ 
n: ℕ
n) = 
f: AddMonoid.End A
f^[
n: ℕ
n] :=
  
hom_coe_pow: ∀ {M : Type ?u.39873} {F : Type ?u.39872} [inst : Monoid F] (c : F → M → M),
  c 1 = id → (∀ (f g : F), c (f * g) = c f ∘ c g) → ∀ (f : F) (n : ℕ), c (f ^ n) = c f^[n]
hom_coe_pow 
_: ?m.39875 → ?m.39874 → ?m.39874
_ 
rfl: ∀ {α : Sort ?u.39878} {a : α}, a = a
rfl (fun 
_: ?m.40288
_ 
_: ?m.40291
_ => 
rfl: ∀ {α : Sort ?u.40293} {a : α}, a = a
rfl) 
_: ?m.39875
_ 
_: ℕ
_
#align add_monoid.End.coe_pow 
AddMonoid.End.coe_pow: ∀ {A : Type u_1} [inst : AddMonoid A] (f : AddMonoid.End A) (n : ℕ), ↑(f ^ n) = ↑f^[n]
AddMonoid.End.coe_pow

namespace RingHom

section Semiring

variable {
R: Type ?u.45356
R : 
Type _: Type (?u.40406+1)
Type _} [
Semiring: Type ?u.40409 → Type ?u.40409
Semiring 
R: Type ?u.40451
R] (
f: R →+* R
f : 
R: Type ?u.40406
R →+* 
R: Type ?u.45356
R) (
n: ℕ
n : 
ℕ: Type
ℕ) (
x: R
x 
y: R
y : 
R: Type ?u.40406
R)

theorem 
coe_pow: ∀ {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ), ↑(f ^ n) = ↑f^[n]
coe_pow (
n: ℕ
n : 
ℕ: Type
ℕ) : ⇑(
f: R →+* R
f ^ 
n: ℕ
n) = 
f: R →+* R
f^[
n: ℕ
n] :=
  
hom_coe_pow: ∀ {M : Type ?u.44849} {F : Type ?u.44848} [inst : Monoid F] (c : F → M → M),
  c 1 = _root_.id → (∀ (f g : F), c (f * g) = c f ∘ c g) → ∀ (f : F) (n : ℕ), c (f ^ n) = c f^[n]
hom_coe_pow 
_: ?m.44851 → ?m.44850 → ?m.44850
_ 
rfl: ∀ {α : Sort ?u.44854} {a : α}, a = a
rfl (fun 
_: ?m.45264
_ 
_: ?m.45267
_ => 
rfl: ∀ {α : Sort ?u.45269} {a : α}, a = a
rfl) 
f: R →+* R
f 
n: ℕ
n
#align ring_hom.coe_pow 
RingHom.coe_pow: ∀ {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ), ↑(f ^ n) = ↑f^[n]
RingHom.coe_pow

theorem 
iterate_map_one: (↑f^[n]) 1 = 1
iterate_map_one : (
f: R →+* R
f^[
n: ℕ
n]) 
1: ?m.45728
1 = 
1: ?m.45765
1 :=
  
f: R →+* R
f.
toMonoidHom: {α : Type ?u.45783} →
  {β : Type ?u.45782} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →* β
toMonoidHom.
iterate_map_one: ∀ {M : Type ?u.45807} [inst : MulOneClass M] (f : M →* M) (n : ℕ), (↑f^[n]) 1 = 1
iterate_map_one 
n: ℕ
n
#align ring_hom.iterate_map_one 
RingHom.iterate_map_one: ∀ {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ), (↑f^[n]) 1 = 1
RingHom.iterate_map_one

theorem 
iterate_map_zero: (↑f^[n]) 0 = 0
iterate_map_zero : (
f: R →+* R
f^[
n: ℕ
n]) 
0: ?m.46237
0 = 
0: ?m.46369
0 :=
  
f: R →+* R
f.
toAddMonoidHom: {α : Type ?u.46387} →
  {β : Type ?u.46386} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →+ β
toAddMonoidHom.
iterate_map_zero: ∀ {M : Type ?u.46411} [inst : AddZeroClass M] (f : M →+ M) (n : ℕ), (↑f^[n]) 0 = 0
iterate_map_zero 
n: ℕ
n
#align ring_hom.iterate_map_zero 
RingHom.iterate_map_zero: ∀ {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ), (↑f^[n]) 0 = 0
RingHom.iterate_map_zero

theorem 
iterate_map_add: (↑f^[n]) (x + y) = (↑f^[n]) x + (↑f^[n]) y
iterate_map_add : (
f: R →+* R
f^[
n: ℕ
n]) (
x: R
x + 
y: R
y) = (
f: R →+* R
f^[
n: ℕ
n]) 
x: R
x + (
f: R →+* R
f^[
n: ℕ
n]) 
y: R
y :=
  
f: R →+* R
f.
toAddMonoidHom: {α : Type ?u.47887} →
  {β : Type ?u.47886} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →+ β
toAddMonoidHom.
iterate_map_add: ∀ {M : Type ?u.47911} [inst : AddZeroClass M] (f : M →+ M) (n : ℕ) (x y : M), (↑f^[n]) (x + y) = (↑f^[n]) x + (↑f^[n]) y
iterate_map_add 
n: ℕ
n 
x: R
x 
y: R
y
#align ring_hom.iterate_map_add 
RingHom.iterate_map_add: ∀ {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ) (x y : R), (↑f^[n]) (x + y) = (↑f^[n]) x + (↑f^[n]) y
RingHom.iterate_map_add

theorem 
iterate_map_mul: (↑f^[n]) (x * y) = (↑f^[n]) x * (↑f^[n]) y
iterate_map_mul : (
f: R →+* R
f^[
n: ℕ
n]) (
x: R
x * 
y: R
y) = (
f: R →+* R
f^[
n: ℕ
n]) 
x: R
x * (
f: R →+* R
f^[
n: ℕ
n]) 
y: R
y :=
  
f: R →+* R
f.
toMonoidHom: {α : Type ?u.49407} →
  {β : Type ?u.49406} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →* β
toMonoidHom.
iterate_map_mul: ∀ {M : Type ?u.49431} [inst : MulOneClass M] (f : M →* M) (n : ℕ) (x y : M), (↑f^[n]) (x * y) = (↑f^[n]) x * (↑f^[n]) y
iterate_map_mul 
n: ℕ
n 
x: R
x 
y: R
y
#align ring_hom.iterate_map_mul 
RingHom.iterate_map_mul: ∀ {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ) (x y : R), (↑f^[n]) (x * y) = (↑f^[n]) x * (↑f^[n]) y
RingHom.iterate_map_mul

theorem 
iterate_map_pow: ∀ (a : R) (n m : ℕ), (↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
iterate_map_pow (
a: ?m.49530
a) (
n: ℕ
n 
m: ℕ
m : 
ℕ: Type
ℕ) : (
f: R →+* R
f^[
n: ℕ
n]) (
a: ?m.49530
a ^ 
m: ℕ
m) = (
f: R →+* R
f^[
n: ℕ
n]) 
a: ?m.49530
a ^ 
m: ℕ
m :=
  
f: R →+* R
f.
toMonoidHom: {α : Type ?u.50418} →
  {β : Type ?u.50417} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →* β
toMonoidHom.
iterate_map_pow: ∀ {M : Type ?u.50442} [inst : Monoid M] (f : M →* M) (n : ℕ) (a : M) (m : ℕ), (↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
iterate_map_pow 
n: ℕ
n 
a: R
a 
m: ℕ
m
#align ring_hom.iterate_map_pow 
RingHom.iterate_map_pow: ∀ {R : Type u_1} [inst : Semiring R] (f : R →+* R) (a : R) (n m : ℕ), (↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
RingHom.iterate_map_pow

theorem 
iterate_map_smul: ∀ (n m : ℕ) (x : R), (↑f^[n]) (m • x) = m • (↑f^[n]) x
iterate_map_smul (
n: ℕ
n 
m: ℕ
m : 
ℕ: Type
ℕ) (
x: R
x : 
R: Type ?u.50517
R) : (
f: R →+* R
f^[
n: ℕ
n]) (
m: ℕ
m • 
x: R
x) = 
m: ℕ
m • (
f: R →+* R
f^[
n: ℕ
n]) 
x: R
x :=
  
f: R →+* R
f.
toAddMonoidHom: {α : Type ?u.51468} →
  {β : Type ?u.51467} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →+ β
toAddMonoidHom.
iterate_map_smul: ∀ {M : Type ?u.51492} [inst : AddMonoid M] (f : M →+ M) (n m : ℕ) (x : M), (↑f^[n]) (m • x) = m • (↑f^[n]) x
iterate_map_smul 
n: ℕ
n 
m: ℕ
m 
x: R
x
#align ring_hom.iterate_map_smul 
RingHom.iterate_map_smul: ∀ {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n m : ℕ) (x : R), (↑f^[n]) (m • x) = m • (↑f^[n]) x
RingHom.iterate_map_smul

end Semiring

variable {
R: Type ?u.51640
R : 
Type _: Type (?u.53234+1)
Type _} [
Ring: Type ?u.53237 → Type ?u.53237
Ring 
R: Type ?u.51805
R] (
f: R →+* R
f : 
R: Type ?u.51640
R →+* 
R: Type ?u.51640
R) (
n: ℕ
n : 
ℕ: Type
ℕ) (
x: R
x 
y: R
y : 
R: Type ?u.51640
R)

theorem 
iterate_map_sub: (↑f^[n]) (x - y) = (↑f^[n]) x - (↑f^[n]) y
iterate_map_sub : (
f: R →+* R
f^[
n: ℕ
n]) (
x: R
x - 
y: R
y) = (
f: R →+* R
f^[
n: ℕ
n]) 
x: R
x - (
f: R →+* R
f^[
n: ℕ
n]) 
y: R
y :=
  
f: R →+* R
f.
toAddMonoidHom: {α : Type ?u.53029} →
  {β : Type ?u.53028} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →+ β
toAddMonoidHom.
iterate_map_sub: ∀ {G : Type ?u.53173} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (x y : G), (↑f^[n]) (x - y) = (↑f^[n]) x - (↑f^[n]) y
iterate_map_sub 
n: ℕ
n 
x: R
x 
y: R
y
#align ring_hom.iterate_map_sub 
RingHom.iterate_map_sub: ∀ {R : Type u_1} [inst : Ring R] (f : R →+* R) (n : ℕ) (x y : R), (↑f^[n]) (x - y) = (↑f^[n]) x - (↑f^[n]) y
RingHom.iterate_map_sub

theorem 
iterate_map_neg: ∀ {R : Type u_1} [inst : Ring R] (f : R →+* R) (n : ℕ) (x : R), (↑f^[n]) (-x) = -(↑f^[n]) x
iterate_map_neg : (
f: R →+* R
f^[
n: ℕ
n]) (-
x: R
x) = -(
f: R →+* R
f^[
n: ℕ
n]) 
x: R
x :=
  
f: R →+* R
f.
toAddMonoidHom: {α : Type ?u.54072} →
  {β : Type ?u.54071} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →+ β
toAddMonoidHom.
iterate_map_neg: ∀ {G : Type ?u.54216} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (x : G), (↑f^[n]) (-x) = -(↑f^[n]) x
iterate_map_neg 
n: ℕ
n 
x: R
x
#align ring_hom.iterate_map_neg 
RingHom.iterate_map_neg: ∀ {R : Type u_1} [inst : Ring R] (f : R →+* R) (n : ℕ) (x : R), (↑f^[n]) (-x) = -(↑f^[n]) x
RingHom.iterate_map_neg

theorem 
iterate_map_zsmul: ∀ (n : ℕ) (m : ℤ) (x : R), (↑f^[n]) (m • x) = m • (↑f^[n]) x
iterate_map_zsmul (
n: ℕ
n : 
ℕ: Type
ℕ) (
m: ℤ
m : 
ℤ: Type
ℤ) (
x: R
x : 
R: Type ?u.54273
R) : (
f: R →+* R
f^[
n: ℕ
n]) (
m: ℤ
m • 
x: R
x) = 
m: ℤ
m • (
f: R →+* R
f^[
n: ℕ
n]) 
x: R
x :=
  
f: R →+* R
f.
toAddMonoidHom: {α : Type ?u.55207} →
  {β : Type ?u.55206} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →+ β
toAddMonoidHom.
iterate_map_zsmul: ∀ {G : Type ?u.55351} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (m : ℤ) (x : G), (↑f^[n]) (m • x) = m • (↑f^[n]) x
iterate_map_zsmul 
n: ℕ
n 
m: ℤ
m 
x: R
x
#align ring_hom.iterate_map_zsmul 
RingHom.iterate_map_zsmul: ∀ {R : Type u_1} [inst : Ring R] (f : R →+* R) (n : ℕ) (m : ℤ) (x : R), (↑f^[n]) (m • x) = m • (↑f^[n]) x
RingHom.iterate_map_zsmul

end RingHom

--what should be the namespace for this section?
section Monoid

variable [
Monoid: Type ?u.59884 → Type ?u.59884
Monoid 
G: Type ?u.55404
G] (
a: G
a : 
G: Type ?u.55423
G) (
n: ℕ
n : 
ℕ: Type
ℕ)

@[
to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] (a : G) (n : ℕ) [inst_1 : AddAction G H],
  (fun x => a +ᵥ x)^[n] = fun x => n • a +ᵥ x
to_additive (attr := simp)]
theorem 
smul_iterate: ∀ [inst : MulAction G H], (fun x => a • x)^[n] = fun x => a ^ n • x
smul_iterate [
MulAction: (α : Type ?u.55437) → Type ?u.55436 → [inst : Monoid α] → Type (max?u.55437?u.55436)
MulAction 
G: Type ?u.55423
G 
H: Type ?u.55426
H] : (
a: G
a • · : 
H: Type ?u.55426
H → 
H: Type ?u.55426
H)^[
n: ℕ
n] = (
a: G
a ^ 
n: ℕ
n • ·) :=
  
funext: ∀ {α : Sort ?u.59360} {β : α → Sort ?u.59359} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun 
b: ?m.59375
b =>
    
Nat.recOn: ∀ {motive : ℕ → Sort ?u.59377} (t : ℕ), motive Nat.zero → (∀ (n : ℕ), motive n → motive (Nat.succ n)) → motive t
Nat.recOn 
n: ℕ
n (by
Goals accomplished! 🐙 
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n: ℕ

inst✝: MulAction G H

b: H

((fun x => a • x)^[Nat.zero]) b = a ^ Nat.zero • brw [
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n: ℕ

inst✝: MulAction G H

b: H

((fun x => a • x)^[Nat.zero]) b = a ^ Nat.zero • b
iterate_zero: ∀ {α : Type ?u.59415} (f : α → α), f^[0] = id
iterate_zero,
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n: ℕ

inst✝: MulAction G H

b: H

id b = a ^ Nat.zero • b 
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n: ℕ

inst✝: MulAction G H

b: H

((fun x => a • x)^[Nat.zero]) b = a ^ Nat.zero • b
id.def: ∀ {α : Sort ?u.59432} (a : α), id a = a
id.def,
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n: ℕ

inst✝: MulAction G H

b: H

b = a ^ Nat.zero • b 
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n: ℕ

inst✝: MulAction G H

b: H

((fun x => a • x)^[Nat.zero]) b = a ^ Nat.zero • b
pow_zero: ∀ {M : Type ?u.59441} [inst : Monoid M] (a : M), a ^ 0 = 1
pow_zero,
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n: ℕ

inst✝: MulAction G H

b: H

b = 1 • b 
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n: ℕ

inst✝: MulAction G H

b: H

((fun x => a • x)^[Nat.zero]) b = a ^ Nat.zero • b
one_smul: ∀ (M : Type ?u.59501) {α : Type ?u.59500} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = b
one_smul
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n: ℕ

inst✝: MulAction G H

b: H

b = b]
Goals accomplished! 🐙)
    fun 
n: ?m.59406
n 
ih: ?m.59409
ih => by
Goals accomplished! 🐙 
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n✝: ℕ

inst✝: MulAction G H

b: H

n: ℕ

ih: ((fun x => a • x)^[n]) b = a ^ n • b

((fun x => a • x)^[Nat.succ n]) b = a ^ Nat.succ n • brw [
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n✝: ℕ

inst✝: MulAction G H

b: H

n: ℕ

ih: ((fun x => a • x)^[n]) b = a ^ n • b

((fun x => a • x)^[Nat.succ n]) b = a ^ Nat.succ n • b
iterate_succ': ∀ {α : Type ?u.59539} (f : α → α) (n : ℕ), f^[Nat.succ n] = f ∘ f^[n]
iterate_succ',
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n✝: ℕ

inst✝: MulAction G H

b: H

n: ℕ

ih: ((fun x => a • x)^[n]) b = a ^ n • b

((fun x => a • x) ∘ (fun x => a • x)^[n]) b = a ^ Nat.succ n • b 
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n✝: ℕ

inst✝: MulAction G H

b: H

n: ℕ

ih: ((fun x => a • x)^[n]) b = a ^ n • b

((fun x => a • x)^[Nat.succ n]) b = a ^ Nat.succ n • b
comp_apply: ∀ {β : Sort ?u.59553} {δ : Sort ?u.59554} {α : Sort ?u.59555} {f : β → δ} {g : α → β} {x : α}, (f ∘ g) x = f (g x)
comp_apply,
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n✝: ℕ

inst✝: MulAction G H

b: H

n: ℕ

ih: ((fun x => a • x)^[n]) b = a ^ n • b

a • ((fun x => a • x)^[n]) b = a ^ Nat.succ n • b 
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n✝: ℕ

inst✝: MulAction G H

b: H

n: ℕ

ih: ((fun x => a • x)^[n]) b = a ^ n • b

((fun x => a • x)^[Nat.succ n]) b = a ^ Nat.succ n • b
ih: ((fun x => a • x)^[n]) b = a ^ n • b
ih,
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n✝: ℕ

inst✝: MulAction G H

b: H

n: ℕ

ih: ((fun x => a • x)^[n]) b = a ^ n • b

a • a ^ n • b = a ^ Nat.succ n • b 
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n✝: ℕ

inst✝: MulAction G H

b: H

n: ℕ

ih: ((fun x => a • x)^[n]) b = a ^ n • b

((fun x => a • x)^[Nat.succ n]) b = a ^ Nat.succ n • b
pow_succ: ∀ {M : Type ?u.59580} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
pow_succ,
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n✝: ℕ

inst✝: MulAction G H

b: H

n: ℕ

ih: ((fun x => a • x)^[n]) b = a ^ n • b

a • a ^ n • b = (a * a ^ n) • b 
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n✝: ℕ

inst✝: MulAction G H

b: H

n: ℕ

ih: ((fun x => a • x)^[n]) b = a ^ n • b

((fun x => a • x)^[Nat.succ n]) b = a ^ Nat.succ n • b
mul_smul: ∀ {α : Type ?u.59636} {β : Type ?u.59635} [inst : Monoid α] [self : MulAction α β] (x y : α) (b : β),
  (x * y) • b = x • y • b
mul_smul
M: Type ?u.55417

N: Type ?u.55420

G: Type u_1

H: Type u_2

inst✝¹: Monoid G

a: G

n✝: ℕ

inst✝: MulAction G H

b: H

n: ℕ

ih: ((fun x => a • x)^[n]) b = a ^ n • b

a • a ^ n • b = a • a ^ n • b]
Goals accomplished! 🐙
#align smul_iterate 
smul_iterate: ∀ {G : Type u_1} {H : Type u_2} [inst : Monoid G] (a : G) (n : ℕ) [inst_1 : MulAction G H],
  (fun x => a • x)^[n] = fun x => a ^ n • x
smul_iterate
#align vadd_iterate 
vadd_iterate: ∀ {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] (a : G) (n : ℕ) [inst_1 : AddAction G H],
  (fun x => a +ᵥ x)^[n] = fun x => n • a +ᵥ x
vadd_iterate

@[
to_additive: ∀ {G : Type u_1} [inst : AddMonoid G] (a : G) (n : ℕ), (fun x => a + x)^[n] = fun x => n • a + x
to_additive (attr := simp)]
theorem 
mul_left_iterate: (fun x => a * x)^[n] = fun x => a ^ n * x
mul_left_iterate : (
a: G
a * ·)^[
n: ℕ
n] = (
a: G
a ^ 
n: ℕ
n * ·) :=
  
smul_iterate: ∀ {G : Type ?u.63109} {H : Type ?u.63110} [inst : Monoid G] (a : G) (n : ℕ) [inst_1 : MulAction G H],
  (fun x => a • x)^[n] = fun x => a ^ n • x
smul_iterate 
a: G
a 
n: ℕ
n
#align mul_left_iterate 
mul_left_iterate: ∀ {G : Type u_1} [inst : Monoid G] (a : G) (n : ℕ), (fun x => a * x)^[n] = fun x => a ^ n * x
mul_left_iterate
#align add_left_iterate 
add_left_iterate: ∀ {G : Type u_1} [inst : AddMonoid G] (a : G) (n : ℕ), (fun x => a + x)^[n] = fun x => n • a + x
add_left_iterate

@[
to_additive: ∀ {G : Type u_1} [inst : AddMonoid G] (a : G) (n : ℕ), (fun x => x + a)^[n] = fun x => x + n • a
to_additive (attr := simp)]
theorem 
mul_right_iterate: (fun x => x * a)^[n] = fun x => x * a ^ n
mul_right_iterate : (· * 
a: G
a)^[
n: ℕ
n] = (· * 
a: G
a ^ 
n: ℕ
n) :=
  
smul_iterate: ∀ {G : Type ?u.67134} {H : Type ?u.67135} [inst : Monoid G] (a : G) (n : ℕ) [inst_1 : MulAction G H],
  (fun x => a • x)^[n] = fun x => a ^ n • x
smul_iterate (
MulOpposite.op: {α : Type ?u.67139} → α → αᵐᵒᵖ
MulOpposite.op 
a: G
a) 
n: ℕ
n
#align mul_right_iterate 
mul_right_iterate: ∀ {G : Type u_1} [inst : Monoid G] (a : G) (n : ℕ), (fun x => x * a)^[n] = fun x => x * a ^ n
mul_right_iterate
#align add_right_iterate 
add_right_iterate: ∀ {G : Type u_1} [inst : AddMonoid G] (a : G) (n : ℕ), (fun x => x + a)^[n] = fun x => x + n • a
add_right_iterate

@[
to_additive: ∀ {G : Type u_1} [inst : AddMonoid G] (a : G) (n : ℕ), ((fun x => x + a)^[n]) 0 = n • a
to_additive]
theorem 
mul_right_iterate_apply_one: ((fun x => x * a)^[n]) 1 = a ^ n
mul_right_iterate_apply_one : ((· * 
a: G
a)^[
n: ℕ
n]) 
1: ?m.67892
1 = 
a: G
a ^ 
n: ℕ
n := by
Goals accomplished! 🐙 
M: Type ?u.67258

N: Type ?u.67261

G: Type u_1

H: Type ?u.67267

inst✝: Monoid G

a: G

n: ℕ

((fun x => x * a)^[n]) 1 = a ^ nsimp [
mul_right_iterate: ∀ {G : Type ?u.70709} [inst : Monoid G] (a : G) (n : ℕ), (fun x => x * a)^[n] = fun x => x * a ^ n
mul_right_iterate]
Goals accomplished! 🐙
#align mul_right_iterate_apply_one 
mul_right_iterate_apply_one: ∀ {G : Type u_1} [inst : Monoid G] (a : G) (n : ℕ), ((fun x => x * a)^[n]) 1 = a ^ n
mul_right_iterate_apply_one
#align add_right_iterate_apply_zero 
add_right_iterate_apply_zero: ∀ {G : Type u_1} [inst : AddMonoid G] (a : G) (n : ℕ), ((fun x => x + a)^[n]) 0 = n • a
add_right_iterate_apply_zero

@[
to_additive: ∀ {G : Type u_1} [inst : AddMonoid G] (n j : ℕ), (fun x => n • x)^[j] = fun x => n ^ j • x
to_additive (attr := simp)]
theorem 
pow_iterate: ∀ (n j : ℕ), (fun x => x ^ n)^[j] = fun x => x ^ n ^ j
pow_iterate (
n: ℕ
n : 
ℕ: Type
ℕ) (
j: ℕ
j : 
ℕ: Type
ℕ) : (fun 
x: G
x : 
G: Type ?u.71290
G => 
x: G
x ^ 
n: ℕ
n)^[
j: ℕ
j] = fun 
x: G
x : 
G: Type ?u.71290
G => 
x: G
x ^ 
n: ℕ
n ^ 
j: ℕ
j :=
  letI : 
MulAction: (α : Type ?u.76351) → Type ?u.76350 → [inst : Monoid α] → Type (max?u.76351?u.76350)
MulAction 
ℕ: Type
ℕ 
G: Type ?u.71290
G :=
    { smul := fun 
n: ?m.76376
n 
g: ?m.76379
g => 
g: ?m.76379
g ^ 
n: ?m.76376
n
      one_smul := 
pow_one: ∀ {M : Type ?u.78906} [inst : Monoid M] (a : M), a ^ 1 = a
pow_one
      mul_smul := fun 
m: ?m.78952
m 
n: ?m.78955
n 
g: ?m.78958
g => 
pow_mul': ∀ {M : Type ?u.78960} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ n) ^ m
pow_mul' 
g: ?m.78958
g 
m: ?m.78952
m 
n: ?m.78955
n }
  
smul_iterate: ∀ {G : Type ?u.78970} {H : Type ?u.78971} [inst : Monoid G] (a : G) (n : ℕ) [inst_1 : MulAction G H],
  (fun x => a • x)^[n] = fun x => a ^ n • x
smul_iterate 
n: ℕ
n 
j: ℕ
j
#align pow_iterate 
pow_iterate: ∀ {G : Type u_1} [inst : Monoid G] (n j : ℕ), (fun x => x ^ n)^[j] = fun x => x ^ n ^ j
pow_iterate
#align nsmul_iterate 
nsmul_iterate: ∀ {G : Type u_1} [inst : AddMonoid G] (n j : ℕ), (fun x => n • x)^[j] = fun x => n ^ j • x
nsmul_iterate

end Monoid

section Group

variable [
Group: Type ?u.79093 → Type ?u.79093
Group 
G: Type ?u.79087
G]

@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] (n : ℤ) (j : ℕ), (fun x => n • x)^[j] = fun x => n ^ j • x
to_additive (attr := simp)]
theorem 
zpow_iterate: ∀ (n : ℤ) (j : ℕ), (fun x => x ^ n)^[j] = fun x => x ^ n ^ j
zpow_iterate (
n: ℤ
n : 
ℤ: Type
ℤ) (
j: ℕ
j : 
ℕ: Type
ℕ) : (fun 
x: G
x : 
G: Type ?u.79102
G => 
x: G
x ^ 
n: ℤ
n)^[
j: ℕ
j] = fun 
x: ?m.81762
x => 
x: ?m.81762
x ^ 
n: ℤ
n ^ 
j: ℕ
j :=
  letI : 
MulAction: (α : Type ?u.82077) → Type ?u.82076 → [inst : Monoid α] → Type (max?u.82077?u.82076)
MulAction 
ℤ: Type
ℤ 
G: Type ?u.79102
G :=
    { smul := fun 
n: ?m.82101
n 
g: ?m.82104
g => 
g: ?m.82104
g ^ 
n: ?m.82101
n
      one_smul := 
zpow_one: ∀ {G : Type ?u.84696} [inst : DivInvMonoid G] (a : G), a ^ 1 = a
zpow_one
      mul_smul := fun 
m: ?m.84749
m 
n: ?m.84752
n 
g: ?m.84755
g => 
zpow_mul': ∀ {α : Type ?u.84757} [inst : DivisionMonoid α] (a : α) (m n : ℤ), a ^ (m * n) = (a ^ n) ^ m
zpow_mul' 
g: ?m.84755
g 
m: ?m.84749
m 
n: ?m.84752
n }
  
smul_iterate: ∀ {G : Type ?u.84806} {H : Type ?u.84807} [inst : Monoid G] (a : G) (n : ℕ) [inst_1 : MulAction G H],
  (fun x => a • x)^[n] = fun x => a ^ n • x
smul_iterate 
n: ℤ
n 
j: ℕ
j
#align zpow_iterate 
zpow_iterate: ∀ {G : Type u_1} [inst : Group G] (n : ℤ) (j : ℕ), (fun x => x ^ n)^[j] = fun x => x ^ n ^ j
zpow_iterate
#align zsmul_iterate 
zsmul_iterate: ∀ {G : Type u_1} [inst : AddGroup G] (n : ℤ) (j : ℕ), (fun x => n • x)^[j] = fun x => n ^ j • x
zsmul_iterate

end Group

section Semigroup

variable [
Semigroup: Type ?u.89663 → Type ?u.89663
Semigroup 
G: Type ?u.87808
G] {
a: G
a 
b: G
b 
c: G
c : 
G: Type ?u.84944
G}

-- Porting note: need `dsimp only`, see https://leanprover.zulipchat.com/#narrow/stream/
-- 287929-mathlib4/topic/dsimp.20before.20rw/near/317063489
@[
to_additive: ∀ {G : Type u_1} [inst : AddSemigroup G] {a b c : G},
  AddSemiconjBy a b c → Semiconj (fun x => a + x) (fun x => b + x) fun x => c + x
to_additive]
theorem 
SemiconjBy.function_semiconj_mul_left: ∀ {G : Type u_1} [inst : Semigroup G] {a b c : G},
  SemiconjBy a b c → Semiconj (fun x => a * x) (fun x => b * x) fun x => c * x
SemiconjBy.function_semiconj_mul_left (
h: SemiconjBy a b c
h : 
SemiconjBy: {M : Type ?u.84959} → [inst : Mul M] → M → M → M → Prop
SemiconjBy 
a: G
a 
b: G
b 
c: G
c) :
    
Function.Semiconj: {α : Type ?u.85486} → {β : Type ?u.85485} → (α → β) → (α → α) → (β → β) → Prop
Function.Semiconj (
a: G
a * ·) (
b: G
b * ·) (
c: G
c * ·) := fun 
j: ?m.87126
j => by
Goals accomplished! 🐙
  
M: Type ?u.84938

N: Type ?u.84941

G: Type u_1

H: Type ?u.84947

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

(fun x => a * x) ((fun x => b * x) j) = (fun x => c * x) ((fun x => a * x) j)dsimp only
M: Type ?u.84938

N: Type ?u.84941

G: Type u_1

H: Type ?u.84947

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

a * (b * j) = c * (a * j);
M: Type ?u.84938

N: Type ?u.84941

G: Type u_1

H: Type ?u.84947

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

a * (b * j) = c * (a * j) 
M: Type ?u.84938

N: Type ?u.84941

G: Type u_1

H: Type ?u.84947

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

(fun x => a * x) ((fun x => b * x) j) = (fun x => c * x) ((fun x => a * x) j)rw [
M: Type ?u.84938

N: Type ?u.84941

G: Type u_1

H: Type ?u.84947

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

a * (b * j) = c * (a * j)← 
mul_assoc: ∀ {G : Type ?u.87153} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc,
M: Type ?u.84938

N: Type ?u.84941

G: Type u_1

H: Type ?u.84947

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

a * b * j = c * (a * j) 
M: Type ?u.84938

N: Type ?u.84941

G: Type u_1

H: Type ?u.84947

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

a * (b * j) = c * (a * j)
h: SemiconjBy a b c
h.
eq: ∀ {S : Type ?u.87196} [inst : Mul S] {a x y : S}, SemiconjBy a x y → a * x = y * a
eq,
M: Type ?u.84938

N: Type ?u.84941

G: Type u_1

H: Type ?u.84947

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

c * a * j = c * (a * j) 
M: Type ?u.84938

N: Type ?u.84941

G: Type u_1

H: Type ?u.84947

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

a * (b * j) = c * (a * j)
mul_assoc: ∀ {G : Type ?u.87713} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc
M: Type ?u.84938

N: Type ?u.84941

G: Type u_1

H: Type ?u.84947

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

c * (a * j) = c * (a * j)]
Goals accomplished! 🐙
#align semiconj_by.function_semiconj_mul_left 
SemiconjBy.function_semiconj_mul_left: ∀ {G : Type u_1} [inst : Semigroup G] {a b c : G},
  SemiconjBy a b c → Semiconj (fun x => a * x) (fun x => b * x) fun x => c * x
SemiconjBy.function_semiconj_mul_left
#align add_semiconj_by.function_semiconj_add_left 
AddSemiconjBy.function_semiconj_add_left: ∀ {G : Type u_1} [inst : AddSemigroup G] {a b c : G},
  AddSemiconjBy a b c → Semiconj (fun x => a + x) (fun x => b + x) fun x => c + x
AddSemiconjBy.function_semiconj_add_left

@[
to_additive: ∀ {G : Type u_1} [inst : AddSemigroup G] {a b : G}, AddCommute a b → Function.Commute (fun x => a + x) fun x => b + x
to_additive]
theorem 
Commute.function_commute_mul_left: ∀ {G : Type u_1} [inst : Semigroup G] {a b : G}, _root_.Commute a b → Function.Commute (fun x => a * x) fun x => b * x
Commute.function_commute_mul_left (
h: _root_.Commute a b
h : 
_root_.Commute: {S : Type ?u.87823} → [inst : Mul S] → S → S → Prop
_root_.Commute 
a: G
a 
b: G
b) :
    
Function.Commute: {α : Type ?u.88349} → (α → α) → (α → α) → Prop
Function.Commute (
a: G
a * ·) (
b: G
b * ·) :=
  
SemiconjBy.function_semiconj_mul_left: ∀ {G : Type ?u.89575} [inst : Semigroup G] {a b c : G},
  SemiconjBy a b c → Semiconj (fun x => a * x) (fun x => b * x) fun x => c * x
SemiconjBy.function_semiconj_mul_left 
h: _root_.Commute a b
h
#align commute.function_commute_mul_left 
Commute.function_commute_mul_left: ∀ {G : Type u_1} [inst : Semigroup G] {a b : G}, _root_.Commute a b → Function.Commute (fun x => a * x) fun x => b * x
Commute.function_commute_mul_left
#align add_commute.function_commute_add_left 
AddCommute.function_commute_add_left: ∀ {G : Type u_1} [inst : AddSemigroup G] {a b : G}, AddCommute a b → Function.Commute (fun x => a + x) fun x => b + x
AddCommute.function_commute_add_left

@[
to_additive: ∀ {G : Type u_1} [inst : AddSemigroup G] {a b c : G},
  AddSemiconjBy a b c → Semiconj (fun x => x + a) (fun x => x + c) fun x => x + b
to_additive]
theorem 
SemiconjBy.function_semiconj_mul_right_swap: SemiconjBy a b c → Semiconj (fun x => x * a) (fun x => x * c) fun x => x * b
SemiconjBy.function_semiconj_mul_right_swap (
h: SemiconjBy a b c
h : 
SemiconjBy: {M : Type ?u.89672} → [inst : Mul M] → M → M → M → Prop
SemiconjBy 
a: G
a 
b: G
b 
c: G
c) :
    
Function.Semiconj: {α : Type ?u.90199} → {β : Type ?u.90198} → (α → β) → (α → α) → (β → β) → Prop
Function.Semiconj (· * 
a: G
a) (· * 
c: G
c) (· * 
b: G
b) := fun 
j: ?m.91839
j => by
Goals accomplished! 🐙 
M: Type ?u.89651

N: Type ?u.89654

G: Type u_1

H: Type ?u.89660

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

(fun x => x * a) ((fun x => x * c) j) = (fun x => x * b) ((fun x => x * a) j)simp_rw [
M: Type ?u.89651

N: Type ?u.89654

G: Type u_1

H: Type ?u.89660

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

j * c * a = j * a * b
mul_assoc: ∀ {G : Type ?u.91917} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc,
M: Type ?u.89651

N: Type ?u.89654

G: Type u_1

H: Type ?u.89660

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

j * (c * a) = j * (a * b) 
M: Type ?u.89651

N: Type ?u.89654

G: Type u_1

H: Type ?u.89660

inst✝: Semigroup G

a, b, c: G

h: SemiconjBy a b c

j: G

(fun x => x * a) ((fun x => x * c) j) = (fun x => x * b) ((fun x => x * a) j)← 
h: SemiconjBy a b c
h.
eq: ∀ {S : Type ?u.91982} [inst : Mul S] {a x y : S}, SemiconjBy a x y → a * x = y * a
eq
Goals accomplished! 🐙]
Goals accomplished! 🐙
#align semiconj_by.function_semiconj_mul_right_swap 
SemiconjBy.function_semiconj_mul_right_swap: ∀ {G : Type u_1} [inst : Semigroup G] {a b c : G},
  SemiconjBy a b c → Semiconj (fun x => x * a) (fun x => x * c) fun x => x * b
SemiconjBy.function_semiconj_mul_right_swap
#align add_semiconj_by.function_semiconj_add_right_swap 
AddSemiconjBy.function_semiconj_add_right_swap: ∀ {G : Type u_1} [inst : AddSemigroup G] {a b c : G},
  AddSemiconjBy a b c → Semiconj (fun x => x + a) (fun x => x + c) fun x => x + b
AddSemiconjBy.function_semiconj_add_right_swap

@[
to_additive: ∀ {G : Type u_1} [inst : AddSemigroup G] {a b : G}, AddCommute a b → Function.Commute (fun x => x + a) fun x => x + b
to_additive]
theorem 
Commute.function_commute_mul_right: ∀ {G : Type u_1} [inst : Semigroup G] {a b : G}, _root_.Commute a b → Function.Commute (fun x => x * a) fun x => x * b
Commute.function_commute_mul_right (
h: _root_.Commute a b
h : 
_root_.Commute: {S : Type ?u.92576} → [inst : Mul S] → S → S → Prop
_root_.Commute 
a: G
a 
b: G
b) :
  
Function.Commute: {α : Type ?u.93102} → (α → α) → (α → α) → Prop
Function.Commute (· * 
a: G
a) (· * 
b: G
b) :=
  
SemiconjBy.function_semiconj_mul_right_swap: ∀ {G : Type ?u.94328} [inst : Semigroup G] {a b c : G},
  SemiconjBy a b c → Semiconj (fun x => x * a) (fun x => x * c) fun x => x * b
SemiconjBy.function_semiconj_mul_right_swap 
h: _root_.Commute a b
h
#align commute.function_commute_mul_right 
Commute.function_commute_mul_right: ∀ {G : Type u_1} [inst : Semigroup G] {a b : G}, _root_.Commute a b → Function.Commute (fun x => x * a) fun x => x * b
Commute.function_commute_mul_right
#align add_commute.function_commute_add_right 
AddCommute.function_commute_add_right: ∀ {G : Type u_1} [inst : AddSemigroup G] {a b : G}, AddCommute a b → Function.Commute (fun x => x + a) fun x => x + b
AddCommute.function_commute_add_right

end Semigroup