-- 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 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:
have := Abelianization.commutator_subset_ker (MonoidHom.transferCenterPow G) g.1.2

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))
this : ↑↑g ∈ (MonoidHom.transferCenterPow G).ker
⊢ 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
⊢ Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)

Tactic:
haveI : FiniteIndex (center G) := ⟨hG⟩

Result:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this : (center G).FiniteIndex
⊢ 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)
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))

Tactic:
have h3 := Nat.mul_le_mul (Nat.le_of_dvd (Nat.pos_of_ne_zero hG) h1) (rank_commutator_le_card 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
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))

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).index ^ ((center G).index * Nat.card ↑(commutatorSet G))

Tactic:
haveI : FiniteIndex ((center G).subgroupOf (_root_.commutator G)) :=
  ⟨ne_zero_of_dvd_ne_zero hG 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
this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))

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 ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)

Tactic:
rw [← ((center G).subgroupOf (_root_.commutator G)).card_mul_index, pow_succ]

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

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
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))

Tactic:
have h2 := rank_le_index_mul_rank ((center G).subgroupOf (_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
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)
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))