-- Mathlib/GroupTheory/Transfer.lean
theorem transfer_eq_pow_aux (g : G)
    (key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k) :
    g ^ H.index ∈ H

Proof state:
case neg
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 • x) q ∈ H
f : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)) → ↥(zpowers g) :=
  fun q => ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x => g • x) q.out
hf : ∀ (q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))), f q ∈ H.subgroupOf (zpowers g)
⊢ g ^ H.index ∈ H

Tactic:
replace key :=
  Subgroup.prod_mem (H.subgroupOf (zpowers g)) fun q (_ : q ∈ Finset.univ) => hf q

Result:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
f : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)) → ↥(zpowers g) :=
  fun q => ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x => g • x) q.out
hf : ∀ (q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))), f q ∈ H.subgroupOf (zpowers g)
key : ∏ c : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), f c ∈ H.subgroupOf (zpowers g)
⊢ g ^ H.index ∈ H

Proof state:
case neg
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 • x) q ∈ H
f : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)) → ↥(zpowers g) :=
  fun q => ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x => g • x) q.out
⊢ g ^ H.index ∈ H

Tactic:
have hf : ∀ q, f q ∈ H.subgroupOf (zpowers g) := fun q => key q.out

Result:
case neg
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 • x) q ∈ H
f : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)) → ↥(zpowers g) :=
  fun q => ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x => g • x) q.out
hf : ∀ (q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))), f q ∈ H.subgroupOf (zpowers g)
⊢ g ^ H.index ∈ H

Proof state:
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
⊢ g ^ H.index ∈ H

Tactic:
by_cases hH : H.index = 0

Result:
case pos
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
⊢ g ^ H.index ∈ H

case neg
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
⊢ g ^ H.index ∈ H

Proof state:
case pos
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

Result:
no goals

Proof state:
case pos
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
⊢ g ^ H.index ∈ H

Tactic:
rw [hH, pow_zero]

Result:
case pos
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

Proof state:
case neg
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
⊢ g ^ H.index ∈ H

Tactic:
letI := fintypeOfIndexNeZero hH

Result:
case neg
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
⊢ g ^ H.index ∈ H

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
f : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)) → ↥(zpowers g) :=
  fun q => ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x => g • x) q.out
hf : ∀ (q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))), f q ∈ H.subgroupOf (zpowers g)
key : ∏ c : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), f c ∈ H.subgroupOf (zpowers g)
⊢ g ^ H.index ∈ H

Tactic:
simpa only [f, minimalPeriod_eq_card, Finset.prod_pow_eq_pow_sum, Fintype.card_sigma,
  Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)), index_eq_card,
  Nat.card_eq_fintype_card] using key

Result:
no goals