-- Mathlib/GroupTheory/Transfer.lean
theorem transfer_eq_pow [FiniteIndex H] (g : G)
    (key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k) :
    transfer ϕ g = ϕ ⟨g ^ H.index, transfer_eq_pow_aux g key⟩

Proof state:
case e_a.e_f
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ (Subtype.val ∘ fun q =>
      ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩) =
    Subtype.val ∘ fun i => ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x => g • x) (Quotient.out i)

Tactic:
funext

Result:
case e_a.e_f.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
x✝ : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))
⊢ (Subtype.val ∘ fun q =>
        ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩)
      x✝ =
    (Subtype.val ∘ fun i => ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x => g • x) (Quotient.out i)) x✝

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ ↑(List.map
          (fun q =>
            ⟨(Quotient.out q.out)⁻¹ * ↑⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x => ↑⟨g, ⋯⟩ • x) q.out *
                Quotient.out q.out,
              ⋯⟩)
          Finset.univ.toList).prod =
    ↑(List.map (fun i => ⟨g, ⋯⟩ ^ Fintype.card ↑(orbit (↥(zpowers g)) (Quotient.out i))) Finset.univ.toList).prod

Tactic:
simp only [Subgroup.val_list_prod, List.map_map, ← minimalPeriod_eq_card]

Result:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ (List.map
        (Subtype.val ∘ fun q =>
          ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩)
        Finset.univ.toList).prod =
    (List.map (Subtype.val ∘ fun i => ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x => g • x) (Quotient.out i))
        Finset.univ.toList).prod

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
⊢ ϕ.transfer g = ϕ ⟨g ^ H.index, ⋯⟩

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_to_list]
  refine (List.prod_map_hom _ _ _).trans ?_ 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_card,
    Nat.card_eq_fintype_card, Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)),
    Fintype.card_sigma, ← Finset.prod_pow_eq_pow_sum, ← Finset.prod_to_list]
  simp only [Subgroup.val_list_prod, List.map_map, ← minimalPeriod_eq_card]
  congr
  funext
  apply key

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ (fun a => ↑a)
      (List.map
          (fun q =>
            ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩)
          Finset.univ.toList).prod =
    (fun a => ↑a) ⟨g ^ H.index, ⋯⟩

Tactic:
dsimp only

Result:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ ↑(List.map
          (fun q =>
            ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩)
          Finset.univ.toList).prod =
    g ^ H.index

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ ↑(List.map
          (fun q =>
            ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩)
          Finset.univ.toList).prod =
    g ^ H.index

Tactic:
rw [H.coe_mk, ← (zpowers g).coe_mk g (mem_zpowers g), ← (zpowers g).coe_pow, index_eq_card,
  Nat.card_eq_fintype_card, Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)),
  Fintype.card_sigma, ← Finset.prod_pow_eq_pow_sum, ← Finset.prod_to_list]

Result:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ ↑(List.map
          (fun q =>
            ⟨(Quotient.out q.out)⁻¹ * ↑⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x => ↑⟨g, ⋯⟩ • x) q.out *
                Quotient.out q.out,
              ⋯⟩)
          Finset.univ.toList).prod =
    ↑(List.map (fun i => ⟨g, ⋯⟩ ^ Fintype.card ↑(orbit (↥(zpowers g)) (Quotient.out i))) Finset.univ.toList).prod

Proof state:
case e_a.e_f.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
x✝ : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))
⊢ (Subtype.val ∘ fun q =>
        ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩)
      x✝ =
    (Subtype.val ∘ fun i => ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x => g • x) (Quotient.out i)) x✝

Tactic:
apply key

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ ϕ
      (List.map
          (fun q =>
            ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩)
          Finset.univ.toList).prod =
    ϕ ⟨g ^ H.index, ⋯⟩

Tactic:
refine congrArg ϕ (Subtype.coe_injective ?_)

Result:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ (fun a => ↑a)
      (List.map
          (fun q =>
            ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩)
          Finset.univ.toList).prod =
    (fun a => ↑a) ⟨g ^ H.index, ⋯⟩