case h₁
G : Type u
inst✝ : Group G
⊢ ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
      commutatorSet { x // x ∈ closureCommutatorRepresentatives G } ⊆
    commutatorSet G

case h₂
G : Type u
inst✝ : Group G
⊢ commutatorSet G ⊆
    ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
      commutatorSet { x // x ∈ closureCommutatorRepresentatives G }
G : Type u
inst✝ : Group G
⊢ ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
      commutatorSet { x // x ∈ closureCommutatorRepresentatives G } =
    commutatorSet G
apply Set.Subset.antisymm
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
case h₁
G : Type u
inst✝ : Group G
⊢ ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
      commutatorSet { x // x ∈ closureCommutatorRepresentatives G } ⊆
    commutatorSet G
rintro - ⟨-, ⟨g₁, g₂, rfl⟩, rfl⟩
no goals
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
exact ⟨g₁, g₂, rfl⟩
no goals
case h₂
G : Type u
inst✝ : Group G
⊢ commutatorSet G ⊆
    ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
      commutatorSet { x // x ∈ closureCommutatorRepresentatives G }
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⟩