-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))
hk : k = 0
pos :
  HPow.hPow (β := ℤ) g
        (↑(minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
              (Quotient.out
                (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                  ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                  (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                    ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1))))) :
          ℤ) *
      Quotient.out
        (Quotient.out
          (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
            (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1)))) =
    if k = 0 then g ^ minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
pos₁ :
  HPow.hPow (β := ℤ) g
        (↑(minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
              (Quotient.out
                (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                  ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                  (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                    ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1))))) :
          ℤ) *
      Quotient.out
        (Quotient.out
          (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
            (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1)))) =
    g ^ minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
pos₂ pos₃ :
  g ^
        minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
          (Quotient.out
            (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
              (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1)))) *
      Quotient.out
        (Quotient.out
          (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
            (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1)))) =
    g ^ minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
⊢ HPow.hPow (β := ℤ) g
        (if k = 0 then
          (↑(minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
                (Quotient.out
                  (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                    ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                    (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                      ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1))))) :
            ℤ)
        else k.cast) *
      Quotient.out
        (Quotient.out
          (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
            (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1)))) =
    if k = 0 then g ^ minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)

Tactic:
rw [if_pos hk, if_pos hk, zpow_natCast]

Premises used: zpow_natCast, if_pos