-- Module: Mathlib.GroupTheory.Transfer
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)
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)
              ⋯)
          (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 ⋯)
              (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
          (Finset.toList Finset.univ)))
e_xs :
  ∀
    (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} (α := Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)) → G)
      (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) ⋯)
      (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 ⋯)
          (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
e_xs₁ :
  ∀
    (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)
    (x : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))),
    Eq (α := G)
      (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)
            ⋯)
        x)
      (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 ⋯)
            (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
        x)
⊢ 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)

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

Premises used: Subgroup.coe_mk, Finset.prod_map_toList, congrArg, Subgroup.val_list_prod, Subgroup.coe_pow, Subgroup.mem_zpowers, List.map_map, List.prod_map_hom, Subtype.coe_injective, Function.comp_def, Finset.prod_pow_eq_pow_sum, Subgroup.zpowers, DFunLike.coe, MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot