awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h1 :
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ≤
    Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) ^
      Group.rank.{u_1} ↥(closureCommutatorRepresentatives G)
h2 :
  Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣
    index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
        1)
⊢ Nat.card.{u_1} ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1))
have h1₁ : index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ≤
  Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ Group.rank.{u_1} ↥(closureCommutatorRepresentatives G)
Tactic: rw [card_commutatorSet_closureCommutatorRepresentatives] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h1 :
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ≤
    Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) ^
      Group.rank.{u_1} ↥(closureCommutatorRepresentatives G)
h2 :
  Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣
    index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
        1)
h1₁ :
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ≤
    Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ Group.rank.{u_1} ↥(closureCommutatorRepresentatives G)
⊢ Nat.card.{u_1} ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1))
have h2₁ : Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
    (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
        Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) +
      1)
Tactic: rw [card_commutatorSet_closureCommutatorRepresentatives] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h1 :
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ≤
    Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ Group.rank.{u_1} ↥(closureCommutatorRepresentatives G)
h2 :
  Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣
    index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) +
        1)
⊢ Nat.card.{u_1} ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1))
have h2₁ : Nat.card.{u_1} ↥(_root_.commutator G) ∣
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
    (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
        Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) +
      1)
Tactic: rw [card_commutator_closureCommutatorRepresentatives] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h1 :
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ≤
    Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ Group.rank.{u_1} ↥(closureCommutatorRepresentatives G)
h2 :
  Nat.card.{u_1} ↥(_root_.commutator G) ∣
    index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) +
        1)
⊢ Nat.card.{u_1} ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1))
have h1₁ : index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ≤
  Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ (2 * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1))
Tactic: replace h1 :=
    h1.trans
      (Nat.pow_le_pow_right Finite.card_pos (rank_closureCommutatorRepresentatives_le G))
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h2 :
  Nat.card.{u_1} ↥(_root_.commutator G) ∣
    index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) +
        1)
h1 :
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ≤
    Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ (2 * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1))
⊢ Nat.card.{u_1} ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1))
have h2₁ : Nat.card.{u_1} ↥(_root_.commutator G) ∣
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
    (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ (2 * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)) *
        Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) +
      1)
Tactic: replace h2 := h2.trans (pow_dvd_pow _ (add_le_add_left (mul_le_mul_left h1 _) 1))
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h1 :
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ≤
    Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ (2 * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1))
h2 :
  Nat.card.{u_1} ↥(_root_.commutator G) ∣
    index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ (2 * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1)) *
          Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) +
        1)
⊢ Nat.card.{u_1} ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1))
have h2₁ : Nat.card.{u_1} ↥(_root_.commutator G) ∣
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
    (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ (2 * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) + 1) + 1)
Tactic: rw [← pow_succ] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h1 :
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ≤
    Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ (2 * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1))
h2 :
  Nat.card.{u_1} ↥(_root_.commutator G) ∣
    index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ (2 * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) + 1) + 1)
⊢ Nat.card.{u_1} ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1))
have refine : 0 <
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
    (Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) ^ (2 * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) + 1) + 1)
Tactic: refine (Nat.le_of_dvd ?_ h2).trans (Nat.pow_le_pow_left h1 _)
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
⊢ Finite.{u_1 + 1} ↥(_root_.commutator G)
have h2 : Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
    (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
        Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
      1)
Tactic: have h2 := card_commutator_dvd_index_center_pow (closureCommutatorRepresentatives G)
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h2 :
  Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣
    index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
        1)
⊢ Finite.{u_1 + 1} ↥(_root_.commutator G)
have refine : ∀ (h : Nat.card.{u_1} ↥(_root_.commutator G) = 0), False
Tactic: refine Nat.finite_of_card_ne_zero fun h => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h2 :
  Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣
    index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
        1)
h : Nat.card.{u_1} ↥(_root_.commutator G) = 0
⊢ False
have h2₁ : index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
    (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
        Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
      1) =
  0
