-- Mathlib/GroupTheory/Transfer.lean
theorem transfer_eq_prod_quotient_orbitRel_zpowers_quot [FiniteIndex H] (g : G)
    [Fintype (Quotient (orbitRel (zpowers g) (G ⧸ H)))] :
    transfer ϕ g =
      ∏ q : Quotient (orbitRel (zpowers g) (G ⧸ H)),
        ϕ
          ⟨q.out.out⁻¹ * g ^ Function.minimalPeriod (g • ·) q.out * q.out.out,
            QuotientGroup.out_conj_pow_minimalPeriod_mem H g q.out⟩

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
⊢ ϕ.transfer g =
    ∏ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)),
      ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩

Tactic:
letI := H.fintypeQuotientOfFiniteIndex

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
⊢ ϕ.transfer g =
    ∏ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)),
      ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
⊢ ∏ a : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H),
      ∏ s : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out a)),
        ϕ
          ⟨(↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨a, s⟩)))⁻¹ *
              ↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨a, s⟩)),
            ⋯⟩ =
    ∏ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)),
      ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩

Tactic:
refine Fintype.prod_congr _ _ (fun q => ?_)

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
⊢ ∏ s : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q)),
      ϕ
        ⟨(↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨q, s⟩)))⁻¹ *
            ↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨q, s⟩)),
          ⋯⟩ =
    ϕ
      ⟨(Quotient.out (Quotient.out q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out q) *
          Quotient.out (Quotient.out q),
        ⋯⟩

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))
hk : k ≠ 0
⊢ ϕ ⟨1, ⋯⟩ = 1

Tactic:
exact map_one ϕ

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
⊢ ∏ s : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q)),
      ϕ
        ⟨(↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨q, s⟩)))⁻¹ *
            ↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨q, s⟩)),
          ⋯⟩ =
    ϕ
      ⟨(Quotient.out (Quotient.out q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out q) *
          Quotient.out (Quotient.out q),
        ⋯⟩

Tactic:
simp only [quotientEquivSigmaZMod_symm_apply, transferTransversal_apply',
  transferTransversal_apply'']

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
⊢ ∏ x : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q)),
      ϕ
        ⟨(g ^ x.cast * Quotient.out (Quotient.out q))⁻¹ *
            if x = 0 then g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
            else g ^ x.cast * Quotient.out (Quotient.out q),
          ⋯⟩ =
    ϕ
      ⟨(Quotient.out (Quotient.out q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out q) *
          Quotient.out (Quotient.out q),
        ⋯⟩

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
⊢ ∀ (x : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))),
    x ≠ 0 →
      ϕ
          ⟨(g ^ x.cast * Quotient.out (Quotient.out q))⁻¹ *
              if x = 0 then g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
              else g ^ x.cast * Quotient.out (Quotient.out q),
            ⋯⟩ =
        1

Tactic:
intro k hk

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))
hk : k ≠ 0
⊢ ϕ
      ⟨(g ^ k.cast * Quotient.out (Quotient.out q))⁻¹ *
          if k = 0 then g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
          else g ^ k.cast * Quotient.out (Quotient.out q),
        ⋯⟩ =
    1

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
⊢ ϕ
      ⟨(g ^ ZMod.cast 0 * Quotient.out (Quotient.out q))⁻¹ *
          if 0 = 0 then g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
          else g ^ ZMod.cast 0 * Quotient.out (Quotient.out q),
        ⋯⟩ =
    ϕ
      ⟨(Quotient.out (Quotient.out q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out q) *
          Quotient.out (Quotient.out q),
        ⋯⟩

Tactic:
simp only [if_pos, ZMod.cast_zero, zpow_zero, one_mul, mul_assoc]

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))
hk : k ≠ 0
⊢ ϕ
      ⟨(g ^ k.cast * Quotient.out (Quotient.out q))⁻¹ *
          if k = 0 then g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
          else g ^ k.cast * Quotient.out (Quotient.out q),
        ⋯⟩ =
    1

Tactic:
simp only [if_neg hk, inv_mul_cancel]

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
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))
hk : k ≠ 0
⊢ ϕ ⟨1, ⋯⟩ = 1