awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
rw :
  Membership.mem (γ := Subgroup ((i : η) → Gs i))
      (Bracket.bracket (L := Subgroup ((i : η) → Gs i)) (map (MonoidHom.mulSingle Gs i) (H i))
        (map (MonoidHom.mulSingle Gs i) (K i)))
      hi →
    hi ∈ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
⊢ Membership.mem (γ := Subgroup ((i : η) → Gs i)) (map (MonoidHom.mulSingle Gs i) ⁅H i, K i⁆) hi →
    hi ∈ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆

Tactic:
rw [map_commutator]

Premises used: Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
h₁ : map (MonoidHom.mulSingle Gs i) (H i) ≤ pi (f := Gs) Set.univ H
h₂ : map (MonoidHom.mulSingle Gs i) (K i) ≤ pi (f := Gs) Set.univ K
⊢ Membership.mem (γ := Subgroup ((i : η) → Gs i))
      (Bracket.bracket (L := Subgroup ((i : η) → Gs i)) (map (MonoidHom.mulSingle Gs i) (H i))
        (map (MonoidHom.mulSingle Gs i) (K i)))
      hi →
    hi ∈ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆

Tactic:
apply commutator_mono

Premises used: Subgroup.commutator_mono
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
h₁ :
  ∀ (i_1 : η),
    Membership.mem (γ := Set η) Set.univ i_1 →
      LE.le (α := Subgroup ((i : η) → Gs i)) (map (MonoidHom.mulSingle Gs i) (H i))
        (comap (Pi.evalMonoidHom Gs i_1) (H i_1))
⊢ map (MonoidHom.mulSingle Gs i) (H i) ≤ pi (f := Gs) Set.univ H

Tactic:
rw [le_pi_iff]

Premises used: Subgroup.le_pi_iff
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : Membership.mem (γ := Set η) Set.univ j
x : Gs i
hx : x ∈ (↑(H i) : Set (Gs i))
pos :
  ∀ (h : j = i),
    Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (H j))
      (((MonoidHom.mulSingle Gs i : Gs i →* (i : η) → Gs i) : (a : Gs i) → (i : η) → Gs i) x : (i : η) → Gs i)
neg :
  ∀ (h : ¬j = i),
    Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (H j))
      (((MonoidHom.mulSingle Gs i : Gs i →* (i : η) → Gs i) : (a : Gs i) → (i : η) → Gs i) x : (i : η) → Gs i)
⊢ Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (H j))
    (((MonoidHom.mulSingle Gs i : Gs i →* (i : η) → Gs i) : (a : Gs i) → (i : η) → Gs i) x : (i : η) → Gs i)

Tactic:
by_cases h : j = i
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : Membership.mem (γ := Set η) Set.univ j
x : Gs i
hx : x ∈ (↑(H i) : Set (Gs i))
h : j = i
pos :
  ∀ (x : Gs j) (hx : x ∈ (↑(H j) : Set (Gs j))),
    Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (H j))
      (((MonoidHom.mulSingle Gs j : Gs j →* (i : η) → Gs i) : (a : Gs j) → (i : η) → Gs i) x : (i : η) → Gs i)
⊢ Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (H j))
    (((MonoidHom.mulSingle Gs i : Gs i →* (i : η) → Gs i) : (a : Gs i) → (i : η) → Gs i) x : (i : η) → Gs i)

Tactic:
subst h
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : Membership.mem (γ := Set η) Set.univ j
x : Gs j
hx : x ∈ (↑(H j) : Set (Gs j))
⊢ Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (H j))
    (((MonoidHom.mulSingle Gs j : Gs j →* (i : η) → Gs i) : (a : Gs j) → (i : η) → Gs i) x : (i : η) → Gs i)

Tactic:
simpa using hx
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : Membership.mem (γ := Set η) Set.univ j
x : Gs i
hx : x ∈ (↑(H i) : Set (Gs i))
h : ¬j = i
⊢ Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (H j))
    (((MonoidHom.mulSingle Gs i : Gs i →* (i : η) → Gs i) : (a : Gs i) → (i : η) → Gs i) x : (i : η) → Gs i)

Tactic:
simp [h, one_mem]

Premises used: OneMemClass.one_mem
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
h₂ :
  ∀ (i_1 : η),
    Membership.mem (γ := Set η) Set.univ i_1 →
      LE.le (α := Subgroup ((i : η) → Gs i)) (map (MonoidHom.mulSingle Gs i) (K i))
        (comap (Pi.evalMonoidHom Gs i_1) (K i_1))
⊢ map (MonoidHom.mulSingle Gs i) (K i) ≤ pi (f := Gs) Set.univ K