Tactic: rw [card_commutator_closureCommutatorRepresentatives, h, zero_dvd_iff] at h2
Cleared hypotheses: h2, h
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β x y : H.LeftTransversal
h : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y) 1
⊢ Eq (α := ↥H) (diff (MonoidHom.id ↥H) y x) 1
have rw : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y)⁻¹ 1
Tactic: rw [← diff_inv, h, inv_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β x y : H.LeftTransversal
h : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y) 1
rw : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y)⁻¹ 1
⊢ Eq (α := ↥H) (diff (MonoidHom.id ↥H) y x) 1
have rw₁ : Eq.{u_1 + 1} (α := ↥H) 1⁻¹ 1
Tactic: rw [← diff_inv, h, inv_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β x y : H.LeftTransversal
h : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y) 1
rw : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y)⁻¹ 1
rw₁ : Eq.{u_1 + 1} (α := ↥H) 1⁻¹ 1
⊢ Eq (α := ↥H) (diff (MonoidHom.id ↥H) y x) 1
have rw₂ : Eq.{u_1 + 1} (α := ↥H) 1 1
Tactic: rw [← diff_inv, h, inv_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β x y z : H.LeftTransversal
h : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y) 1
h' : Eq (α := ↥H) (diff (MonoidHom.id ↥H) y z) 1
⊢ Eq (α := ↥H) (diff (MonoidHom.id ↥H) x z) 1
have rw : HMul.hMul (α := ↥H) (diff (MonoidHom.id ↥H) x y) (diff (MonoidHom.id ↥H) y z) = 1
Tactic: rw [← diff_mul_diff, h, h', one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β x y z : H.LeftTransversal
h : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y) 1
h' : Eq (α := ↥H) (diff (MonoidHom.id ↥H) y z) 1
rw : HMul.hMul (α := ↥H) (diff (MonoidHom.id ↥H) x y) (diff (MonoidHom.id ↥H) y z) = 1
S : H.LeftTransversal
⊢ Eq (α := ↥H) (diff (MonoidHom.id ↥H) x z) 1
have rw₁ : HMul.hMul (α := ↥H) 1 (diff (MonoidHom.id ↥H) y z) = 1
Tactic: rw [← diff_mul_diff, h, h', one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β x y z : H.LeftTransversal
h : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y) 1
h' : Eq (α := ↥H) (diff (MonoidHom.id ↥H) y z) 1
rw : HMul.hMul (α := ↥H) (diff (MonoidHom.id ↥H) x y) (diff (MonoidHom.id ↥H) y z) = 1
S : H.LeftTransversal
rw₁ : HMul.hMul (α := ↥H) 1 (diff (MonoidHom.id ↥H) y z) = 1
⊢ Eq (α := ↥H) (diff (MonoidHom.id ↥H) x z) 1
have rw₂ : HMul.hMul (α := ↥H) 1 1 = 1
Tactic: rw [← diff_mul_diff, h, h', one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β x y z : H.LeftTransversal
h : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y) 1
h' : Eq (α := ↥H) (diff (MonoidHom.id ↥H) y z) 1
rw : HMul.hMul (α := ↥H) (diff (MonoidHom.id ↥H) x y) (diff (MonoidHom.id ↥H) y z) = 1
S : H.LeftTransversal
rw₁ : HMul.hMul (α := ↥H) 1 (diff (MonoidHom.id ↥H) y z) = 1
rw₂ : HMul.hMul (α := ↥H) 1 1 = 1
⊢ Eq (α := ↥H) (diff (MonoidHom.id ↥H) x z) 1
have rw₃ : Eq.{u_1 + 1} (α := ↥H) 1 1
Tactic: rw [← diff_mul_diff, h, h', one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) ⋯ = 1
have rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) sorry) : G) = (↑1 : G)
Tactic: rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) ⋯) : G) = (↑1 : G)
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) ⋯ = 1
have rw₁ : (unop g)⁻¹ * (↑1 : G) * unop g = (↑1 : G)
Tactic: rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) ⋯) : G) = (↑1 : G)
rw₁ : (unop g)⁻¹ * (↑1 : G) * unop g = (↑1 : G)
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) ⋯ = 1
have rw₂ : (unop g)⁻¹ * 1 * unop g = 1
Tactic: rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) ⋯) : G) = (↑1 : G)
rw₁ : (unop g)⁻¹ * (↑1 : G) * unop g = (↑1 : G)
rw₂ : (unop g)⁻¹ * 1 * unop g = 1
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) ⋯ = 1
have rw₃ : (unop g)⁻¹ * unop g = 1
Tactic: rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) ⋯) : G) = (↑1 : G)
rw₁ : (unop g)⁻¹ * (↑1 : G) * unop g = (↑1 : G)
rw₂ : (unop g)⁻¹ * 1 * unop g = 1
rw₃ : (unop g)⁻¹ * unop g = 1
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) ⋯ = 1
have rw₄ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
ϕ : ↥H →* ↥H :=
  { toFun := fun (h : ↥H) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑h : G) * unop g) ⋯, map_one' := ⋯,
    map_mul' := ⋯ }
