G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) ^
      Group.rank { x // x ∈ closureCommutatorRepresentatives G }
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
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 } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
have h1 := index_center_le_pow (closureCommutatorRepresentatives G)
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) ^
      Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) *
          Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) +
        1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) ^
      Group.rank { x // x ∈ closureCommutatorRepresentatives G }
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
have h2 := card_commutator_dvd_index_center_pow (closureCommutatorRepresentatives G)
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) ^
      Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) *
          Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) +
        1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
rw [card_commutatorSet_closureCommutatorRepresentatives] at h1 h2
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
rw [card_commutator_closureCommutatorRepresentatives] at h2
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
replace h1 :=
  h1.trans
    (Nat.pow_le_pow_of_le_right Finite.card_pos (rank_closureCommutatorRepresentatives_le G))
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G)) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
replace h2 := h2.trans (pow_dvd_pow _ (add_le_add_right (mul_le_mul_right' h1 _) 1))
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G)) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
rw [← pow_succ'] at h2
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ 0 <
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
refine' (Nat.le_of_dvd _ h2).trans (Nat.pow_le_pow_of_le_left h1 _)
no goals
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ 0 <
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
exact pow_pos (Nat.pos_of_ne_zero FiniteIndex.finiteIndex) _