awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ Eq.{u_2 + 1} (α := A)
    (∏ q : G ⧸ H,
      (ϕ : (a : ↥H) → A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((⋯.leftQuotientEquiv (S := (↑(H.transferTransversal g) : Set G)) :
                      (a : G ⧸ H) → (↑(↑(H.transferTransversal g) : Set G) : Type u_1))
                    q) :
                G)⁻¹
            (↑((⋯.leftQuotientEquiv (S := (↑(g • H.transferTransversal g) : Set G)) :
                    (a : G ⧸ H) → (↑(↑(g • H.transferTransversal g) : Set G) : Type u_1))
                  q) :
              G))
          ⋯))
    (∏ i :
      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
        ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)),
      (ϕ : (a : ↥H) → A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((⋯.leftQuotientEquiv (S := (↑(H.transferTransversal g) : Set G)) :
                      (a : G ⧸ H) → (↑(↑(H.transferTransversal g) : Set G) : Type u_1))
                    (((H.quotientEquivSigmaZMod g).symm :
                        (a :
                            (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                              ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) →
                          G ⧸ H)
                      i)) :
                G)⁻¹
            (↑((⋯.leftQuotientEquiv (S := (↑(g • H.transferTransversal g) : Set G)) :
                    (a : G ⧸ H) → (↑(↑(g • H.transferTransversal g) : Set G) : Type u_1))
                  (((H.quotientEquivSigmaZMod g).symm :
                      (a :
                          (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                            ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) →
                        G ⧸ H)
                    i)) :
              G))
          ⋯))

Tactic:
((quotientEquivSigmaZMod H g).symm.prod_comp _).symm

Premises used: Equiv.prod_comp, Subgroup.quotientEquivSigmaZMod, Equiv.symm, Eq.symm
-- 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
inst_3 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ Eq.{u_2 + 1} (α := A)
    (∏ a : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H),
      ∏ s : ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out a)),
        (ϕ : (a : ↥H) → A)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((⋯.leftQuotientEquiv (S := (↑(H.transferTransversal g) : Set G)) :
                        (a : G ⧸ H) → (↑(↑(H.transferTransversal g) : Set G) : Type u_1))
                      (((H.quotientEquivSigmaZMod g).symm :
                          (a :
                              (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                                ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) →
                            G ⧸ H)
                        (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                          ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) a s))) :
                  G)⁻¹
              (↑((⋯.leftQuotientEquiv (S := (↑(g • H.transferTransversal g) : Set G)) :
                      (a : G ⧸ H) → (↑(↑(g • H.transferTransversal g) : Set G) : Type u_1))
                    (((H.quotientEquivSigmaZMod g).symm :
                        (a :
                            (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                              ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) →
                          G ⧸ H)
                      (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                        ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) a s))) :
                G))
            ⋯))
    (∏ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)),
      (ϕ : (a : ↥H) → A)
        (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) ⋯))

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

Premises used: Fintype.prod_congr
-- 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
inst_3 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
rw :
  Eq.{u_2 + 1} (α := A)
    ((ϕ : (a : ↥H) → A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          ((HPow.hPow (β := ℤ) g
                  (ZMod.cast (n := Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)) 0) *
                Quotient.out (Quotient.out q))⁻¹ *
            if Eq (α := ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) 0 0 then
              g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
            else
              HPow.hPow (β := ℤ) g
                  (ZMod.cast (n := Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)) 0) *
                Quotient.out (Quotient.out q))
          ⋯) :
      A)
    ((ϕ : (a : ↥H) → A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          ((Quotient.out (Quotient.out q))⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) *
            Quotient.out (Quotient.out q))
          ⋯) :
      A)
rw₁ :
  ∀ (x : ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))),
    x ≠ 0 →
      Eq.{u_2 + 1} (α := A)
        ((ϕ : (a : ↥H) → A)
            (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
              ((HPow.hPow (β := ℤ) g x.cast * Quotient.out (Quotient.out q))⁻¹ *
                if x = 0 then
                  g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
                else HPow.hPow (β := ℤ) g x.cast * Quotient.out (Quotient.out q))
              ⋯) :
          A)
        (1 : A)
⊢ Eq.{u_2 + 1} (α := A)
    (∏ x : ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)),
        (ϕ : (a : ↥H) → A)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            ((HPow.hPow (β := ℤ) g x.cast * Quotient.out (Quotient.out q))⁻¹ *
              if x = 0 then
                g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
              else HPow.hPow (β := ℤ) g x.cast * Quotient.out (Quotient.out q))
            ⋯) :
      A)
    ((ϕ : (a : ↥H) → A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          ((Quotient.out (Quotient.out q))⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) *
            Quotient.out (Quotient.out q))
          ⋯) :
      A)