⊢ diff (MonoidHom.id ↥H) (g • α) (g • β) =
    Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑(diff (MonoidHom.id ↥H) α β) : G) * unop g) ⋯
have refine : ∀ (x : G ⧸ H),
  Eq (α := ↥H)
    ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((sorry.leftQuotientEquiv (S := (↑(g • α) : Set G)) : (a : G ⧸ H) → (↑(↑(g • α) : Set G) : Type u_1)) x) :
                G)⁻¹
            (↑((sorry.leftQuotientEquiv (S := (↑(g • β) : Set G)) : (a : G ⧸ H) → (↑(↑(g • β) : Set G) : Type u_1)) x) : G))
          sorry) :
      ↥H)
    ((ϕ : (a : ↥H) → ↥H)
        ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((sorry.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1))
                      ((Equiv.symm (toPerm g) : (a : G ⧸ H) → G ⧸ H) x)) :
                  G)⁻¹
              (↑((sorry.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1))
                    ((Equiv.symm (toPerm g) : (a : G ⧸ H) → G ⧸ H) x)) :
                G))
            sorry)) :
      ↥H)
Tactic: refine (Fintype.prod_equiv (MulAction.toPerm g).symm _ _ fun x ↦ ?_).trans (map_prod ϕ _ _).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
g₁ g₂ : G
q : H.QuotientDiff
T : H.LeftTransversal
⊢ Eq.{u_1 + 1} (α := H.LeftTransversal) ((fun (α : H.LeftTransversal) ↦ op (g₁ * g₂)⁻¹ • α) T)
    ((fun (α : H.LeftTransversal) ↦ op g₁⁻¹ • α) ((fun (α : H.LeftTransversal) ↦ op g₂⁻¹ • α) T))
have rw : Eq.{u_1 + 1} (α := H.LeftTransversal) ((fun (α : H.LeftTransversal) ↦ op (g₂⁻¹ * g₁⁻¹) • α) T)
  ((fun (α : H.LeftTransversal) ↦ op g₁⁻¹ • α) ((fun (α : H.LeftTransversal) ↦ op g₂⁻¹ • α) T))
Tactic: rw [mul_inv_rev]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun (α : H.LeftTransversal) ↦ HSMul.hSMul (α := Gᵐᵒᵖ) (op 1⁻¹) α) T = T
have rw : (fun (α : H.LeftTransversal) ↦ HSMul.hSMul (α := Gᵐᵒᵖ) (op 1) α) T = T
Tactic: rw [inv_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ diff (MonoidHom.id ↥H) α (op (↑h : G) • β) = diff (MonoidHom.id ↥H) α β * h ^ H.index
have rw : Eq.{u_1 + 1} (α := ↥H)
  (∏ q : G ⧸ H,
    (MonoidHom.id ↥H : (a : ↥H) → ↥H)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        (HMul.hMul (α := G)
          (↑((sorry.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
          (↑((sorry.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
                  (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
                q) :
            G))
        sorry))
  (∏ x : G ⧸ H,
    HMul.hMul (α := ↥H)
      ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((sorry.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) x) : G)⁻¹
              (↑((sorry.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) x) : G))
            sorry) :
        ↥H)
      h)
Tactic: rw [diff, diff, index_eq_card, Nat.card_eq_fintype_card,
      ← Finset.card_univ, ← Finset.prod_const, ← Finset.prod_mul_distrib]