-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : G ⧸ H
rw :
  (↑(HPow.hPow (β := ℤ) g
            (ZMod.cast (n :=
              minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
                (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
                  (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                    ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                    ((H.quotientEquivSigmaZMod g :
                        (a : G ⧸ H) →
                          (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                      q))))
              (Sigma.snd (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                  ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                  ((H.quotientEquivSigmaZMod g :
                      (a : G ⧸ H) →
                        (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                          ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                    q) :
                ZMod
                  (minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
                    (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
                      (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                        ((H.quotientEquivSigmaZMod g :
                            (a : G ⧸ H) →
                              (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                                ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                          q)))))) *
          Quotient.out (s := QuotientGroup.leftRel H)
            (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
              (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                ((H.quotientEquivSigmaZMod g :
                    (a : G ⧸ H) →
                      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                  q)))) :
      G ⧸ H) =
    q
rw₁ :
  (↑(HSMul.hSMul (β := G)
          (HPow.hPow (β := ℤ) g
            (ZMod.cast (n :=
              minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
                (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
                  (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                    ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                    ((H.quotientEquivSigmaZMod g :
                        (a : G ⧸ H) →
                          (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                      q))))
              (Sigma.snd (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                  ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                  ((H.quotientEquivSigmaZMod g :
                      (a : G ⧸ H) →
                        (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                          ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                    q) :
                ZMod
                  (minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
                    (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
                      (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                        ((H.quotientEquivSigmaZMod g :
                            (a : G ⧸ H) →
                              (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                                ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                          q)))))))
          (Quotient.out (s := QuotientGroup.leftRel H)
            (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
              (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                ((H.quotientEquivSigmaZMod g :
                    (a : G ⧸ H) →
                      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                  q))))) :
      G ⧸ H) =
    q
rw₂ :
  HSMul.hSMul (β := G ⧸ H)
      (HPow.hPow (β := ℤ) g
        (ZMod.cast (n :=
          minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
            (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
              (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                ((H.quotientEquivSigmaZMod g :
                    (a : G ⧸ H) →
                      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                  q))))
          (Sigma.snd (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
              ((H.quotientEquivSigmaZMod g :
                  (a : G ⧸ H) →
                    (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                      ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                q) :
            ZMod
              (minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
                (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
                  (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                    ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                    ((H.quotientEquivSigmaZMod g :
                        (a : G ⧸ H) →
                          (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                      q)))))))
      (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
        (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
          ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
          ((H.quotientEquivSigmaZMod g :
              (a : G ⧸ H) →
                (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                  ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
            q))) =
    q
⊢ (↑(H.transferFunction g q) : G ⧸ H) = q
have rw₃ : ((H.quotientEquivSigmaZMod g).symm :
      (a :
          (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) →
        G ⧸ H)
    (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
      ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
      (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
        ((H.quotientEquivSigmaZMod g :
            (a : G ⧸ H) →
              (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
          q))
      (Sigma.snd (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
        ((H.quotientEquivSigmaZMod g :
            (a : G ⧸ H) →
              (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
          q))) =
  q
Tactic: rw [transferFunction_apply, ← smul_eq_mul, Quotient.coe_smul_out,
    ← quotientEquivSigmaZMod_symm_apply, Sigma.eta, symm_apply_apply]