-- 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))
rw :
  H.transferFunction g (HPow.hPow (β := ℤ) g k.cast • Quotient.out q) =
    HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
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)))
                  (HPow.hPow (β := ℤ) g k.cast • Quotient.out 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)))
                (HPow.hPow (β := ℤ) g k.cast • Quotient.out 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)))
                      (HPow.hPow (β := ℤ) g k.cast • Quotient.out 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)))
              (HPow.hPow (β := ℤ) g k.cast • Quotient.out q)))) =
    HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
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)))
                  (((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))) q k) :
                    G ⧸ H)))))
          (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)))
                (((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))) q k) :
                  G ⧸ H)) :
            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)))
                      (((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))) q k) :
                        G ⧸ H))))))) *
      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)))
              (((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))) q k) :
                G ⧸ H)))) =
    HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
rw₃ rw₄ :
  HPow.hPow (β := ℤ) g
        (ZMod.cast (n :=
          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))))
          (Sigma.snd (β := 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))) *
      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))) =
    HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
⊢ (↑((⋯.leftQuotientEquiv (S := (↑(H.transferTransversal g) : Set G)) :
            (a : G ⧸ H) → (↑(↑(H.transferTransversal g) : Set G) : Type u_1))
          (HPow.hPow (β := ℤ) g k.cast • Quotient.out q)) :
      G) =
    HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)

Tactic:
rw [transferTransversal_apply, transferFunction_apply, ← quotientEquivSigmaZMod_symm_apply,
    apply_symm_apply]

Premises used: Subgroup.transferTransversal_apply, Equiv.apply_symm_apply, Subgroup.transferFunction_apply, Subgroup.quotientEquivSigmaZMod_symm_apply