G : Type u_1
H : Type ?u.178531
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑(((fun x_1 => { val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_2 => x * x_2) n 1) } * x_1)^[n])
        1) =
    1
G : Type u_1
H : Type ?u.178531
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑(((fun x x_1 => x * x_1)
            { val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1) }^[n])
        1) =
    ↑1
dsimp
G : Type u_1
H : Type ?u.178531
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑((fun x_1 => { val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_2 => x * x_2) n 1) } ^ n * x_1)
        1) =
    1
G : Type u_1
H : Type ?u.178531
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑(((fun x_1 => { val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_2 => x * x_2) n 1) } * x_1)^[n])
        1) =
    1
rw [mul_left_iterate]
G : Type u_1
H : Type ?u.178531
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑({ val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_1 => x * x_1) n 1) } ^ n) * 1 = 1
G : Type u_1
H : Type ?u.178531
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑((fun x_1 => { val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_2 => x * x_2) n 1) } ^ n * x_1)
        1) =
    1
change _ * 1 = 1
no goals
G : Type u_1
H : Type ?u.178531
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑({ val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_1 => x * x_1) n 1) } ^ n) * 1 = 1
rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
  (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]