α : Type ?u.27674
M✝ : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
M : Type u_1
inst✝ : Monoid M
x : M
m n : ℕ
h : x ^ n = 1
t : x ^ m = x ^ (n * (m / n) + m % n)
⊢ x ^ m = x ^ (m % n)
α : Type ?u.27674
M✝ : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
M : Type u_1
inst✝ : Monoid M
x : M
m n : ℕ
h : x ^ n = 1
⊢ x ^ m = x ^ (m % n)
have t : x ^ m = x ^ (n * (m / n) + m % n) :=
  congr_arg (fun a => x ^ a) ((Nat.add_comm _ _).trans (Nat.mod_add_div _ _)).symm
α : Type ?u.27674
M✝ : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
M : Type u_1
inst✝ : Monoid M
x : M
m n : ℕ
h : x ^ n = 1
t : x ^ m = x ^ (n * (m / n) + m % n)
⊢ x ^ m = x ^ (m % n)
α : Type ?u.27674
M✝ : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
M : Type u_1
inst✝ : Monoid M
x : M
m n : ℕ
h : x ^ n = 1
t : x ^ m = x ^ (n * (m / n) + m % n)
⊢ x ^ m = x ^ (m % n)
dsimp at t
no goals
α : Type ?u.27674
M✝ : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
M : Type u_1
inst✝ : Monoid M
x : M
m n : ℕ
h : x ^ n = 1
t : x ^ m = x ^ (n * (m / n) + m % n)
⊢ x ^ m = x ^ (m % n)
rw [t, pow_add, pow_mul, h, one_pow, one_mul]