G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
⊢ (g ^
        if k = 0 then ↑(minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' { fst := q, snd := k - 1 }.fst))
        else ↑k) *
      Quotient.out' (Quotient.out' { fst := q, snd := k - 1 }.fst) =
    if k = 0 then g ^ minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
    else g ^ ↑k * Quotient.out' (Quotient.out' q)
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
⊢ ↑(↑(toEquiv (_ : ↑(g • transferTransversal H g) ∈ leftTransversals ↑H)) (g ^ ↑k • Quotient.out' q)) =
    if k = 0 then g ^ minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
    else g ^ ↑k * Quotient.out' (Quotient.out' q)
rw [smul_apply_eq_smul_apply_inv_smul, transferTransversal_apply, transferFunction_apply, ←
  mul_smul, ← zpow_neg_one, ← zpow_add, quotientEquivSigmaZMod_apply, smul_eq_mul, ← mul_assoc,
  ← zpow_one_add, Int.cast_add, Int.cast_neg, Int.cast_one, int_cast_cast, cast_id', id.def, ←
  sub_eq_neg_add, cast_sub_one, add_sub_cancel'_right]
case pos
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
hk : k = 0
⊢ (g ^
        if k = 0 then ↑(minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' { fst := q, snd := k - 1 }.fst))
        else ↑k) *
      Quotient.out' (Quotient.out' { fst := q, snd := k - 1 }.fst) =
    if k = 0 then g ^ minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
    else g ^ ↑k * Quotient.out' (Quotient.out' q)

case neg
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
hk : ¬k = 0
⊢ (g ^
        if k = 0 then ↑(minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' { fst := q, snd := k - 1 }.fst))
        else ↑k) *
      Quotient.out' (Quotient.out' { fst := q, snd := k - 1 }.fst) =
    if k = 0 then g ^ minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
    else g ^ ↑k * Quotient.out' (Quotient.out' q)
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
⊢ (g ^
        if k = 0 then ↑(minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' { fst := q, snd := k - 1 }.fst))
        else ↑k) *
      Quotient.out' (Quotient.out' { fst := q, snd := k - 1 }.fst) =
    if k = 0 then g ^ minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
    else g ^ ↑k * Quotient.out' (Quotient.out' q)
by_cases hk : k = 0
no goals
case pos
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
hk : k = 0
⊢ (g ^
        if k = 0 then ↑(minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' { fst := q, snd := k - 1 }.fst))
        else ↑k) *
      Quotient.out' (Quotient.out' { fst := q, snd := k - 1 }.fst) =
    if k = 0 then g ^ minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
    else g ^ ↑k * Quotient.out' (Quotient.out' q)
rw [if_pos hk, if_pos hk, zpow_ofNat]
no goals
case neg
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
hk : ¬k = 0
⊢ (g ^
        if k = 0 then ↑(minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' { fst := q, snd := k - 1 }.fst))
        else ↑k) *
      Quotient.out' (Quotient.out' { fst := q, snd := k - 1 }.fst) =
    if k = 0 then g ^ minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
    else g ^ ↑k * Quotient.out' (Quotient.out' q)
rw [if_neg hk, if_neg hk]