-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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))
pos :
  ∀ (hk : k = 0),
    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)
⊢ 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)
have neg : ∀ (hk : ¬k = 0),
  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: by_cases hk : k = 0