Tactic:
rw [le_pi_iff]

Premises used: Subgroup.le_pi_iff
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : Membership.mem (γ := Set η) Set.univ j
x : Gs i
hx : x ∈ (↑(K i) : Set (Gs i))
pos :
  ∀ (h : j = i),
    Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (K j))
      (((MonoidHom.mulSingle Gs i : Gs i →* (i : η) → Gs i) : (a : Gs i) → (i : η) → Gs i) x : (i : η) → Gs i)
neg :
  ∀ (h : ¬j = i),
    Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (K j))
      (((MonoidHom.mulSingle Gs i : Gs i →* (i : η) → Gs i) : (a : Gs i) → (i : η) → Gs i) x : (i : η) → Gs i)
⊢ Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (K j))
    (((MonoidHom.mulSingle Gs i : Gs i →* (i : η) → Gs i) : (a : Gs i) → (i : η) → Gs i) x : (i : η) → Gs i)

Tactic:
by_cases h : j = i
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : Membership.mem (γ := Set η) Set.univ j
x : Gs i
hx : x ∈ (↑(K i) : Set (Gs i))
h : j = i
pos :
  ∀ (x : Gs j) (hx : x ∈ (↑(K j) : Set (Gs j))),
    Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (K j))
      (((MonoidHom.mulSingle Gs j : Gs j →* (i : η) → Gs i) : (a : Gs j) → (i : η) → Gs i) x : (i : η) → Gs i)
⊢ Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (K j))
    (((MonoidHom.mulSingle Gs i : Gs i →* (i : η) → Gs i) : (a : Gs i) → (i : η) → Gs i) x : (i : η) → Gs i)

Tactic:
subst h
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : Membership.mem (γ := Set η) Set.univ j
x : Gs j
hx : x ∈ (↑(K j) : Set (Gs j))
⊢ Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (K j))
    (((MonoidHom.mulSingle Gs j : Gs j →* (i : η) → Gs i) : (a : Gs j) → (i : η) → Gs i) x : (i : η) → Gs i)

Tactic:
simpa using hx
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : Membership.mem (γ := Set η) Set.univ j
x : Gs i
hx : x ∈ (↑(K i) : Set (Gs i))
h : ¬j = i
⊢ Membership.mem (α := (i : η) → Gs i) (γ := Subgroup ((i : η) → Gs i)) (comap (Pi.evalMonoidHom Gs j) (K j))
    (((MonoidHom.mulSingle Gs i : Gs i →* (i : η) → Gs i) : (a : Gs i) → (i : η) → Gs i) x : (i : η) → Gs i)

Tactic:
simp [h, one_mem]

Premises used: OneMemClass.one_mem
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
apply : (pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆) ≤ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
apply₁ : ∀ (i : η), map (MonoidHom.mulSingle Gs i) ⁅H i, K i⁆ ≤ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
apply₂ :
  ∀ (i : η) ⦃hi : (i : η) → Gs i⦄,
    Membership.mem (γ := Subgroup ((i : η) → Gs i)) (map (MonoidHom.mulSingle Gs i) ⁅H i, K i⁆) hi →
      hi ∈ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
apply₃ :
  ∀ (i : η) ⦃hi : (i : η) → Gs i⦄,
    Membership.mem (γ := Subgroup ((i : η) → Gs i))
        (Bracket.bracket (L := Subgroup ((i : η) → Gs i)) (map (MonoidHom.mulSingle Gs i) (H i))
          (map (MonoidHom.mulSingle Gs i) (K i)))
        hi →
      hi ∈ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
⊢ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆ = pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆

Tactic:
classical
    apply le_antisymm (commutator_pi_pi_le H K)
    rw [pi_le_iff]
    intro i hi
    rw [map_commutator]
    apply commutator_mono <;>
      · rw [le_pi_iff]
        intro j _hj
        rintro _ ⟨x, hx, rfl⟩
        by_cases h : j = i
        · subst h
          simpa using hx
        · simp [h, one_mem]

Premises used: Subgroup.pi_le_iff, Subgroup.commutator_mono, Subgroup.le_pi_iff, Subgroup.commutator_pi_pi_le, le_antisymm, OneMemClass.one_mem, Subgroup.map_commutator, rfl
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
rw : Group.FG.{u_1} ↥(closure (commutatorSet G))
⊢ Group.FG.{u_1} ↥(_root_.commutator G)

Tactic:
rw [commutator_eq_closure]

Premises used: commutator_eq_closure
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Group.FG.{u_1} ↥(closure (commutatorSet G))

Tactic:
apply Group.closure_finite_fg

