[GOAL]
G : Type u
inst✝ : Group G
⊢ commutator G = Subgroup.closure (commutatorSet G)
[PROOFSTEP]
simp [commutator, Subgroup.commutator_def, commutatorSet]
[GOAL]
G : Type u
inst✝ : Group G
⊢ commutator G = Subgroup.normalClosure (commutatorSet G)
[PROOFSTEP]
simp [commutator, Subgroup.commutator_def', commutatorSet]
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.FG { x // x ∈ commutator G }
[PROOFSTEP]
rw [commutator_eq_closure]
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.FG { x // x ∈ Subgroup.closure (commutatorSet G) }
[PROOFSTEP]
apply Group.closure_finite_fg
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ commutator G } ≤ Nat.card ↑(commutatorSet G)
[PROOFSTEP]
rw [Subgroup.rank_congr (commutator_eq_closure G)]
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ Subgroup.closure (commutatorSet G) } ≤ Nat.card ↑(commutatorSet G)
[PROOFSTEP]
apply Subgroup.rank_closure_finite_le_nat_card
[GOAL]
G : Type u
inst✝ : Group G
⊢ ⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆ ≤ Subgroup.center G
[PROOFSTEP]
rw [← Subgroup.centralizer_univ, ← Subgroup.coe_top, ← Subgroup.commutator_eq_bot_iff_le_centralizer]
[GOAL]
G : Type u
inst✝ : Group G
⊢ ⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥
[PROOFSTEP]
suffices ⁅⁅⊤, centralizer (commutator G : Set G)⁆, centralizer (commutator G : Set G)⁆ = ⊥
  by
  refine' Subgroup.commutator_commutator_eq_bot_of_rotate _ this
  rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]
