-- 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
⊢ 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
            (fun
                (q :
                  Quotient (α := G ⧸ H)
                    (orbitRel
                      (↥(zpowers
                          (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g sorry) : 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 sorry) : G) ^
                      Function.minimalPeriod
                        (fun (x : G ⧸ H) ↦
                          (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g sorry) : G) •
                            x)
                        q.out *
                  Quotient.out q.out)
                sorry)
            (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 sorry)
                (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
            (Finset.toList Finset.univ))) :
      G)
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