awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ (pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆) ≤ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
have rw : ∀ (i : η), map (MonoidHom.mulSingle Gs i) ⁅H i, K i⁆ ≤ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
Tactic: rw [pi_le_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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
⊢ 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⁆
have 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⁆
Tactic: rw [map_commutator]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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
⊢ 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⁆
have h₁ : map (MonoidHom.mulSingle Gs i) (H i) ≤ pi (f := Gs) Set.univ H
Tactic: apply commutator_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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
⊢ 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⁆
have h₂ : map (MonoidHom.mulSingle Gs i) (K i) ≤ pi (f := Gs) Set.univ K
Tactic: apply commutator_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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
⊢ map (MonoidHom.mulSingle Gs i) (H i) ≤ pi (f := Gs) Set.univ H
have 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))
Tactic: rw [le_pi_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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))
⊢ 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)
have 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)
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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)
have 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)
Tactic: subst h
Cleared hypotheses: i, x, hx, h
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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
⊢ map (MonoidHom.mulSingle Gs i) (K i) ≤ pi (f := Gs) Set.univ K
have 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))
Tactic: rw [le_pi_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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))
⊢ 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)
have 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)
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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)
have 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)
Tactic: subst h
Cleared hypotheses: i, x, hx, h
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆ = pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆
have apply : (pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆) ≤ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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⁆
⊢ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆ = pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆
have apply₁ : ∀ (i : η), map (MonoidHom.mulSingle Gs i) ⁅H i, K i⁆ ≤ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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⁆
⊢ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆ = pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆
have 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⁆
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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⁆
⊢ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆ = pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆
have 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⁆
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Group.FG.{u_1} ↥(_root_.commutator G)
have rw : Group.FG.{u_1} ↥(closure (commutatorSet G))
Tactic: rw [commutator_eq_closure]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Group.rank.{u_1} ↥(_root_.commutator G) ≤ Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)
have rw : Group.rank.{u_1} ↥(closure (commutatorSet G)) ≤ Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)
Tactic: rw [Subgroup.rank_congr (commutator_eq_closure G)]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
inst_2 : Group.FG G
⊢ FiniteIndex (center G)
have obtain : ∀ (S : Finset G) (hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤), FiniteIndex (center G)
Tactic: obtain ⟨S, -, hS⟩ := Group.rank_spec G
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
inst_2 : Group.FG G
⊢ index (center G) ≤ Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ Group.rank G
have 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
Tactic: obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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} (↑(commutatorSet G) : Type u_1) ^ Group.rank G
have rw : index (center G) ≤ Nat.card.{u_1} ((↑(↑S : Set G) : Type u_1) → (↑(commutatorSet G) : Type u_1))
Tactic: rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) =
    Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)