[GOAL]
G : Type u
inst✝ : Group G
this : ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
⊢ ⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥
[PROOFSTEP]
refine' Subgroup.commutator_commutator_eq_bot_of_rotate _ this
[GOAL]
G : Type u
inst✝ : Group G
this : ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
⊢ ⁅⁅centralizer ↑(commutator G), ⊤⁆, centralizer ↑(commutator G)⁆ = ⊥
[PROOFSTEP]
rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]
[GOAL]
G : Type u
inst✝ : Group G
⊢ ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
[PROOFSTEP]
rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]
[GOAL]
G : Type u
inst✝ : Group G
⊢ centralizer ↑(commutator G) ≤ centralizer ↑⁅⊤, centralizer ↑(commutator G)⁆
[PROOFSTEP]
exact Set.centralizer_subset (Subgroup.commutator_mono le_top le_top)
[GOAL]
G : Type u
inst✝ : Group G
src✝ : Group (G ⧸ commutator G) := QuotientGroup.Quotient.group (commutator G)
x y : Abelianization G
a b : G
⊢ ⁅b⁻¹, a⁻¹⁆ = ((fun x x_1 => x * x_1) a b)⁻¹ * (fun x x_1 => x * x_1) b a
[PROOFSTEP]
group
[GOAL]
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutator G ≤ MonoidHom.ker f
[PROOFSTEP]
rw [commutator_eq_closure, Subgroup.closure_le]
[GOAL]
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutatorSet G ⊆ ↑(MonoidHom.ker f)
[PROOFSTEP]
rintro x ⟨p, q, rfl⟩
[GOAL]
case intro.intro
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
p q : G
⊢ ⁅p, q⁆ ∈ ↑(MonoidHom.ker f)
[PROOFSTEP]
simp [MonoidHom.mem_ker, mul_right_comm (f p) (f q), commutatorElement_def]
[GOAL]
G : Type u
inst✝² inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
⊢ Function.LeftInverse ↑(Abelianization.map (toMonoidHom (symm e))) ↑(Abelianization.map (toMonoidHom e))
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
G : Type u
inst✝² inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
x✝ : Abelianization G
a : G
⊢ ↑(Abelianization.map (toMonoidHom (symm e))) (↑(Abelianization.map (toMonoidHom e)) (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
[PROOFSTEP]
simp
[GOAL]
G : Type u
inst✝² inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
⊢ Function.RightInverse ↑(Abelianization.map (toMonoidHom (symm e))) ↑(Abelianization.map (toMonoidHom e))
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
G : Type u
inst✝² inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
x✝ : Abelianization H
a : H
⊢ ↑(Abelianization.map (toMonoidHom e)) (↑(Abelianization.map (toMonoidHom (symm e))) (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
[PROOFSTEP]
simp
[GOAL]
G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : CommGroup H
src✝ : H →* Abelianization H := of
⊢ Function.RightInverse ↑(↑lift (MonoidHom.id H)) ↑of
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : CommGroup H
src✝ : H →* Abelianization H := of
x✝ : Abelianization H
a : H
⊢ ↑of (↑(↑lift (MonoidHom.id H)) (Quot.mk Setoid.r a)) = Quot.mk Setoid.r a
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ closureCommutatorRepresentatives G } ≤ 2 * Nat.card ↑(commutatorSet G)
[PROOFSTEP]
rw [two_mul]
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ closureCommutatorRepresentatives G } ≤ Nat.card ↑(commutatorSet G) + Nat.card ↑(commutatorSet G)
[PROOFSTEP]
exact
  (Subgroup.rank_closure_finite_le_nat_card _).trans
    ((Set.card_union_le _ _).trans
      (add_le_add ((Finite.card_image_le _).trans (Finite.card_range_le _))
        ((Finite.card_image_le _).trans (Finite.card_range_le _))))
[GOAL]
G : Type u
inst✝ : Group G
⊢ ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
      commutatorSet { x // x ∈ closureCommutatorRepresentatives G } =
    commutatorSet G
[PROOFSTEP]
apply Set.Subset.antisymm
[GOAL]
case h₁
G : Type u
inst✝ : Group G
⊢ ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
      commutatorSet { x // x ∈ closureCommutatorRepresentatives G } ⊆
    commutatorSet G
[PROOFSTEP]
rintro - ⟨-, ⟨g₁, g₂, rfl⟩, rfl⟩
[GOAL]
case h₁.intro.intro.intro.intro
G : Type u
inst✝ : Group G
g₁ g₂ : { x // x ∈ closureCommutatorRepresentatives G }
⊢ ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ⁅g₁, g₂⁆ ∈ commutatorSet G
[PROOFSTEP]
exact ⟨g₁, g₂, rfl⟩
[GOAL]
case h₂
G : Type u
inst✝ : Group G
⊢ commutatorSet G ⊆
    ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
      commutatorSet { x // x ∈ closureCommutatorRepresentatives G }
[PROOFSTEP]
exact fun g hg =>
  ⟨_,
    ⟨⟨_, subset_closure (Or.inl ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩)⟩, ⟨_, subset_closure (Or.inr ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩)⟩, rfl⟩,
    hg.choose_spec.choose_spec⟩
[GOAL]
G : Type u
inst✝ : Group G
⊢ Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) = Nat.card ↑(commutatorSet G)
[PROOFSTEP]
rw [← image_commutatorSet_closureCommutatorRepresentatives G]
[GOAL]
G : Type u
inst✝ : Group G
⊢ Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) =
    Nat.card
      ↑(↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
          commutatorSet { x // x ∈ closureCommutatorRepresentatives G })
[PROOFSTEP]
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))
[GOAL]
G : Type u
inst✝ : Group G
⊢ Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } =
    Nat.card { x // x ∈ _root_.commutator G }
[PROOFSTEP]
rw [commutator_eq_closure G, ← image_commutatorSet_closureCommutatorRepresentatives, ← MonoidHom.map_closure, ←
  commutator_eq_closure]
[GOAL]
G : Type u
inst✝ : Group G
⊢ Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } =
    Nat.card
      { x //
        x ∈
          map (Subgroup.subtype (closureCommutatorRepresentatives G))
            (_root_.commutator { x // x ∈ closureCommutatorRepresentatives G }) }
[PROOFSTEP]
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Finite ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G })
[PROOFSTEP]
apply Nat.finite_of_card_ne_zero
[GOAL]
case h
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) ≠ 0
[PROOFSTEP]
rw [card_commutatorSet_closureCommutatorRepresentatives]
[GOAL]
case h
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card ↑(commutatorSet G) ≠ 0
[PROOFSTEP]
exact Finite.card_pos.ne'