Premises used: Group.closure_finite_fg
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
rw : Group.rank.{u_1} ↥(closure (commutatorSet G)) ≤ Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)
⊢ Group.rank.{u_1} ↥(_root_.commutator G) ≤ Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)

Tactic:
rw [Subgroup.rank_congr (commutator_eq_closure G)]

Premises used: commutator_eq_closure, Subgroup.rank_congr
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Group.rank.{u_1} ↥(closure (commutatorSet G)) ≤ Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)

Tactic:
apply Subgroup.rank_closure_finite_le_nat_card

Premises used: Subgroup.rank_closure_finite_le_nat_card
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
inst_2 : Group.FG G
obtain : ∀ (S : Finset G) (hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤), FiniteIndex (center G)
⊢ FiniteIndex (center G)

Tactic:
obtain ⟨S, -, hS⟩ := Group.rank_spec G

Premises used: Group.rank_spec
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
inst_2 : Group.FG G
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
⊢ FiniteIndex (center G)

Tactic:
⟨mt (Finite.card_eq_zero_of_embedding (quotientCenterEmbedding hS)) Finite.card_pos.ne'⟩

Premises used: Subgroup.quotientCenterEmbedding, mt, Finite.card_eq_zero_of_embedding, Finite.card_pos, LT.lt.ne', Subgroup.FiniteIndex.mk
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
inst_2 : Group.FG G
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
⊢ FiniteIndex (center G)

Tactic:
exact ⟨mt (Finite.card_eq_zero_of_embedding (quotientCenterEmbedding hS)) Finite.card_pos.ne'⟩
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
inst_2 : Group.FG G
obtain :
  ∀ (S : Finset G) (hS1 : S.card = Group.rank G) (hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤),
    index (center G) ≤ Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ Group.rank G
⊢ index (center G) ≤ Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ Group.rank G

Tactic:
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G

Premises used: Group.rank_spec
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
inst_2 : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
rw : index (center G) ≤ Nat.card.{u_1} ((↑(↑S : Set G) : Type u_1) → (↑(commutatorSet G) : Type u_1))
⊢ index (center G) ≤ Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ Group.rank G

Tactic:
rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]

Premises used: Finset.coe_sort_coe, Nat.card_fun, Fintype.card_coe, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
inst_2 : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
⊢ index (center G) ≤ Nat.card.{u_1} ((↑(↑S : Set G) : Type u_1) → (↑(commutatorSet G) : Type u_1))

Tactic:
Finite.card_le_of_embedding (quotientCenterEmbedding hS2)

Premises used: Subgroup.quotientCenterEmbedding, Subgroup.index, Finite.card_le_of_embedding
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
inst_2 : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
⊢ index (center G) ≤ Nat.card.{u_1} ((↑(↑S : Set G) : Type u_1) → (↑(commutatorSet G) : Type u_1))

Tactic:
exact Finite.card_le_of_embedding (quotientCenterEmbedding hS2)

Premises used: Subgroup.quotientCenterEmbedding, Finite.card_le_of_embedding
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
rw :
  Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) =
    Nat.card.{u_1}
      (↑(Set.image (α := ↥(closureCommutatorRepresentatives G))
            (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
            (commutatorSet ↥(closureCommutatorRepresentatives G))) :
        Type u_1)
⊢ Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) =
    Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)

Tactic:
rw [← image_commutatorSet_closureCommutatorRepresentatives G]

Premises used: image_commutatorSet_closureCommutatorRepresentatives
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
⊢ Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) =
    Nat.card.{u_1}
      (↑(Set.image (α := ↥(closureCommutatorRepresentatives G))
            (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
            (commutatorSet ↥(closureCommutatorRepresentatives G))) :
        Type u_1)

Tactic:
Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
⊢ Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) =
    Nat.card.{u_1}
      (↑(Set.image (α := ↥(closureCommutatorRepresentatives G))
            (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
            (commutatorSet ↥(closureCommutatorRepresentatives G))) :
        Type u_1)

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
rw :
  Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) =
    Nat.card.{u_1}
      ↥(map (G := ↥(closureCommutatorRepresentatives G)) (Subgroup.subtype (closureCommutatorRepresentatives G))
          (_root_.commutator ↥(closureCommutatorRepresentatives G)))
⊢ Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) = Nat.card.{u_1} ↥(_root_.commutator G)

Tactic:
rw [commutator_eq_closure G, ← image_commutatorSet_closureCommutatorRepresentatives, ←
    MonoidHom.map_closure, ← commutator_eq_closure]

