-- Mathlib/GroupTheory/Schreier.lean
theorem card_commutator_dvd_index_center_pow [Finite (commutatorSet G)] :
    Nat.card (_root_.commutator G) ∣
      (center G).index ^ ((center G).index * Nat.card (commutatorSet G) + 1)

Proof state:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : (center G).index = 0
⊢ Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)

Tactic:
simp_rw [hG, zero_mul, zero_add, pow_one, dvd_zero]

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝ : (center G).FiniteIndex
h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index
this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
h3 :
  (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤
    (center G).index * Nat.card ↑(commutatorSet G)
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))

Tactic:
refine dvd_trans ?_ (pow_dvd_pow (center G).index (h2.trans h3))

Result:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝ : (center G).FiniteIndex
h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index
this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
h3 :
  (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤
    (center G).index * Nat.card ↑(commutatorSet G)
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ Group.rank ↥((center G).subgroupOf (_root_.commutator G))

Proof state:
case neg.hG
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝¹ : (center G).FiniteIndex
h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index
this✝ : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
h3 :
  (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤
    (center G).index * Nat.card ↑(commutatorSet G)
g : ↥((center G).subgroupOf (_root_.commutator G))
this : ↑↑g ∈ (MonoidHom.transferCenterPow G).ker
⊢ g ^ (center G).index = 1

Tactic:
simpa only [MonoidHom.mem_ker, Subtype.ext_iff] using this

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this : (center G).FiniteIndex
h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) * ((center G).subgroupOf (_root_.commutator G)).index ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G)) * (center G).index

Tactic:
refine mul_dvd_mul ?_ h1

Result:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this : (center G).FiniteIndex
h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)

Tactic:
by_cases hG : (center G).index = 0

Result:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : (center G).index = 0
⊢ Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)

case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
⊢ Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)

Proof state:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝ : (center G).FiniteIndex
h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index
this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
h3 :
  (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤
    (center G).index * Nat.card ↑(commutatorSet G)
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ Group.rank ↥((center G).subgroupOf (_root_.commutator G))

Tactic:
apply card_dvd_exponent_pow_rank'

Result:
case neg.hG
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝ : (center G).FiniteIndex
h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index
this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
h3 :
  (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤
    (center G).index * Nat.card ↑(commutatorSet G)
⊢ ∀ (g : ↥((center G).subgroupOf (_root_.commutator G))), g ^ (center G).index = 1

Proof state:
case neg.hG
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝ : (center G).FiniteIndex
h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index
this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
h3 :
  (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤
    (center G).index * Nat.card ↑(commutatorSet G)
⊢ ∀ (g : ↥((center G).subgroupOf (_root_.commutator G))), g ^ (center G).index = 1

Tactic:
intro g

Result:
case neg.hG
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝ : (center G).FiniteIndex
h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index
this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
h3 :
  (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤
    (center G).index * Nat.card ↑(commutatorSet G)
g : ↥((center G).subgroupOf (_root_.commutator G))
⊢ g ^ (center G).index = 1

Proof state:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this : (center G).FiniteIndex
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) * ((center G).subgroupOf (_root_.commutator G)).index ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G)) * (center G).index

Tactic:
have h1 := relindex_dvd_index_of_normal (center G) (_root_.commutator G)

Result:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this : (center G).FiniteIndex
h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) * ((center G).subgroupOf (_root_.commutator G)).index ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G)) * (center G).index