Tactic:
rw [Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod (g • ·) q.out)) _]

Premises used: OfNat.ofNat, Fintype.prod_eq_single
-- 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
inst_3 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
⊢ Eq.{u_2 + 1} (α := A)
    ((ϕ : (a : ↥H) → A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          ((HPow.hPow (β := ℤ) g
                  (ZMod.cast (n := Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)) 0) *
                Quotient.out (Quotient.out q))⁻¹ *
            if Eq (α := ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) 0 0 then
              g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
            else
              HPow.hPow (β := ℤ) g
                  (ZMod.cast (n := Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)) 0) *
                Quotient.out (Quotient.out q))
          ⋯) :
      A)
    ((ϕ : (a : ↥H) → A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          ((Quotient.out (Quotient.out q))⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) *
            Quotient.out (Quotient.out q))
          ⋯) :
      A)

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

Premises used: mul_assoc, zpow_zero, if_pos, ZMod.cast_zero, one_mul
-- 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
inst_3 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))
hk : k ≠ 0
simp : Eq.{u_2 + 1} (α := A) ((ϕ : (a : ↥H) → A) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) 1 ⋯) : A) (1 : A)
⊢ Eq.{u_2 + 1} (α := A)
    ((ϕ : (a : ↥H) → A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          ((HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q))⁻¹ *
            if k = 0 then
              g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
            else HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q))
          ⋯) :
      A)
    (1 : A)

Tactic:
simp only [if_neg hk, inv_mul_cancel]

Premises used: inv_mul_cancel, if_neg
-- 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
inst_3 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))
hk : k ≠ 0
⊢ Eq.{u_2 + 1} (α := A) ((ϕ : (a : ↥H) → A) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) 1 ⋯) : A) (1 : A)

Tactic:
map_one ϕ

Premises used: map_one
-- 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
inst_3 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))
hk : k ≠ 0
⊢ Eq.{u_2 + 1} (α := A) ((ϕ : (a : ↥H) → A) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) 1 ⋯) : A) (1 : A)

Tactic:
exact map_one ϕ

Premises used: map_one
-- 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
inst_3 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
letI letI₁ letI₂ :
  Eq.{u_2 + 1} (α := A) ((ϕ.transfer : (a : G) → A) g : A)
    (∏ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)),
        (ϕ : (a : ↥H) → A)
          (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)
            ⋯) :
      A)
⊢ Eq.{u_2 + 1} (α := A) ((ϕ.transfer : (a : G) → A) g : A)
    (∏ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)),
        (ϕ : (a : ↥H) → A)
          (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)
            ⋯) :
      A)

Tactic:
classical
    letI := H.fintypeQuotientOfFiniteIndex
    calc
      transfer ϕ g = ∏ q : G ⧸ H, _ := transfer_def ϕ (transferTransversal H g) g
      _ = _ := ((quotientEquivSigmaZMod H g).symm.prod_comp _).symm
      _ = _ := Finset.prod_sigma _ _ _
      _ = _ := by
        refine Fintype.prod_congr _ _ (fun q => ?_)
        simp only [quotientEquivSigmaZMod_symm_apply, transferTransversal_apply',
          transferTransversal_apply'']
        rw [Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod (g • ·) q.out)) _]
        · simp only [if_pos, ZMod.cast_zero, zpow_zero, one_mul, mul_assoc]
        · intro k hk
          simp only [if_neg hk, inv_mul_cancel]
          exact map_one ϕ

Premises used: MonoidHom.transfer, MonoidHom.transfer_def, Subgroup.transferTransversal, Finset.prod_sigma, DFunLike.coe
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
pos : ∀ (hH : H.index = 0), g ^ H.index ∈ H
neg : ∀ (hH : ¬H.index = 0), g ^ H.index ∈ H
⊢ g ^ H.index ∈ H

Tactic:
by_cases hH : H.index = 0

Premises used: Subgroup.index
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : H.index = 0
pos : 1 ∈ H
⊢ g ^ H.index ∈ H

Tactic:
rw [hH, pow_zero]

Premises used: pow_zero
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : H.index = 0
⊢ 1 ∈ H

Tactic:
H.one_mem

Premises used: Set.Mem, Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : H.index = 0
⊢ 1 ∈ H

Tactic:
exact H.one_mem

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
⊢ ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H

Tactic:
replace key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H := fun k g₀ hk =>
      (congr_arg (· ∈ H) (key k g₀ hk)).mp hk
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H
⊢ ∀ (q : G ⧸ H), g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q ∈ H

Tactic:
replace key : ∀ q : G ⧸ H, g ^ Function.minimalPeriod (g • ·) q ∈ H := fun q =>
      key (Function.minimalPeriod (g • ·) q) q.out
        (QuotientGroup.out_conj_pow_minimalPeriod_mem H g q)
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (q : G ⧸ H), g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q ∈ H
f : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)) → ↥(zpowers g) :=
  fun (q : 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) q.out)
