-- 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
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
letI letI₁ letI₂ :
  Eq.{u_2 + 1} (α := A) ((ϕ.transfer : (a : G) → A) g : A)
    ((ϕ : (a : ↥H) → A) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g ^ H.index) ⋯) : A)
letI₃ :
  ∀
    (key :
      ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
        (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k),
    Eq.{u_2 + 1} (α := A) ((ϕ.transfer : (a : G) → A) g : A)
      ((ϕ : (a : ↥H) → A) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g ^ H.index) ⋯) : A)
letI₄ :
  let this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex;
  ∀
    (key :
      ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
        (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k),
    Eq.{u_2 + 1} (α := A)
      ((ϕ : (a : ↥H) → A)
          (List.prod
            (List.map
              (fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
                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)
                  ⋯)
              (Finset.toList Finset.univ))) :
        A)
      ((ϕ : (a : ↥H) → A) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g ^ H.index) ⋯) : A)
letI₅ :
  let this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex;
  ∀
    (key :
      ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
        (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k),
    Eq.{u_1 + 1} (α := G)
      ((fun (a : ↥H) ↦ (↑a : G))
        (List.prod
          (List.map
            (fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
              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)
                ⋯)
            (Finset.toList Finset.univ))))
      ((fun (a : ↥H) ↦ (↑a : G)) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g ^ H.index) ⋯))
letI₆ :
  let this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex;
  ∀
    (key :
      ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
        (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k),
    (↑(List.prod
            (List.map
              (fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
                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)
                  ⋯)
              (Finset.toList Finset.univ))) :
        G) =
      g ^ H.index
letI₇ :
  let this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex;
  ∀
    (key :
      ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
        (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k),
    Eq.{u_1 + 1} (α := G)
      (↑(List.prod
            (List.map
              (fun
                  (q :
                    Quotient (α := G ⧸ H)
                      (orbitRel
                        (↥(zpowers
                            (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯) :
                              G)))
                        (G ⧸ H))) ↦
                Subtype.mk (p := fun (x : G) ↦ x ∈ H)
                  ((Quotient.out q.out)⁻¹ *
                      (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯) : G) ^
                        Function.minimalPeriod
                          (fun (x : G ⧸ H) ↦
                            (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯) :
                                G) •
                              x)
                          q.out *
                    Quotient.out q.out)
                  ⋯)
              (Finset.toList Finset.univ))) :
        G)
      (↑(List.prod
            (List.map
              (fun (i : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
                HPow.hPow (α := ↥(zpowers g))
                  (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯)
                  (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
              (Finset.toList Finset.univ))) :
        G)
⊢ Eq.{u_2 + 1} (α := A) ((ϕ.transfer : (a : G) → A) g : A)
    ((ϕ : (a : ↥H) → A) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g ^ H.index) ⋯) : A)
have letI₈ : let this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex;
∀
  (key :
    ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
      (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k),
  Eq.{u_1 + 1} (α := G)
    (List.prod
      (List.map (α := Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
        (Function.comp (β := ↥H) (Subtype.val (p := fun (x : G) ↦ x ∈ H))
          fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
          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)
        (Finset.toList Finset.univ)))
    (List.prod
      (List.map (α := Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
        (Function.comp (β := ↥(zpowers g))
          (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x))
          fun (i : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
          HPow.hPow (α := ↥(zpowers g))
            (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g sorry)
            (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
        (Finset.toList Finset.univ)))
Tactic: classical
    letI := H.fintypeQuotientOfFiniteIndex
    change ∀ (k g₀) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑(⟨g₀⁻¹ * g ^ k * g₀, hk⟩ : H) = g ^ k at key
    rw [transfer_eq_prod_quotient_orbitRel_zpowers_quot, ← Finset.prod_map_toList,
      ← Function.comp_def ϕ, List.prod_map_hom]
    refine congrArg ϕ (Subtype.coe_injective ?_)
    dsimp only
    rw [H.coe_mk, ← (zpowers g).coe_mk g (mem_zpowers g), ← (zpowers g).coe_pow,
      index_eq_sum_minimalPeriod H g, ← Finset.prod_pow_eq_pow_sum, ← Finset.prod_map_toList]
    simp only [Subgroup.val_list_prod, List.map_map]
    congr 2
    funext
    apply key
Cleared hypotheses: key