case pos
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : index (center G) = 0
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)

case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
by_cases hG : (center G).index = 0
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
haveI : FiniteIndex (center G) := ⟨hG⟩
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } *
      index (subgroupOf (center G) (_root_.commutator G)) ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G)) * index (center G)
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
rw [← ((center G).subgroupOf (_root_.commutator G)).card_mul_index, pow_succ']
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } *
      index (subgroupOf (center G) (_root_.commutator G)) ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G)) * index (center G)
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } *
      index (subgroupOf (center G) (_root_.commutator G)) ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G)) * index (center G)
have h1 := relindex_dvd_index_of_normal (center G) (_root_.commutator G)
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } *
      index (subgroupOf (center G) (_root_.commutator G)) ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G)) * index (center G)
refine' mul_dvd_mul _ h1
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
haveI : FiniteIndex ((center G).subgroupOf (_root_.commutator G)) :=
  ⟨ne_zero_of_dvd_ne_zero hG h1⟩
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
have h2 := rank_le_index_mul_rank ((center G).subgroupOf (_root_.commutator G))
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
have h3 := Nat.mul_le_mul (Nat.le_of_dvd (Nat.pos_of_ne_zero hG) h1) (rank_commutator_le_card G)
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
refine' dvd_trans _ (pow_dvd_pow (center G).index (h2.trans h3))
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ ∀ (g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }), g ^ index (center G) = 1
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
apply card_dvd_exponent_pow_rank'
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
⊢ g ^ index (center G) = 1
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ ∀ (g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }), g ^ index (center G) = 1
intro g
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝¹ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this✝ : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
this : ↑↑g ∈ MonoidHom.ker (MonoidHom.transferCenterPow G)
⊢ g ^ index (center G) = 1
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
⊢ g ^ index (center G) = 1
have := Abelianization.commutator_subset_ker (MonoidHom.transferCenterPow G) g.1.2
no goals
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝¹ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this✝ : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
this : ↑↑g ∈ MonoidHom.ker (MonoidHom.transferCenterPow G)
⊢ g ^ index (center G) = 1
simpa only [MonoidHom.mem_ker, Subtype.ext_iff] using this
no goals
case pos
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : index (center G) = 0
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
simp_rw [hG, MulZeroClass.zero_mul, zero_add, pow_one, dvd_zero]