⊢ ∀ (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))),
    Membership.mem (γ := Subgroup ↥(zpowers g)) (H.subgroupOf (zpowers g)) (f q)

Tactic:
have hf : ∀ q, f q ∈ H.subgroupOf (zpowers g) := fun q => key q.out
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (q : G ⧸ H), g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q ∈ H
f : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)) → ↥(zpowers g) :=
  fun (q : 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) q.out)
hf :
  ∀ (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))),
    Membership.mem (γ := Subgroup ↥(zpowers g)) (H.subgroupOf (zpowers g)) (f q)
⊢ Membership.mem (γ := Subgroup ↥(zpowers g)) (H.subgroupOf (zpowers g))
    (∏ c : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), f c)

Tactic:
replace key :=
      Subgroup.prod_mem (H.subgroupOf (zpowers g)) fun q (_ : q ∈ Finset.univ) => hf q
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
f : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)) → ↥(zpowers g) :=
  fun (q : 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) q.out)
hf :
  ∀ (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))),
    Membership.mem (γ := Subgroup ↥(zpowers g)) (H.subgroupOf (zpowers g)) (f q)
key :
  Membership.mem (γ := Subgroup ↥(zpowers g)) (H.subgroupOf (zpowers g))
    (∏ c : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), f c)
⊢ g ^ H.index ∈ H

Tactic:
simpa only [f, Finset.prod_pow_eq_pow_sum, index_eq_sum_minimalPeriod H g] using key

Premises used: Subgroup.index_eq_sum_minimalPeriod, Finset.prod_pow_eq_pow_sum
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
neg neg₁ neg₂ : ∀ (key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H), g ^ H.index ∈ H
neg₃ neg₄ : ∀ (key : ∀ (q : G ⧸ H), g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q ∈ H), g ^ H.index ∈ H
neg₅ :
  ∀ (key : ∀ (q : G ⧸ H), g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q ∈ H),
    let f : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)) → ↥(zpowers g) :=
      fun (q : 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) q.out);
    ∀
      (hf :
        ∀ (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))),
          Membership.mem (γ := Subgroup ↥(zpowers g)) (H.subgroupOf (zpowers g)) (f q)),
      g ^ H.index ∈ H
neg₆ :
  let f : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)) → ↥(zpowers g) :=
    fun (q : 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) q.out);
  ∀
    (hf :
      ∀ (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))),
        Membership.mem (γ := Subgroup ↥(zpowers g)) (H.subgroupOf (zpowers g)) (f q))
    (key :
      Membership.mem (γ := Subgroup ↥(zpowers g)) (H.subgroupOf (zpowers g))
        (∏ c : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), f c)),
    g ^ H.index ∈ H
⊢ g ^ H.index ∈ H

Tactic:
classical
    replace key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H := fun k g₀ hk =>
      (congr_arg (· ∈ H) (key k g₀ hk)).mp hk
    replace key : ∀ q : G ⧸ H, g ^ Function.minimalPeriod (g • ·) q ∈ H := fun q =>
      key (Function.minimalPeriod (g • ·) q) q.out
        (QuotientGroup.out_conj_pow_minimalPeriod_mem H g q)
    let f : Quotient (orbitRel (zpowers g) (G ⧸ H)) → zpowers g := fun q =>
      (⟨g, mem_zpowers g⟩ : zpowers g) ^ Function.minimalPeriod (g • ·) q.out
    have hf : ∀ q, f q ∈ H.subgroupOf (zpowers g) := fun q => key q.out
    replace key :=
      Subgroup.prod_mem (H.subgroupOf (zpowers g)) fun q (_ : q ∈ Finset.univ) => hf q
    simpa only [f, Finset.prod_pow_eq_pow_sum, index_eq_sum_minimalPeriod H g] using key

Premises used: Finset.prod_pow_eq_pow_sum
-- 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
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
change :
  ∀
    (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)
⊢ 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:
change ∀ (k g₀) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑(⟨g₀⁻¹ * g ^ k * g₀, hk⟩ : H) = g ^ k at key
-- 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
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
rw :
  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)
⊢ 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:
rw [transfer_eq_prod_quotient_orbitRel_zpowers_quot, ← Finset.prod_map_toList,
      ← Function.comp_def ϕ, List.prod_map_hom]

Premises used: Finset.prod_map_toList, List.prod_map_hom, Function.comp_def, DFunLike.coe, MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot
-- 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
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)

Tactic:
congrArg ϕ (Subtype.coe_injective ?_)

Premises used: congrArg, Subtype.coe_injective, DFunLike.coe