Premises used: commutator_eq_closure, MonoidHom.map_closure, image_commutatorSet_closureCommutatorRepresentatives
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
⊢ Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) =
    Nat.card.{u_1}
      ↥(map (G := ↥(closureCommutatorRepresentatives G)) (Subgroup.subtype (closureCommutatorRepresentatives G))
          (_root_.commutator ↥(closureCommutatorRepresentatives G)))

Tactic:
Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
⊢ Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) =
    Nat.card.{u_1}
      ↥(map (G := ↥(closureCommutatorRepresentatives G)) (Subgroup.subtype (closureCommutatorRepresentatives G))
          (_root_.commutator ↥(closureCommutatorRepresentatives G)))

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Finite.{u_1 + 1} (↑(commutatorRepresentatives G) : Type u_1)

Tactic:
Set.finite_coe_iff.mpr (Set.finite_range _)

Premises used: Iff.mpr, Set.finite_range, Set.finite_coe_iff
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Group.FG.{u_1} ↥(closureCommutatorRepresentatives G)

Tactic:
Group.closure_finite_fg _

Premises used: Set.Mem, closureCommutatorRepresentatives, Group.closure_finite_fg
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
rw :
  Group.rank.{u_1} ↥(closureCommutatorRepresentatives G) ≤
    Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) + Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)
⊢ Group.rank.{u_1} ↥(closureCommutatorRepresentatives G) ≤ 2 * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)

Tactic:
rw [two_mul]

Premises used: two_mul
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Group.rank.{u_1} ↥(closureCommutatorRepresentatives G) ≤
    Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) + Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)

Tactic:
(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 _))))

Premises used: Set.Mem, Subgroup.rank_closure_finite_le_nat_card, add_le_add, closureCommutatorRepresentatives, Set.card_union_le, Finite.card_image_le, LE.le.trans, Finite.card_range_le
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Group.rank.{u_1} ↥(closureCommutatorRepresentatives G) ≤
    Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) + Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)

Tactic:
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 _))))

Premises used: Subgroup.rank_closure_finite_le_nat_card, add_le_add, Set.card_union_le, Finite.card_image_le, LE.le.trans, Finite.card_range_le
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h : Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) ≠ 0
⊢ Finite.{u_1 + 1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1)

Tactic:
apply Nat.finite_of_card_ne_zero

Premises used: Nat.finite_of_card_ne_zero
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h : Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ≠ 0
⊢ Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) ≠ 0

Tactic:
rw [card_commutatorSet_closureCommutatorRepresentatives]

Premises used: card_commutatorSet_closureCommutatorRepresentatives
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ≠ 0

Tactic:
Finite.card_pos.ne'

Premises used: Finite.card_pos, LT.lt.ne'
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ≠ 0

Tactic:
exact Finite.card_pos.ne'

Premises used: Finite.card_pos, LT.lt.ne'
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
⊢ commProb M =
    (↑(Nat.card.{u_1} { p : M × M // Commute p.1 p.2 }) : ℚ) / HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M) : ℚ) 2

Tactic:
rfl

Premises used: commProb, rfl
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
M' : Type u_2
inst_1 : Mul M'
simp_rw :
  (↑(Nat.card { p : (M × M') × M × M' // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 }) : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M) : ℚ) 2 * HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M') : ℚ) 2) =
    (↑(Nat.card (Prod.{u_1, u_2} { p : M × M // p.1 * p.2 = p.2 * p.1 } { p : M' × M' // p.1 * p.2 = p.2 * p.1 })) :
        ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M) : ℚ) 2 * HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M') : ℚ) 2)
⊢ commProb (M × M') = commProb M * commProb M'

Tactic:
simp_rw [commProb_def, div_mul_div_comm, Nat.card_prod, Nat.cast_mul, mul_pow, ← Nat.cast_mul,
    ← Nat.card_prod, Commute, SemiconjBy, Prod.ext_iff]

Premises used: div_mul_div_comm, SemiconjBy, Commute, Prod.ext_iff, Nat.cast_mul, Nat.card_prod, mul_pow, commProb_def
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
M' : Type u_2
inst_1 : Mul M'
e_a :
  Nat.card { p : (M × M') × M × M' // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 } =
    Nat.card (Prod.{u_1, u_2} { p : M × M // p.1 * p.2 = p.2 * p.1 } { p : M' × M' // p.1 * p.2 = p.2 * p.1 })
⊢ (↑(Nat.card { p : (M × M') × M × M' // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 }) : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M) : ℚ) 2 * HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M') : ℚ) 2) =
    (↑(Nat.card (Prod.{u_1, u_2} { p : M × M // p.1 * p.2 = p.2 * p.1 } { p : M' × M' // p.1 * p.2 = p.2 * p.1 })) :
        ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M) : ℚ) 2 * HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M') : ℚ) 2)

Tactic:
congr 2