-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Type u_2
inst_1 : CommGroup A
ϕ : MonoidHom.{u_1, u_2} (↥H) A
inst_2 : H.FiniteIndex
g : G
inst_3 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ Eq.{u_2 + 1} (α := A) ((ϕ.transfer : (a : G) → A) g : A)
    (∏ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)),
        (ϕ : (a : ↥H) → A)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out * Quotient.out q.out)
            ⋯) :
      A)
have transfer : Eq.{u_2 + 1} (α := A)
  (∏ a : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H),
    ∏ s : ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out a)),
      (ϕ : (a : ↥H) → A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((sorry.leftQuotientEquiv (S := (↑(H.transferTransversal g) : Set G)) :
                      (a : G ⧸ H) → (↑(↑(H.transferTransversal g) : Set G) : Type u_1))
                    (((H.quotientEquivSigmaZMod g).symm :
                        (a :
                            (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                              ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) →
                          G ⧸ H)
                      (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                        ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) a s))) :
                G)⁻¹
            (↑((sorry.leftQuotientEquiv (S := (↑(g • H.transferTransversal g) : Set G)) :
                    (a : G ⧸ H) → (↑(↑(g • H.transferTransversal g) : Set G) : Type u_1))
                  (((H.quotientEquivSigmaZMod g).symm :
                      (a :
                          (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                            ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) →
                        G ⧸ H)
                    (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                      ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) a s))) :
              G))
          sorry))
  (∏ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)),
    (ϕ : (a : ↥H) → A)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out * Quotient.out q.out) sorry))
Tactic: calc
      transfer ϕ g = ∏ q : G ⧸ H, _ := transfer_def ϕ (transferTransversal H g) g
      _ = _ := ((quotientEquivSigmaZMod H g).symm.prod_comp _).symm
      _ = _ := Finset.prod_sigma _ _ _
      _ = _ := by
        refine Fintype.prod_congr _ _ (fun q => ?_)
        simp only [quotientEquivSigmaZMod_symm_apply, transferTransversal_apply',
          transferTransversal_apply'']
        rw [Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod (g • ·) q.out)) _]
        · simp only [if_pos, ZMod.cast_zero, zpow_zero, one_mul, mul_assoc]
        · intro k hk
          simp only [if_neg hk, inv_mul_cancel]
          exact map_one ϕ