Theorem: torsion_implies_square_torsion (UnitConjecture/TorsionFree.lean)

State before:
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
g_tor : g ^ n = 1
⊢ (g ^ 2) ^ n = g ^ (2 * n)
Tactic:
rw [← pow_mul]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
g_tor : g ^ n = 1
⊢ g ^ (2 * n) = g ^ (n * 2)
Tactic:
rw [mul_comm]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
g_tor : g ^ n = 1
⊢ g ^ (n * 2) = (g ^ n) ^ 2
Tactic:
rw [pow_mul]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
g_tor : g ^ n = 1
⊢ (g ^ n) ^ 2 = 1 ^ 2
Tactic:
rw [← g_tor]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
g_tor : g ^ n = 1
⊢ 1 ^ 2 = 1
Tactic:
rw [one_pow]
State after:
no goals