[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
rla : IsLeftRegular a
⊢ IsLeftRegular (a ^ n)
[PROOFSTEP]
simp only [IsLeftRegular, ← mul_left_iterate, rla.iterate n]
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
rra : IsRightRegular a
⊢ IsRightRegular (a ^ n)
[PROOFSTEP]
rw [IsRightRegular, ← mul_right_iterate]
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective (fun x => x * a)^[n]
[PROOFSTEP]
exact rra.iterate n
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n) ↔ IsLeftRegular a
[PROOFSTEP]
refine' ⟨_, IsLeftRegular.pow n⟩
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n) → IsLeftRegular a
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ']
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ Nat.pred n * a) → IsLeftRegular a
[PROOFSTEP]
exact IsLeftRegular.of_mul
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) ↔ IsRightRegular a
[PROOFSTEP]
refine' ⟨_, IsRightRegular.pow n⟩
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) → IsRightRegular a
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ]
[GOAL]
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ Nat.pred n) → IsRightRegular a
[PROOFSTEP]
exact IsRightRegular.of_mul