have 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)
Tactic: rw [← image_commutatorSet_closureCommutatorRepresentatives G]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) = Nat.card.{u_1} ↥(_root_.commutator G)
have 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)))
Tactic: rw [commutator_eq_closure G, ← image_commutatorSet_closureCommutatorRepresentatives, ←
    MonoidHom.map_closure, ← commutator_eq_closure]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
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) ≤ 2 * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)
have 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)
Tactic: rw [two_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Finite.{u_1 + 1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1)
have h : Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) ≠ 0
Tactic: apply Nat.finite_of_card_ne_zero
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) ≠ 0
have h : Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ≠ 0
Tactic: rw [card_commutatorSet_closureCommutatorRepresentatives]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
M' : Type u_2
inst_1 : Mul M'
⊢ commProb (M × M') = commProb M * commProb M'
have 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)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
M' : Type u_2
inst_1 : Mul M'
⊢ (↑(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)
have 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 })
Tactic: congr 2
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
α : Type u_2
i : α → Type u_3
inst : Fintype α
inst_1 : (a : α) → Mul (i a)
⊢ commProb ((a : α) → i a) = ∏ a : α, commProb.{u_3} (i a)
have simp_rw : (↑(Nat.card { p : ((a : α) → i a) × ((a : α) → i a) // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x }) : ℚ) /
    HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card ((a : α) → i a)) : ℚ) 2 =
  (↑(Nat.card ((a : α) → { p : i a × i a // p.1 * p.2 = p.2 * p.1 })) : ℚ) /
    HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card ((a : α) → i a)) : ℚ) 2
Tactic: simp_rw [commProb_def, Finset.prod_div_distrib, Finset.prod_pow, ← Nat.cast_prod,
    ← Nat.card_pi, Commute, SemiconjBy, funext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
α : Type u_2
i : α → Type u_3
inst : Fintype α
inst_1 : (a : α) → Mul (i a)
⊢ (↑(Nat.card { p : ((a : α) → i a) × ((a : α) → i a) // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x }) : ℚ) /
      HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card ((a : α) → i a)) : ℚ) 2 =
    (↑(Nat.card ((a : α) → { p : i a × i a // p.1 * p.2 = p.2 * p.1 })) : ℚ) /
      HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card ((a : α) → i a)) : ℚ) 2
have e_a : Nat.card { p : ((a : α) → i a) × ((a : α) → i a) // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x } =
  Nat.card ((a : α) → { p : i a × i a // p.1 * p.2 = p.2 * p.1 })
Tactic: congr 2
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Mul β
⊢ commProb (α → β) = commProb β ^ card α
have rw : ∏ a : α, commProb β = commProb β ^ card α
Tactic: rw [commProb_pi, Finset.prod_const, Finset.card_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Mul β
rw : ∏ a : α, commProb β = commProb β ^ card α
⊢ commProb (α → β) = commProb β ^ card α
have rw₁ : commProb β ^ Finset.card.{u_2} (α := α) Finset.univ = commProb β ^ card α
Tactic: rw [commProb_pi, Finset.prod_const, Finset.card_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Mul β
rw : ∏ a : α, commProb β = commProb β ^ card α
rw₁ : commProb β ^ Finset.card.{u_2} (α := α) Finset.univ = commProb β ^ card α
⊢ commProb (α → β) = commProb β ^ card α
have rw₂ : commProb β ^ card α = commProb β ^ card α
Tactic: rw [commProb_pi, Finset.prod_const, Finset.card_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
⊢ commProb M ≤ 1
have refine : (↑(Nat.card.{u_1} { p : M × M // Commute p.1 p.2 }) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M) : ℚ) 2
Tactic: refine div_le_one_of_le₀ ?_ (sq_nonneg (Nat.card M : ℚ))
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
⊢ (↑(Nat.card.{u_1} { p : M × M // Commute p.1 p.2 }) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M) : ℚ) 2
have norm_cast : Nat.card.{u_1} { p : M × M // Commute p.1 p.2 } ≤ HPow.hPow (β := ℕ) (Nat.card M) 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
⊢ Nat.card.{u_1} { p : M × M // Commute p.1 p.2 } ≤ HPow.hPow (β := ℕ) (Nat.card M) 2
have rw : Nat.card.{u_1} { p : M × M // Commute p.1 p.2 } ≤ Nat.card.{u_1} (M × M)
Tactic: rw [sq, ← Nat.card_prod]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
⊢ commProb M = 1 ↔ IsMulCommutative M
have haveI : ∀ (this : Fintype M), commProb M = 1 ↔ IsMulCommutative M
Tactic: haveI := Fintype.ofFinite M
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
this : Fintype M
⊢ commProb M = 1 ↔ IsMulCommutative M
have rw : (↑(card.{u_1} (↑{x : M × M | Commute x.1 x.2} : Type u_1)) : ℚ) / HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 = 1 ↔
  IsMulCommutative M
Tactic: rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
this : Fintype M
⊢ (↑(card.{u_1} (↑{x : M × M | Commute x.1 x.2} : Type u_1)) : ℚ) / HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 = 1 ↔
    IsMulCommutative M
have rw : (∀ (x : M × M), Membership.mem (γ := Set (M × M)) {x : M × M | Commute x.1 x.2} x) ↔ IsMulCommutative M
Tactic: rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod,
    set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
this : Fintype M
rw : (∀ (x : M × M), Membership.mem (γ := Set (M × M)) {x : M × M | Commute x.1 x.2} x) ↔ IsMulCommutative M
⊢ (↑(card.{u_1} (↑{x : M × M | Commute x.1 x.2} : Type u_1)) : ℚ) / HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 = 1 ↔
    IsMulCommutative M
have rw₁ : HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 ≠ 0
Tactic: rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod,
    set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall]